Timings for Idempotent.v

Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.

Require Import Basics.Equivalences Basics.Trunc Types.Sigma WildCat.Core.

Require Import Nat.Core Rings.Ring.

Local Open Scope mc_scope.

(** * Idempotent elements of rings *)

(** ** Definition *)

Class IsIdempotent (R : Ring) (e : R)
  := rng_idem : e * e = e.

Instance ishprop_isidempotent R e : IsHProp (IsIdempotent R e).

Proof.

  unfold IsIdempotent; exact _.

Defined.

(** *** Examples *)

(** Zero is idempotent. *)

Instance isidempotent_zero (R : Ring) : IsIdempotent R 0
  := rng_mult_zero_r 0.

(** One is idempotent. *)

Instance isidempotent_one (R : Ring) : IsIdempotent R 1
  := rng_mult_one_r 1.

(** If [e] is idempotent, then [1 - e] is idempotent. *)

Instance isidempotent_complement (R : Ring) (e : R) `{IsIdempotent R e}
  : IsIdempotent R (1 - e).

Proof.

  unfold IsIdempotent.

  rewrite rng_dist_l_negate.

  rewrite 2 rng_dist_r_negate.

  rewrite 2 rng_mult_one_l.

  rewrite rng_mult_one_r.

  rewrite rng_idem.

  rewrite rng_plus_negate_r.

  rewrite rng_negate_zero.

  napply rng_plus_zero_r.

Defined.

(** If [e] is idempotent, then it is also an idempotent element of the opposite ring. *)

Instance isidempotent_op (R : Ring) (e : R) `{i : IsIdempotent R e}
  : IsIdempotent (rng_op R) e
  := i.

(** Any positive power of an idempotent element [e] is [e]. *)

Definition rng_power_idem {R : Ring} (e : R) `{IsIdempotent R e} (n : nat)
  : (1 <= n)%nat -> rng_power e n = e.

Proof.

  intros L; induction L.

  -

 snapply rng_mult_one_r.

  -

 rhs_V rapply rng_idem.

    exact (ap (e *.) IHL).

Defined.

(** Ring homomorphisms preserve idempotent elements. *)

Instance isidempotent_rng_homo {R S : Ring} (f : R $-> S) (e : R)
  : IsIdempotent R e -> IsIdempotent S (f e).

Proof.

  intros p.

  lhs_V napply rng_homo_mult.

  exact (ap f p).

Defined.

(** ** Orthogonal idempotent elements *)

(** Two idempotent elements [e] and [f] are orthogonal if both [e * f = 0] and [f * e = 0]. *)

Class IsOrthogonal (R : Ring) (e f : R)
  `{!IsIdempotent R e, !IsIdempotent R f} := {
  rng_idem_orth : e * f = 0 ;
  rng_idem_orth' : f * e = 0 ;
}.

Definition issig_IsOrthogonal {R : Ring} {e f : R}
  `{IsIdempotent R e, IsIdempotent R f}
  : _ <~> IsOrthogonal R e f
  := ltac:(issig).

Instance ishprop_isorthogonal R e f
  `{IsIdempotent R e, IsIdempotent R f}
  : IsHProp (IsOrthogonal R e f).

Proof.

  exact (istrunc_equiv_istrunc _ issig_IsOrthogonal).

 
Defined.

(** *** Properties *)

(** Two idempotents being orthogonal is a symmetric relation. *)

Definition isorthogonal_swap (R : Ring) (e f : R) `{IsOrthogonal R e f}
  : IsOrthogonal R f e
  := {| rng_idem_orth := rng_idem_orth' ; rng_idem_orth' := rng_idem_orth |}.

Hint Immediate isorthogonal_swap : typeclass_instances.

(** If [e] and [f] are orthogonal idempotents, then they are also orthogonal idempotents in the opposite ring. *)

Instance isorthogonal_op {R : Ring} (e f : R) `{r : IsOrthogonal R e f}
  : IsOrthogonal (rng_op R) e f.

Proof.

  snapply Build_IsOrthogonal.

  -

 exact (rng_idem_orth' (R:=R)).

  -

 exact (rng_idem_orth (R:=R)).

Defined.

(** If [e] and [f] are orthogonal idempotents, then [e + f] is idempotent. *)

Instance isidempotent_plus_orthogonal {R : Ring} (e f : R)
  `{IsOrthogonal R e f}
  : IsIdempotent R (e + f).

Proof.

  unfold IsIdempotent.

  rewrite rng_dist_l.

  rewrite 2 rng_dist_r.

  rewrite 2 rng_idem.

  rewrite 2 rng_idem_orth.

  by rewrite rng_plus_zero_r, rng_plus_zero_l.

Defined.

(** An idempotent element [e] is orthogonal to its complement [1 - e]. *)

Instance isorthogonal_complement {R : Ring} (e : R) `{IsIdempotent R e}
  : IsOrthogonal R e (1 - e).

Proof.

  snapply Build_IsOrthogonal.

  1: rewrite rng_dist_l_negate,rng_mult_one_r.

  2: rewrite rng_dist_r_negate, rng_mult_one_l.

  1,2: rewrite rng_idem.

  1,2: apply rng_plus_negate_r.

Defined.