Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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).
R: Ring
e: R
IsHProp (IsIdempotent R e)
Proof.
R: Ring
e: R
IsHProp (IsIdempotent R e)
  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).
R: Ring
e: R
H: IsIdempotent R e
IsIdempotent R (1 - e)
Proof.
R: Ring
e: R
H: IsIdempotent R e
IsIdempotent R (1 - e)
  unfold IsIdempotent.
R: Ring
e: R
H: IsIdempotent R e
(1 - e) * (1 - e) = 1 - e
  rewrite rng_dist_l_negate.
R: Ring
e: R
H: IsIdempotent R e
(1 - e) * 1 - (1 - e) * e = 1 - e
  rewrite 2 rng_dist_r_negate.
R: Ring
e: R
H: IsIdempotent R e
1 * 1 - e * 1 - (1 * e - e * e) = 1 - e
  rewrite 2 rng_mult_one_l.
R: Ring
e: R
H: IsIdempotent R e
1 - e * 1 - (e - e * e) = 1 - e
  rewrite rng_mult_one_r.
R: Ring
e: R
H: IsIdempotent R e
1 - e - (e - e * e) = 1 - e
  rewrite rng_idem.
R: Ring
e: R
H: IsIdempotent R e
1 - e - (e - e) = 1 - e
  rewrite rng_plus_negate_r.
R: Ring
e: R
H: IsIdempotent R e
1 - e - 0 = 1 - e
  rewrite rng_negate_zero.
R: Ring
e: R
H: IsIdempotent R e
1 - e + 0 = 1 - e
  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.
R: Ring
e: R
H: IsIdempotent R e
n: nat
(1 <= n)%nat -> rng_power e n = e
Proof.
R: Ring
e: R
H: IsIdempotent R e
n: nat
(1 <= n)%nat -> rng_power e n = e
  intros L; induction L.
R: Ring
e: R
H: IsIdempotent R e
rng_power e 1 = e
R: Ring
e: R
H: IsIdempotent R e
m: nat
L: (1 <= m)%nat
IHL: rng_power e m = e
rng_power e m.+1 = e
  -
R: Ring
e: R
H: IsIdempotent R e
rng_power e 1 = e snapply rng_mult_one_r.
  -
R: Ring
e: R
H: IsIdempotent R e
m: nat
L: (1 <= m)%nat
IHL: rng_power e m = e
rng_power e m.+1 = e rhs_V rapply rng_idem.
R: Ring
e: R
H: IsIdempotent R e
m: nat
L: (1 <= m)%nat
IHL: rng_power e m = e
rng_power e m.+1 = e * e
    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).
R, S: Ring
f: R $-> S
e: R
IsIdempotent R e -> IsIdempotent S (f e)
Proof.
R, S: Ring
f: R $-> S
e: R
IsIdempotent R e -> IsIdempotent S (f e)
  intros p.
R, S: Ring
f: R $-> S
e: R
p: IsIdempotent R e
IsIdempotent S (f e)
  lhs_V napply rng_homo_mult.
R, S: Ring
f: R $-> S
e: R
p: IsIdempotent R e
f (e * e) = f e
  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).
R: Ring
e, f: R
H: IsIdempotent R e
H0: IsIdempotent R f
IsHProp (IsOrthogonal R e f)
Proof.
R: Ring
e, f: R
H: IsIdempotent R e
H0: IsIdempotent R f
IsHProp (IsOrthogonal R e f)
  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.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
r: IsOrthogonal R e f
IsOrthogonal (rng_op R) e f
Proof.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
r: IsOrthogonal R e f
IsOrthogonal (rng_op R) e f
  snapply Build_IsOrthogonal.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
r: IsOrthogonal R e f
e * f = 0
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
r: IsOrthogonal R e f
f * e = 0
  -
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
r: IsOrthogonal R e f
e * f = 0 exact (rng_idem_orth' (R:=R)).
  -
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
r: IsOrthogonal R e f
f * e = 0 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).
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
IsIdempotent R (e + f)
Proof.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
IsIdempotent R (e + f)
  unfold IsIdempotent.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
(e + f) * (e + f) = e + f
  rewrite rng_dist_l.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
(e + f) * e + (e + f) * f = e + f
  rewrite 2 rng_dist_r.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
e * e + f * e + (e * f + f * f) = e + f
  rewrite 2 rng_idem.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
e + f * e + (e * f + f) = e + f
  rewrite 2 rng_idem_orth.
R: Ring
e, f: R
IsIdempotent0: IsIdempotent R e
IsIdempotent1: IsIdempotent R f
H: IsOrthogonal R e f
e + 0 + (0 + f) = e + f
  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).
R: Ring
e: R
H: IsIdempotent R e
IsOrthogonal R e (1 - e)
Proof.
R: Ring
e: R
H: IsIdempotent R e
IsOrthogonal R e (1 - e)
  snapply Build_IsOrthogonal.
R: Ring
e: R
H: IsIdempotent R e
e * (1 - e) = 0
R: Ring
e: R
H: IsIdempotent R e
(1 - e) * e = 0
  1: rewrite rng_dist_l_negate,rng_mult_one_r.
R: Ring
e: R
H: IsIdempotent R e
e - e * e = 0
R: Ring
e: R
H: IsIdempotent R e
(1 - e) * e = 0
  2: rewrite rng_dist_r_negate, rng_mult_one_l.
R: Ring
e: R
H: IsIdempotent R e
e - e * e = 0
R: Ring
e: R
H: IsIdempotent R e
e - e * e = 0
  1,2: rewrite rng_idem.
R: Ring
e: R
H: IsIdempotent R e
e - e = 0
R: Ring
e: R
H: IsIdempotent R e
e - e = 0
  1,2: apply rng_plus_negate_r.
Defined.