diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v new file mode 100644 index 0000000000..36e23dc519 --- /dev/null +++ b/theories/Algebra/Rings/Idempotent.v @@ -0,0 +1,128 @@ +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. + +Global Instance ishprop_isidempotent R e : IsHProp (IsIdempotent R e). +Proof. + unfold IsIdempotent; exact _. +Defined. + +(** *** Examples *) + +(** Zero is idempotent. *) +Global Instance isidempotent_zero (R : Ring) : IsIdempotent R 0 + := rng_mult_zero_r 0. + +(** One is idempotent. *) +Global Instance isidempotent_one (R : Ring) : IsIdempotent R 1 + := rng_mult_one_r 1. + +(** If [e] is idempotent, then [1 - e] is idempotent. *) +Global 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. + nrapply rng_plus_zero_r. +Defined. + +(** If [e] is idempotent, then it is also an idempotent element of the opposite ring. *) +Global 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. + - snrapply rng_mult_one_r. + - rhs_V rapply rng_idem. + exact (ap (e *.) IHL). +Defined. + +(** Ring homomorphisms preserve idempotent elements. *) +Global Instance isidempotent_rng_homo {R S : Ring} (f : R $-> S) (e : R) + : IsIdempotent R e -> IsIdempotent S (f e). +Proof. + intros p. + lhs_V nrapply 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). + +Global 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. *) +Global Instance isorthogonal_op {R : Ring} (e f : R) `{r : IsOrthogonal R e f} + : IsOrthogonal (rng_op R) e f. +Proof. + snrapply 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. *) +Global 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]. *) +Global Instance isorthogonal_complement {R : Ring} (e : R) `{IsIdempotent R e} + : IsOrthogonal R e (1 - e). +Proof. + snrapply 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.