From fe083fee2e0ee8eb33986b65c0ac1f33c32766dc Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 30 Sep 2024 02:09:13 +0100 Subject: [PATCH 1/6] Idempotent ring elements Signed-off-by: Ali Caglayan --- theories/Algebra/Rings/Idempotent.v | 129 ++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) create mode 100644 theories/Algebra/Rings/Idempotent.v diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v new file mode 100644 index 0000000000..09c08a94c3 --- /dev/null +++ b/theories/Algebra/Rings/Idempotent.v @@ -0,0 +1,129 @@ +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_compliment (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) `{IsIdempotent R e} + : IsIdempotent (rng_op R) e + := rng_idem (R:=R). + +(** 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_compliment {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. From d7cb35aef73f0528cc56d51a9ba81f8ee1f4008d Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 30 Sep 2024 22:03:44 +0100 Subject: [PATCH 2/6] Update theories/Algebra/Rings/Idempotent.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/Idempotent.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v index 09c08a94c3..8d40ac7078 100644 --- a/theories/Algebra/Rings/Idempotent.v +++ b/theories/Algebra/Rings/Idempotent.v @@ -27,7 +27,7 @@ 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_compliment (R : Ring) (e : R) `{IsIdempotent R e} +Global Instance isidempotent_complement (R : Ring) (e : R) `{IsIdempotent R e} : IsIdempotent R (1 - e). Proof. unfold IsIdempotent. From ebea79a8eba79900532806e1bda24bb4094644ba Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 30 Sep 2024 22:03:50 +0100 Subject: [PATCH 3/6] Update theories/Algebra/Rings/Idempotent.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/Idempotent.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v index 8d40ac7078..932bbb9043 100644 --- a/theories/Algebra/Rings/Idempotent.v +++ b/theories/Algebra/Rings/Idempotent.v @@ -93,8 +93,6 @@ 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. From 1b98b8820b32cded7a79c97ba65a94d916154ef9 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 30 Sep 2024 22:59:06 +0100 Subject: [PATCH 4/6] Update theories/Algebra/Rings/Idempotent.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/Idempotent.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v index 932bbb9043..6e15e19008 100644 --- a/theories/Algebra/Rings/Idempotent.v +++ b/theories/Algebra/Rings/Idempotent.v @@ -116,7 +116,7 @@ Proof. Defined. (** An idempotent element [e] is orthogonal to its complement [1 - e]. *) -Global Instance isorthogonal_compliment {R : Ring} (e : R) `{IsIdempotent R e} +Global Instance isorthogonal_complement {R : Ring} (e : R) `{IsIdempotent R e} : IsOrthogonal R e (1 - e). Proof. snrapply Build_IsOrthogonal. From 51ae9372f361de554942201f677486e1d8809a31 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 30 Sep 2024 22:59:14 +0100 Subject: [PATCH 5/6] Update theories/Algebra/Rings/Idempotent.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/Idempotent.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v index 6e15e19008..21905fdcd7 100644 --- a/theories/Algebra/Rings/Idempotent.v +++ b/theories/Algebra/Rings/Idempotent.v @@ -93,6 +93,7 @@ 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. From 72e906be3b8ed3cc61e3ab0922f2edc7ad044997 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 30 Sep 2024 22:59:34 +0100 Subject: [PATCH 6/6] Update theories/Algebra/Rings/Idempotent.v Co-authored-by: Dan Christensen --- theories/Algebra/Rings/Idempotent.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Algebra/Rings/Idempotent.v b/theories/Algebra/Rings/Idempotent.v index 21905fdcd7..36e23dc519 100644 --- a/theories/Algebra/Rings/Idempotent.v +++ b/theories/Algebra/Rings/Idempotent.v @@ -42,9 +42,9 @@ Proof. Defined. (** If [e] is idempotent, then it is also an idempotent element of the opposite ring. *) -Global Instance isidempotent_op (R : Ring) (e : R) `{IsIdempotent R e} +Global Instance isidempotent_op (R : Ring) (e : R) `{i : IsIdempotent R e} : IsIdempotent (rng_op R) e - := rng_idem (R:=R). + := i. (** Any positive power of an idempotent element [e] is [e]. *) Definition rng_power_idem {R : Ring} (e : R) `{IsIdempotent R e} (n : nat)