From f4a9f0aa602315531252068ac8d039600ed1fb8c Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 10 Oct 2024 23:18:57 +0100
Subject: [PATCH 01/11] associativity of ideal product

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 43ff35d0-6f6a-46c5-94b5-479411cf915c -->
---
 theories/Algebra/Rings/Ideal.v | 33 +++++++++++++++++++++++++++++----
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 160c1205786..a7da65b0f59 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -904,12 +904,37 @@ Section IdealLemmas.
     + by apply ideal_in_plus_negate.
   Defined.
 
-  (** TODO: *)
   (** The product of ideals is an associative operation. *)
-  (* Lemma ideal_product_assoc (I J K : Ideal R) : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
+  Lemma ideal_product_assoc (I J K : Ideal R) : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
   Proof.
-    intros r; split; apply Trunc_functor.
-  Abort. *)
+    snrapply ideal_subset_antisymm.
+    - intros x.
+      apply Trunc_rec. 
+      intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
+      + strip_truncations.
+        induction q as [t [z w r s] | | t k p1 IHp1 p2 IHp2].
+        * rewrite rng_mult_assoc.
+          by apply tr, sgt_in, ipn_in; [ apply tr, sgt_in, ipn_in | ].
+        * rewrite rng_mult_zero_r.
+          apply ideal_in_zero.
+        * rewrite rng_dist_l_negate.
+          by apply ideal_in_plus_negate.
+      + apply ideal_in_zero.
+      + by apply ideal_in_plus_negate.
+    - intros x.
+      apply Trunc_rec.
+      intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
+      + strip_truncations.
+        induction p as [t [y w r s] | | t k p1 IHp1 p2 IHp2].
+        * rewrite <- rng_mult_assoc.
+          by apply tr, sgt_in, ipn_in; [ | apply tr, sgt_in, ipn_in ].
+        * rewrite rng_mult_zero_l.
+          apply ideal_in_zero.
+        * rewrite rng_dist_r_negate.
+          by apply ideal_in_plus_negate.
+      + apply ideal_in_zero.
+      + by apply ideal_in_plus_negate.
+  Defined.
 
   (** Products of ideals are subsets of their intersection. *)
   Lemma ideal_product_subset_intersection (I J : Ideal R) : I ⋅ J ⊆ I ∩ J.

From b615412d1ecede886fe0229dd7160fda0c7205a1 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 18 Nov 2024 11:46:36 +0000
Subject: [PATCH 02/11] explode IdealLemmas section

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 872 +++++++++++++++++----------------
 1 file changed, 438 insertions(+), 434 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index a7da65b0f59..d24a439bb3a 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -793,454 +793,458 @@ End Notation.
 
 (** *** Ideal lemmas *)
 
-Section IdealLemmas.
-
-  Context {R : Ring}.
-
-  (** Subset relation is antisymmetric. *)
-  Lemma ideal_subset_antisymm (I J : Subgroup R) : I ⊆ J -> J ⊆ I -> I ↔ J.
-  Proof.
-    intros p q x; split; by revert x.
-  Defined.
-
-  (** The zero ideal is contained in all ideals. *)
-  Lemma ideal_zero_subset (I : Subgroup R) : ideal_zero R ⊆ I.
-  Proof.
-    intros x p; rewrite p; apply ideal_in_zero.
-  Defined.
-
-  (** The unit ideal contains all ideals. *)
-  Lemma ideal_unit_subset (I : Subgroup R) : I ⊆ ideal_unit R.
-  Proof.
-    hnf; cbn; trivial.
-  Defined.
-
-  (** Intersection includes into the left *)
-  Lemma ideal_intersection_subset_l (I J : Ideal R) : I ∩ J ⊆ I.
-  Proof.
-    intro; exact fst.
-  Defined.
-
-  (** Intersection includes into the right *)
-  Lemma ideal_intersection_subset_r (I J : Ideal R) : I ∩ J ⊆ J.
-  Proof.
-    intro; exact snd.
-  Defined.
-
-  (** Subsets of intersections *)
-  Lemma ideal_intersection_subset (I J K : Ideal R)
-    : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
-  Proof.
-    intros p q x r; specialize (p x r); specialize (q x r); by split.
-  Defined.
-
-  (** Ideals include into their sum on the left *)
-  Lemma ideal_sum_subset_l (I J : Ideal R) : I ⊆ (I + J).
-  Proof.
-    intros x p.
-    apply tr, sgt_in.
-    left; exact p.
-  Defined.
+(** Subset relation is antisymmetric. *)
+Lemma ideal_subset_antisymm {R : Ring} (I J : Subgroup R)
+  : I ⊆ J -> J ⊆ I -> I ↔ J.
+Proof.
+  intros p q x; split; by revert x.
+Defined.
 
-  (** Ideals include into their sum on the right *)
-  Lemma ideal_sum_subset_r (I J : Ideal R) : J ⊆ (I + J).
-  Proof.
-    intros x p.
-    apply tr, sgt_in.
-    right; exact p.
-  Defined.
+(** The zero ideal is contained in all ideals. *)
+Lemma ideal_zero_subset {R : Ring} (I : Subgroup R) : ideal_zero R ⊆ I.
+Proof.
+  intros x p; rewrite p; apply ideal_in_zero.
+Defined.
 
-  #[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
+(** The unit ideal contains all ideals. *)
+Lemma ideal_unit_subset {R : Ring} (I : Subgroup R) : I ⊆ ideal_unit R.
+Proof.
+  hnf; cbn; trivial.
+Defined.
 
-  (** Products of ideals are included in their left factor *)
-  Lemma ideal_product_subset_l (I J : Ideal R) : I ⋅ J ⊆ I.
-  Proof.
-    intros r p.
-    strip_truncations.
-    induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
-    + destruct i as [s t].
-      by rapply isrightideal.
-    + rapply ideal_in_zero.
-    + by rapply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals are included in their right factor. *)
-  Lemma ideal_product_subset_r (I J : Ideal R) : I ⋅ J ⊆ J.
-  Proof.
-    intros r p.
-    strip_truncations.
-    induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
-    + destruct i as [s t].
-      by apply isleftideal.
-    + rapply ideal_in_zero.
-    + by rapply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals preserve subsets on the left *)
-  Lemma ideal_product_subset_pres_l (I J K : Ideal R) : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
-  Proof.
-    intros p r q.
-    strip_truncations.
-    induction q as [r i | | r s ].
-    + destruct i.
-      apply tr, sgt_in, ipn_in.
-      1: apply p.
-      1,2: assumption.
+(** Intersection includes into the left *)
+Lemma ideal_intersection_subset_l {R : Ring} (I J : Ideal R) : I ∩ J ⊆ I.
+Proof.
+  intro; exact fst.
+Defined.
+
+(** Intersection includes into the right *)
+Lemma ideal_intersection_subset_r {R : Ring} (I J : Ideal R) : I ∩ J ⊆ J.
+Proof.
+  intro; exact snd.
+Defined.
+
+(** Subsets of intersections *)
+Lemma ideal_intersection_subset {R : Ring} (I J K : Ideal R)
+  : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
+Proof.
+  intros p q x r; specialize (p x r); specialize (q x r); by split.
+Defined.
+
+(** Ideals include into their sum on the left *)
+Lemma ideal_sum_subset_l {R : Ring} (I J : Ideal R) : I ⊆ (I + J).
+Proof.
+  intros x p.
+  apply tr, sgt_in.
+  left; exact p.
+Defined.
+
+(** Ideals include into their sum on the right *)
+Lemma ideal_sum_subset_r {R : Ring} (I J : Ideal R) : J ⊆ (I + J).
+Proof.
+  intros x p.
+  apply tr, sgt_in.
+  right; exact p.
+Defined.
+
+#[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
+
+(** Products of ideals are included in their left factor *)
+Lemma ideal_product_subset_l {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ I.
+Proof.
+  intros r p.
+  strip_truncations.
+  induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
+  + destruct i as [s t].
+    by rapply isrightideal.
+  + rapply ideal_in_zero.
+  + by rapply ideal_in_plus_negate.
+Defined.
+
+(** Products of ideals are included in their right factor. *)
+Lemma ideal_product_subset_r {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ J.
+Proof.
+  intros r p.
+  strip_truncations.
+  induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
+  + destruct i as [s t].
+    by apply isleftideal.
+  + rapply ideal_in_zero.
+  + by rapply ideal_in_plus_negate.
+Defined.
+
+(** Products of ideals preserve subsets on the left *)
+Lemma ideal_product_subset_pres_l {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
+Proof.
+  intros p r q.
+  strip_truncations.
+  induction q as [r i | | r s ].
+  + destruct i.
+    apply tr, sgt_in, ipn_in.
+    1: apply p.
+    1,2: assumption.
+  + apply ideal_in_zero.
+  + by apply ideal_in_plus_negate.
+Defined.
+
+(** Products of ideals preserve subsets on the right *)
+Lemma ideal_product_subset_pres_r {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
+Proof.
+  intros p r q.
+  strip_truncations.
+  induction q as [r i | | r s ].
+  + destruct i.
+    apply tr, sgt_in, ipn_in.
+    2: apply p.
+    1,2: assumption.
+  + apply ideal_in_zero.
+  + by apply ideal_in_plus_negate.
+Defined.
+
+(** The product of ideals is an associative operation. *)
+Lemma ideal_product_assoc {R : Ring} (I J K : Ideal R)
+  : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
+Proof.
+  snrapply ideal_subset_antisymm.
+  - intros x.
+    apply Trunc_rec. 
+    intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
+    + strip_truncations.
+      induction q as [t [z w r s] | | t k p1 IHp1 p2 IHp2].
+      * rewrite rng_mult_assoc.
+        by apply tr, sgt_in, ipn_in; [ apply tr, sgt_in, ipn_in | ].
+      * rewrite rng_mult_zero_r.
+        apply ideal_in_zero.
+      * rewrite rng_dist_l_negate.
+        by apply ideal_in_plus_negate.
     + apply ideal_in_zero.
     + by apply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals preserve subsets on the right *)
-  Lemma ideal_product_subset_pres_r (I J K : Ideal R) : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
-  Proof.
-    intros p r q.
-    strip_truncations.
-    induction q as [r i | | r s ].
-    + destruct i.
-      apply tr, sgt_in, ipn_in.
-      2: apply p.
-      1,2: assumption.
+  - intros x.
+    apply Trunc_rec.
+    intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
+    + strip_truncations.
+      induction p as [t [y w r s] | | t k p1 IHp1 p2 IHp2].
+      * rewrite <- rng_mult_assoc.
+        by apply tr, sgt_in, ipn_in; [ | apply tr, sgt_in, ipn_in ].
+      * rewrite rng_mult_zero_l.
+        apply ideal_in_zero.
+      * rewrite rng_dist_r_negate.
+        by apply ideal_in_plus_negate.
     + apply ideal_in_zero.
     + by apply ideal_in_plus_negate.
-  Defined.
-
-  (** The product of ideals is an associative operation. *)
-  Lemma ideal_product_assoc (I J K : Ideal R) : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
-  Proof.
-    snrapply ideal_subset_antisymm.
-    - intros x.
-      apply Trunc_rec. 
-      intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
-      + strip_truncations.
-        induction q as [t [z w r s] | | t k p1 IHp1 p2 IHp2].
-        * rewrite rng_mult_assoc.
-          by apply tr, sgt_in, ipn_in; [ apply tr, sgt_in, ipn_in | ].
-        * rewrite rng_mult_zero_r.
-          apply ideal_in_zero.
-        * rewrite rng_dist_l_negate.
-          by apply ideal_in_plus_negate.
-      + apply ideal_in_zero.
-      + by apply ideal_in_plus_negate.
-    - intros x.
-      apply Trunc_rec.
-      intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
-      + strip_truncations.
-        induction p as [t [y w r s] | | t k p1 IHp1 p2 IHp2].
-        * rewrite <- rng_mult_assoc.
-          by apply tr, sgt_in, ipn_in; [ | apply tr, sgt_in, ipn_in ].
-        * rewrite rng_mult_zero_l.
-          apply ideal_in_zero.
-        * rewrite rng_dist_r_negate.
-          by apply ideal_in_plus_negate.
-      + apply ideal_in_zero.
-      + by apply ideal_in_plus_negate.
-  Defined.
-
-  (** Products of ideals are subsets of their intersection. *)
-  Lemma ideal_product_subset_intersection (I J : Ideal R) : I ⋅ J ⊆ I ∩ J.
-  Proof.
-    apply ideal_intersection_subset.
-    + apply ideal_product_subset_l.
-    + apply ideal_product_subset_r.
-  Defined.
-
-  (** Sums of ideals are the smallest ideal containing the summands. *)
-  Lemma ideal_sum_smallest (I J K : Ideal R) : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
-  Proof.
-    intros p q.
-    refine (ideal_sum_ind I J (fun x _ => K x) p q _ _).
-    1: apply ideal_in_zero.
-    intros y z s t.
-    rapply ideal_in_plus_negate.
-  Defined.
-
-  (** Ideals absorb themselves under sum. *)
-  Lemma ideal_sum_self (I : Ideal R) : I + I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: by rapply ideal_sum_smallest.
-    rapply ideal_sum_subset_l.
-  Defined.
-
-  (** Sums preserve inclusions in the left summand. *)
-  Lemma ideal_sum_subset_pres_l (I J K : Ideal R) : I ⊆ J -> (I + K) ⊆ (J + K).
-  Proof.
-    intros p.
-    apply ideal_sum_smallest.
-    { transitivity J.
-      1: exact p.
-      apply ideal_sum_subset_l. }
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Sums preserve inclusions in the right summand. *)
-  Lemma ideal_sum_subset_pres_r (I J K : Ideal R) : I ⊆ J -> (K + I) ⊆ (K + J).
-  Proof.
-    intros p.
-    apply ideal_sum_smallest.
-    1: apply ideal_sum_subset_l.
-    transitivity J.
+Defined.
+
+(** Products of ideals are subsets of their intersection. *)
+Lemma ideal_product_subset_intersection {R : Ring} (I J : Ideal R)
+  : I ⋅ J ⊆ I ∩ J.
+Proof.
+  apply ideal_intersection_subset.
+  + apply ideal_product_subset_l.
+  + apply ideal_product_subset_r.
+Defined.
+
+(** Sums of ideals are the smallest ideal containing the summands. *)
+Lemma ideal_sum_smallest {R : Ring} (I J K : Ideal R)
+  : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
+Proof.
+  intros p q.
+  refine (ideal_sum_ind I J (fun x _ => K x) p q _ _).
+  1: apply ideal_in_zero.
+  intros y z s t.
+  rapply ideal_in_plus_negate.
+Defined.
+
+(** Ideals absorb themselves under sum. *)
+Lemma ideal_sum_self {R : Ring} (I : Ideal R) : I + I ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: by rapply ideal_sum_smallest.
+  rapply ideal_sum_subset_l.
+Defined.
+
+(** Sums preserve inclusions in the left summand. *)
+Lemma ideal_sum_subset_pres_l {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> (I + K) ⊆ (J + K).
+Proof.
+  intros p.
+  apply ideal_sum_smallest.
+  { transitivity J.
     1: exact p.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Products left distribute over sums *)
-  (** Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
-  Lemma ideal_dist_l (I J K : Ideal R) : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
-  Proof.
-    (** We split into two directions. *)
-    apply ideal_subset_antisymm.
-    (** We deal with the difficult inclusion first. The proof comes down to breaking down the definition and reassembling into the right. *)
-    { intros r p.
-      strip_truncations.
-      induction p as [ r i | | r s p1 IHp1 p2 IHp2].
-      - destruct i as [r s p q].
-        strip_truncations.
-        induction q as [ t k | | t k p1 IHp1 p2 IHp2 ].
-        + apply tr, sgt_in.
-          destruct k as [j | k].
-          * left; by apply tr, sgt_in, ipn_in.
-          * right; by apply tr, sgt_in, ipn_in.
-        + apply tr, sgt_in; left.
-          rewrite rng_mult_zero_r.
-          apply ideal_in_zero.
-        + rewrite rng_dist_l.
-          rewrite rng_mult_negate_r.
-          by apply ideal_in_plus_negate.
-      - apply ideal_in_zero.
-      - by apply ideal_in_plus_negate. }
-    (** This is the easy direction which can use previous lemmas. *)
-    apply ideal_sum_smallest.
-    1,2: apply ideal_product_subset_pres_r.
-    1: apply ideal_sum_subset_l.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Products distribute over sums on the right. *)
-  (** The proof is very similar to the left version *)
-  Lemma ideal_dist_r (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
-  Proof.
-    apply ideal_subset_antisymm.
-    { intros r p.
-      strip_truncations.
-      induction p as [ r i | | r s p1 IHp1 p2 IHp2].
-      - destruct i as [r s p q].
-        strip_truncations.
-        induction p as [ t k | | t k p1 IHp1 p2 IHp2 ].
-        + apply tr, sgt_in.
-          destruct k as [j | k].
-          * left; by apply tr, sgt_in, ipn_in.
-          * right; by apply tr, sgt_in, ipn_in.
-        + apply tr, sgt_in; left.
-          rewrite rng_mult_zero_l.
-          apply ideal_in_zero.
-        + rewrite rng_dist_r.
-          rewrite rng_mult_negate_l.
-          by apply ideal_in_plus_negate.
-      - apply ideal_in_zero.
-      - by apply ideal_in_plus_negate. }
-    apply ideal_sum_smallest.
-    1,2: apply ideal_product_subset_pres_l.
-    1: apply ideal_sum_subset_l.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Ideal sums are commutative *)
-  Lemma ideal_sum_comm (I J : Ideal R) : I + J ↔ J + I.
-  Proof.
-    apply ideal_subset_antisymm; apply ideal_sum_smallest.
-    1,3: apply ideal_sum_subset_r.
-    1,2: apply ideal_sum_subset_l.
-  Defined.
-
-  (** Zero ideal is left additive identity. *) 
-  Lemma ideal_sum_zero_l I : ideal_zero R + I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_sum_smallest.
-    1: apply ideal_zero_subset.
-    1: reflexivity.
-    apply ideal_sum_subset_r.
-  Defined.
-
-  (** Zero ideal is right additive identity. *)
-  Lemma ideal_sum_zero_r I : I + ideal_zero R ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_sum_smallest.
-    1: reflexivity.
-    1: apply ideal_zero_subset.
-    apply ideal_sum_subset_l.
-  Defined.
-
-  (** Unit ideal is left multiplicative identity. *)
-  Lemma ideal_product_unit_l I : ideal_unit R ⋅ I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_product_subset_r.
-    intros r p.
-    rewrite <- rng_mult_one_l.
-    by apply tr, sgt_in, ipn_in.
-  Defined.
-
-  (** Unit ideal is right multiplicative identity. *)
-  Lemma ideal_product_unit_r I : I ⋅ ideal_unit R ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_product_subset_l.
-    intros r p.
-    rewrite <- rng_mult_one_r.
-    by apply tr, sgt_in, ipn_in.
-  Defined.
-
-  (** Intersecting with unit ideal on the left does nothing. *)
-  Lemma ideal_intresection_unit_l I : ideal_unit R ∩ I ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_intersection_subset_r.
-    apply ideal_intersection_subset.
-    1: apply ideal_unit_subset.
-    reflexivity.
-  Defined.
-
-  (** Intersecting with unit ideal on right does nothing. *)
-  Lemma ideal_intersection_unit_r I : I ∩ ideal_unit R ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    1: apply ideal_intersection_subset_l.
-    apply ideal_intersection_subset.
-    1: reflexivity.
-    apply ideal_unit_subset.
-  Defined.
-
-  (** Product of intersection and sum is subset of sum of products *)
-  Lemma ideal_product_intersection_sum_subset (I J : Ideal R)
-    : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
-  Proof.
-    etransitivity.
-    1: rapply ideal_dist_l.
-    etransitivity.
-    1: rapply ideal_sum_subset_pres_r.
-    1: rapply ideal_product_subset_pres_l.
-    1: apply ideal_intersection_subset_l.
-    etransitivity.
-    1: rapply ideal_sum_subset_pres_l.
-    1: rapply ideal_product_subset_pres_l.
-    1: apply ideal_intersection_subset_r.
-    rapply ideal_sum_comm.
-  Defined.
-
-  (** Ideals are subsets of their ideal quotients *)
-  Lemma ideal_quotient_subset (I J : Ideal R) : I ⊆ (I :: J).
-  Proof.
-    intros x i; split; apply tr; intros r j; cbn.
-    - by rapply isrightideal.
-    - by rapply isleftideal.
-  Defined.
-
-  (** If J divides I then the ideal quotient of J by I is trivial. *)
-  Lemma ideal_quotient_trivial (I J : Ideal R)
-    : I ⊆ J -> J :: I ↔ ideal_unit R.
-  Proof.
-    intros p.
-    apply ideal_subset_antisymm.
-    1: cbv; trivial.
-    intros r _; split; apply tr; intros x q; cbn.
-    - by apply isleftideal, p. 
-    - rapply isrightideal.
-      by apply p.
-  Defined.
-
-  (** The ideal quotient of I by unit is I. *)
-  Lemma ideal_quotient_unit_bottom (I : Ideal R)
-    : (I :: ideal_unit R) ↔ I.
-  Proof.
-    apply ideal_subset_antisymm.
-    - intros r [p q].
+    apply ideal_sum_subset_l. }
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Sums preserve inclusions in the right summand. *)
+Lemma ideal_sum_subset_pres_r {R : Ring} (I J K : Ideal R)
+  : I ⊆ J -> (K + I) ⊆ (K + J).
+Proof.
+  intros p.
+  apply ideal_sum_smallest.
+  1: apply ideal_sum_subset_l.
+  transitivity J.
+  1: exact p.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Products left distribute over sums *)
+(** Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
+Lemma ideal_dist_l {R : Ring} (I J K : Ideal R)
+  : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
+Proof.
+  (** We split into two directions. *)
+  apply ideal_subset_antisymm.
+  (** We deal with the difficult inclusion first. The proof comes down to breaking down the definition and reassembling into the right. *)
+  { intros r p.
+    strip_truncations.
+    induction p as [ r i | | r s p1 IHp1 p2 IHp2].
+    - destruct i as [r s p q].
       strip_truncations.
-      rewrite <- rng_mult_one_r.
-      exact (p ring_one tt).
-    - apply ideal_quotient_subset.
-  Defined.
-
-  (** The ideal quotient of unit by I is unit. *)
-  Lemma ideal_quotient_unit_top (I : Ideal R)
-    : (ideal_unit R :: I) ↔ ideal_unit R.
-  Proof.
-    split.
-    - cbn; trivial.
-    - intros ?; split; apply tr;
-      cbn; split; trivial. 
-  Defined.
-
-  (** The ideal quotient by a sum is an intersection of ideal quotients. *)
-  Lemma ideal_quotient_sum (I J K : Ideal R)
-    : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
-  Proof.
-    apply ideal_subset_antisymm.
-    { intros r [p q]; strip_truncations; split; split; apply tr; intros x jk.
-      - by rapply p; rapply ideal_sum_subset_l.
-      - by rapply q; rapply ideal_sum_subset_l.
-      - by rapply p; rapply ideal_sum_subset_r.
-      - by rapply q; rapply ideal_sum_subset_r. }
-    intros r [[p q] [u v]]; strip_truncations; split; apply tr;
-    intros x jk; strip_truncations.
-    - induction jk as [? [] | | ? ? ? ? ? ? ].
-      + by apply p.
-      + by apply u.
-      + apply u, ideal_in_zero.
+      induction q as [ t k | | t k p1 IHp1 p2 IHp2 ].
+      + apply tr, sgt_in.
+        destruct k as [j | k].
+        * left; by apply tr, sgt_in, ipn_in.
+        * right; by apply tr, sgt_in, ipn_in.
+      + apply tr, sgt_in; left.
+        rewrite rng_mult_zero_r.
+        apply ideal_in_zero.
       + rewrite rng_dist_l.
         rewrite rng_mult_negate_r.
         by apply ideal_in_plus_negate.
-    - induction jk as [? [] | | ? ? ? ? ? ? ].
-      + by apply q.
-      + by apply v.
-      + apply v, ideal_in_zero.
-      + change (I ((g - h) * r)). 
-        rewrite rng_dist_r.
+    - apply ideal_in_zero.
+    - by apply ideal_in_plus_negate. }
+  (** This is the easy direction which can use previous lemmas. *)
+  apply ideal_sum_smallest.
+  1,2: apply ideal_product_subset_pres_r.
+  1: apply ideal_sum_subset_l.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Products distribute over sums on the right. *)
+(** The proof is very similar to the left version *)
+Lemma ideal_dist_r {R : Ring} (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
+Proof.
+  apply ideal_subset_antisymm.
+  { intros r p.
+    strip_truncations.
+    induction p as [ r i | | r s p1 IHp1 p2 IHp2].
+    - destruct i as [r s p q].
+      strip_truncations.
+      induction p as [ t k | | t k p1 IHp1 p2 IHp2 ].
+      + apply tr, sgt_in.
+        destruct k as [j | k].
+        * left; by apply tr, sgt_in, ipn_in.
+        * right; by apply tr, sgt_in, ipn_in.
+      + apply tr, sgt_in; left.
+        rewrite rng_mult_zero_l.
+        apply ideal_in_zero.
+      + rewrite rng_dist_r.
         rewrite rng_mult_negate_l.
         by apply ideal_in_plus_negate.
-  Defined.
-
-  (** Ideal quotients distribute over intersections. *)
-  Lemma ideal_quotient_intersection (I J K : Ideal R)
-    : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
-  Proof.
-    apply ideal_subset_antisymm.
-    - intros r [p q]; strip_truncations; split; split; apply tr; intros x k.
-      1,3: by apply p.
-      1,2: by apply q.
-    - intros r [[p q] [u v]].
-      strip_truncations; split; apply tr; intros x k; split.
-      + by apply p.
-      + by apply u.
-      + by apply q.
-      + by apply v.
-  Defined.
-
-  (** Annihilators reverse the order of inclusion. *)
-  Lemma ideal_annihilator_subset (I J : Ideal R) : I ⊆ J -> Ann J ⊆ Ann I.
-  Proof.
-    intros p x [q q']; hnf in q, q'; strip_truncations;
-      split; apply tr; intros y i.
-    - by apply q, p.
-    - by apply q', p.
-  Defined.
-
-  (** The annihilator of an ideal is equal to a quotient of zero. *)
-  Lemma ideal_annihilator_zero_quotient (I : Ideal R)
-    : Ann I ↔ ideal_zero R :: I.
-  Proof.
-    intros x; split.
-    - intros [p q]; strip_truncations; split; apply tr; intros y i.
-      + exact (p y i).
-      + exact (q y i).
-    - intros [p q]; strip_truncations; split; apply tr; intros y i.
-      + exact (p y i).
-      + exact (q y i).
-  Defined.
-  
-End IdealLemmas.
+    - apply ideal_in_zero.
+    - by apply ideal_in_plus_negate. }
+  apply ideal_sum_smallest.
+  1,2: apply ideal_product_subset_pres_l.
+  1: apply ideal_sum_subset_l.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Ideal sums are commutative *)
+Lemma ideal_sum_comm {R : Ring} (I J : Ideal R) : I + J ↔ J + I.
+Proof.
+  apply ideal_subset_antisymm; apply ideal_sum_smallest.
+  1,3: apply ideal_sum_subset_r.
+  1,2: apply ideal_sum_subset_l.
+Defined.
+
+(** Zero ideal is left additive identity. *) 
+Lemma ideal_sum_zero_l {R : Ring} I : ideal_zero R + I ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: apply ideal_sum_smallest.
+  1: apply ideal_zero_subset.
+  1: reflexivity.
+  apply ideal_sum_subset_r.
+Defined.
+
+(** Zero ideal is right additive identity. *)
+Lemma ideal_sum_zero_r {R : Ring} I : I + ideal_zero R ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: apply ideal_sum_smallest.
+  1: reflexivity.
+  1: apply ideal_zero_subset.
+  apply ideal_sum_subset_l.
+Defined.
+
+(** Unit ideal is left multiplicative identity. *)
+Lemma ideal_product_unit_l {R : Ring} I : ideal_unit R ⋅ I ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: apply ideal_product_subset_r.
+  intros r p.
+  rewrite <- rng_mult_one_l.
+  by apply tr, sgt_in, ipn_in.
+Defined.
+
+(** Unit ideal is right multiplicative identity. *)
+Lemma ideal_product_unit_r {R : Ring} I : I ⋅ ideal_unit R ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: apply ideal_product_subset_l.
+  intros r p.
+  rewrite <- rng_mult_one_r.
+  by apply tr, sgt_in, ipn_in.
+Defined.
+
+(** Intersecting with unit ideal on the left does nothing. *)
+Lemma ideal_intresection_unit_l {R : Ring} I : ideal_unit R ∩ I ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: apply ideal_intersection_subset_r.
+  apply ideal_intersection_subset.
+  1: apply ideal_unit_subset.
+  reflexivity.
+Defined.
+
+(** Intersecting with unit ideal on right does nothing. *)
+Lemma ideal_intersection_unit_r {R : Ring} I : I ∩ ideal_unit R ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  1: apply ideal_intersection_subset_l.
+  apply ideal_intersection_subset.
+  1: reflexivity.
+  apply ideal_unit_subset.
+Defined.
+
+(** Product of intersection and sum is subset of sum of products *)
+Lemma ideal_product_intersection_sum_subset {R : Ring} (I J : Ideal R)
+  : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
+Proof.
+  etransitivity.
+  1: rapply ideal_dist_l.
+  etransitivity.
+  1: rapply ideal_sum_subset_pres_r.
+  1: rapply ideal_product_subset_pres_l.
+  1: apply ideal_intersection_subset_l.
+  etransitivity.
+  1: rapply ideal_sum_subset_pres_l.
+  1: rapply ideal_product_subset_pres_l.
+  1: apply ideal_intersection_subset_r.
+  rapply ideal_sum_comm.
+Defined.
+
+(** Ideals are subsets of their ideal quotients *)
+Lemma ideal_quotient_subset {R : Ring} (I J : Ideal R) : I ⊆ (I :: J).
+Proof.
+  intros x i; split; apply tr; intros r j; cbn.
+  - by rapply isrightideal.
+  - by rapply isleftideal.
+Defined.
+
+(** If J divides I then the ideal quotient of J by I is trivial. *)
+Lemma ideal_quotient_trivial {R : Ring} (I J : Ideal R)
+  : I ⊆ J -> J :: I ↔ ideal_unit R.
+Proof.
+  intros p.
+  apply ideal_subset_antisymm.
+  1: cbv; trivial.
+  intros r _; split; apply tr; intros x q; cbn.
+  - by apply isleftideal, p. 
+  - rapply isrightideal.
+    by apply p.
+Defined.
+
+(** The ideal quotient of I by unit is I. *)
+Lemma ideal_quotient_unit_bottom {R : Ring} (I : Ideal R)
+  : (I :: ideal_unit R) ↔ I.
+Proof.
+  apply ideal_subset_antisymm.
+  - intros r [p q].
+    strip_truncations.
+    rewrite <- rng_mult_one_r.
+    exact (p ring_one tt).
+  - apply ideal_quotient_subset.
+Defined.
+
+(** The ideal quotient of unit by I is unit. *)
+Lemma ideal_quotient_unit_top {R : Ring} (I : Ideal R)
+  : (ideal_unit R :: I) ↔ ideal_unit R.
+Proof.
+  split.
+  - cbn; trivial.
+  - intros ?; split; apply tr;
+    cbn; split; trivial. 
+Defined.
+
+(** The ideal quotient by a sum is an intersection of ideal quotients. *)
+Lemma ideal_quotient_sum {R : Ring} (I J K : Ideal R)
+  : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
+Proof.
+  apply ideal_subset_antisymm.
+  { intros r [p q]; strip_truncations; split; split; apply tr; intros x jk.
+    - by rapply p; rapply ideal_sum_subset_l.
+    - by rapply q; rapply ideal_sum_subset_l.
+    - by rapply p; rapply ideal_sum_subset_r.
+    - by rapply q; rapply ideal_sum_subset_r. }
+  intros r [[p q] [u v]]; strip_truncations; split; apply tr;
+  intros x jk; strip_truncations.
+  - induction jk as [? [] | | ? ? ? ? ? ? ].
+    + by apply p.
+    + by apply u.
+    + apply u, ideal_in_zero.
+    + rewrite rng_dist_l.
+      rewrite rng_mult_negate_r.
+      by apply ideal_in_plus_negate.
+  - induction jk as [? [] | | ? ? ? ? ? ? ].
+    + by apply q.
+    + by apply v.
+    + apply v, ideal_in_zero.
+    + change (I ((g - h) * r)). 
+      rewrite rng_dist_r.
+      rewrite rng_mult_negate_l.
+      by apply ideal_in_plus_negate.
+Defined.
+
+(** Ideal quotients distribute over intersections. *)
+Lemma ideal_quotient_intersection {R : Ring} (I J K : Ideal R)
+  : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
+Proof.
+  apply ideal_subset_antisymm.
+  - intros r [p q]; strip_truncations; split; split; apply tr; intros x k.
+    1,3: by apply p.
+    1,2: by apply q.
+  - intros r [[p q] [u v]].
+    strip_truncations; split; apply tr; intros x k; split.
+    + by apply p.
+    + by apply u.
+    + by apply q.
+    + by apply v.
+Defined.
+
+(** Annihilators reverse the order of inclusion. *)
+Lemma ideal_annihilator_subset {R : Ring} (I J : Ideal R)
+  : I ⊆ J -> Ann J ⊆ Ann I.
+Proof.
+  intros p x [q q']; hnf in q, q'; strip_truncations;
+    split; apply tr; intros y i.
+  - by apply q, p.
+  - by apply q', p.
+Defined.
+
+(** The annihilator of an ideal is equal to a quotient of zero. *)
+Lemma ideal_annihilator_zero_quotient {R : Ring} (I : Ideal R)
+  : Ann I ↔ ideal_zero R :: I.
+Proof.
+  intros x; split.
+  - intros [p q]; strip_truncations; split; apply tr; intros y i.
+    + exact (p y i).
+    + exact (q y i).
+  - intros [p q]; strip_truncations; split; apply tr; intros y i.
+    + exact (p y i).
+    + exact (q y i).
+Defined.
 
 (** TODO: Maximal ideals *)
 (** TODO: Principal ideal *)

From f6997e2aa4f57f7ed937c1092a92c28c36ac5617 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 7 Nov 2024 19:06:50 +0000
Subject: [PATCH 03/11] deduplicate opposite argument in ideals for
 ideal_produc_assoc

We show that the opposite of product ideals is the opposite of the
reverse product. This allows us to deduplicate the argument occuring in
ideal_product_assoc.

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 204 ++++++++++++++++++++-------------
 1 file changed, 124 insertions(+), 80 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index d24a439bb3a..cc559f2d715 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -53,7 +53,7 @@ Definition issig_LeftIdeal (R : Ring) : _ <~> LeftIdeal R := ltac:(issig).
 (** A right ideal of a ring [R] is a subgroup [I] of [R] which is closed under right multiplication. *)
 Definition RightIdeal (R : Ring) := LeftIdeal (rng_op R).
 
-Global Instance isrightdeal_rightideal {R} (I : RightIdeal R)
+Global Instance isrightideal_rightideal {R} (I : RightIdeal R)
   : IsRightIdeal (R:=R) I
   := leftideal_isleftideal _ I.
 
@@ -76,6 +76,12 @@ Definition ideal_op (R : Ring) : Ideal R -> Ideal (rng_op R)
   := fun I => Build_Ideal (rng_op R) I _.
 Coercion ideal_op : Ideal >-> Ideal.
 
+Definition rightideal_op (R : Ring) : LeftIdeal R -> RightIdeal (rng_op R)
+  := fun I => Build_RightIdeal (rng_op R) I _.
+
+Definition leftideal_op (R : Ring) : RightIdeal R -> LeftIdeal (rng_op R)
+  := fun I => Build_LeftIdeal (rng_op R) I _.
+
 (** *** Truncatedness properties *)
 
 Section IdealTrunc.
@@ -139,6 +145,80 @@ Section IdealElements.
   Definition ideal_in_plus_r : I (a + b) -> I a -> I b := subgroup_in_op_r I a b.
 End IdealElements.
 
+(** *** Ideal equality *)
+
+(** Classically, set based equality suffices for ideals. Since we are talking about predicates, we use pointwise iffs. This can of course be shown to be equivalent to the identity type. *)
+Definition ideal_eq {R : Ring} (I J : Subgroup R) := forall x, I x <-> J x.
+
+(** With univalence we can characterize equality of ideals. *)
+Lemma equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R} : ideal_eq I J <~> I = J.
+Proof.
+  refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _).
+  refine (equiv_path_sigma_hprop _ _ oE _).
+  rapply equiv_path_subgroup'.
+Defined.
+
+(** Under funext, ideal equiality is a proposition. *)
+Global Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
+  : IsHProp (ideal_eq I J) := _.
+
+(** Ideal equality is reflexive. *)
+Global Instance reflexive_ideal_eq {R : Ring} : Reflexive (@ideal_eq R).
+Proof.
+  intros I x; by split.
+Defined.
+
+(** Ideal equality is symmetric. *)
+Global Instance symmetric_ideal_eq {R : Ring} : Symmetric (@ideal_eq R).
+Proof.
+  intros I J p x; specialize (p x); by symmetry.
+Defined.
+
+(** Ideal equality is transitive. *)
+Global Instance transitive_ideal_eq {R : Ring} : Transitive (@ideal_eq R).
+Proof.
+  intros I J K p q x; specialize (p x); specialize (q x); by transitivity (J x).
+Defined.
+
+(** *** Subset relation on ideals *)
+
+(** We define the subset relation on ideals in the usual way: *)
+Definition ideal_subset {R : Ring} (I J : Subgroup R) := (forall x, I x -> J x).
+
+(** The subset relation is reflexive. *)
+Global Instance reflexive_ideal_subset {R : Ring} : Reflexive (@ideal_subset R)
+  := fun _ _ => idmap.
+
+(** The subset relation is transitive. *)
+Global Instance transitive_ideal_subset {R : Ring} : Transitive (@ideal_subset R).
+Proof.
+  intros x y z p q a.
+  exact (q a o p a).
+Defined.
+
+(** We can coerce equality to the subset relation, since equality is defined to be the subset relation in each direction. *)
+Coercion ideal_eq_subset {R : Ring} {I J : Subgroup R} : ideal_eq I J -> ideal_subset I J.
+Proof.
+  intros f x; apply f.
+Defined.
+
+(** *** Left and right ideals are invariant under ideal equality *)
+
+(** Left ideals are invariant under ideal equality. *)
+Definition isleftideal_eq {R : Ring} (I J : Subgroup R) (p : ideal_eq I J)
+  : IsLeftIdeal I -> IsLeftIdeal J.
+Proof.
+  intros i r x j.
+  apply p in j.
+  apply p.
+  by apply i.
+Defined.
+
+(** Right ideals are invariant under ideal equality. *)
+Definition isrightideal_eq {R : Ring} (I J : Subgroup R) (p : ideal_eq I J)
+  : IsRightIdeal I -> IsRightIdeal J
+  := isleftideal_eq (R := rng_op R) I J p.
+
 (** ** Constructions of ideals *)
 
 (** *** Zero Ideal *)
@@ -295,6 +375,13 @@ Inductive ideal_product_naive_type {R : Ring} (I J : Subgroup R) : R -> Type :=
 Definition ideal_product_type {R : Ring} (I J : Subgroup R) : Subgroup R
   := subgroup_generated (G := R) (ideal_product_naive_type I J). 
 
+(** The product ideal swapped is just the product ideal of the opposite ring. *)
+Definition ideal_product_type_op {R : Ring} (I J : Subgroup R)
+  : ideal_eq (ideal_product_type (R:=R) I J) (ideal_product_type (R:=rng_op R) J I).
+Proof.
+  intros x; split; rapply (functor_subgroup_generated _ _ (Id _)); intros r []; by nrapply ipn_in.
+Defined.
+
 (** The product of left ideals is a left ideal. *)
 Global Instance isleftideal_ideal_product_type {R : Ring} (I J : Subgroup R)
   `{IsLeftIdeal R I, IsLeftIdeal R J}
@@ -313,12 +400,9 @@ Global Instance isrightideal_ideal_product_type {R : Ring} (I J : Subgroup R)
   `{IsRightIdeal R I, IsRightIdeal R J}
   : IsRightIdeal (ideal_product_type I J).
 Proof.
-  intro r.
-  nrapply (functor_subgroup_generated _ _ (grp_homo_rng_right_mult (R:=R) r)).
-  intros s [s1 s2 p1 p2]; cbn.
-  rewrite <- simple_associativity.
-  nrefine (ipn_in I J s1 (s2 * r) p1 _).
-  by apply isrightideal.
+  nrapply isrightideal_eq.
+  1: symmetry; rapply ideal_product_type_op.
+  by apply isleftideal_ideal_product_type.
 Defined.
 
 (** The product of ideals is an ideal. *)
@@ -337,6 +421,16 @@ Definition rightideal_product {R : Ring}
   : RightIdeal R -> RightIdeal R -> RightIdeal R
   := leftideal_product.
 
+Definition leftideal_product_op {R : Ring} (I J : RightIdeal R)
+  : leftideal_product (leftideal_op R I) (leftideal_op R J)
+    = rightideal_product I J
+  := idpath.
+
+Definition rightideal_product_op {R : Ring} (I J : LeftIdeal R)
+  : rightideal_product (rightideal_op R I) (rightideal_op R J)
+    = leftideal_product I J
+  := idpath.
+
 (** Product of ideals. *)
 Definition ideal_product {R : Ring}
   : Ideal R -> Ideal R -> Ideal R
@@ -471,63 +565,6 @@ Defined.
 Definition ideal_principal {R : Ring} (x : R) : Ideal R
   := ideal_generated (fun r => x = r).
 
-(** *** Ideal equality *)
-
-(** Classically, set based equality suffices for ideals. Since we are talking about predicates, we use pointwise iffs. This can of course be shown to be equivalent to the identity type. *)
-Definition ideal_eq {R : Ring} (I J : Subgroup R) := forall x, I x <-> J x.
-
-(** With univalence we can characterize equality of ideals. *)
-Lemma equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R} : ideal_eq I J <~> I = J.
-Proof.
-  refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _).
-  refine (equiv_path_sigma_hprop _ _ oE _).
-  rapply equiv_path_subgroup'.
-Defined.
-
-(** Under funext, ideal equiality is a proposition. *)
-Global Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
-  : IsHProp (ideal_eq I J) := _.
-
-(** Ideal equality is reflexive. *)
-Global Instance reflexive_ideal_eq {R : Ring} : Reflexive (@ideal_eq R).
-Proof.
-  intros I x; by split.
-Defined.
-
-(** Ideal equality is symmetric. *)
-Global Instance symmetric_ideal_eq {R : Ring} : Symmetric (@ideal_eq R).
-Proof.
-  intros I J p x; specialize (p x); by symmetry.
-Defined.
-
-(** Ideal equality is transitive. *)
-Global Instance transitive_ideal_eq {R : Ring} : Transitive (@ideal_eq R).
-Proof.
-  intros I J K p q x; specialize (p x); specialize (q x); by transitivity (J x).
-Defined.
-
-(** *** Subset relation on ideals *)
-
-(** We define the subset relation on ideals in the usual way: *)
-Definition ideal_subset {R : Ring} (I J : Subgroup R) := (forall x, I x -> J x).
-
-(** The subset relation is reflexive. *)
-Global Instance reflexive_ideal_subset {R : Ring} : Reflexive (@ideal_subset R)
-  := fun _ _ => idmap.
-
-(** The subset relation is transitive. *)
-Global Instance transitive_ideal_subset {R : Ring} : Transitive (@ideal_subset R).
-Proof.
-  intros x y z p q a.
-  exact (q a o p a).
-Defined.
-
-(** We can coerce equality to the subset relation, since equality is defined to be the subset relation in each direction. *)
-Coercion ideal_eq_subset {R : Ring} {I J : Subgroup R} : ideal_eq I J -> ideal_subset I J.
-Proof.
-  intros f x; apply f.
-Defined.
-
 (** *** Quotient (a.k.a colon) ideals *)
 
 (** The definitions here are not entirely standard, but will become so when considering only commutative rings. For the non-commutative case there isn't a lot written about ideal quotients. *)
@@ -903,12 +940,21 @@ Proof.
   + by apply ideal_in_plus_negate.
 Defined.
 
+(** The product of opposite ideals is the opposite of the reversed product. *)
+Definition ideal_product_op {R : Ring} (I J : Ideal R)
+  : (ideal_op R I) ⋅ (ideal_op R J)
+    ↔ ideal_op R (J ⋅ I).
+Proof.
+  rapply ideal_product_type_op.
+Defined.
+
 (** The product of ideals is an associative operation. *)
 Lemma ideal_product_assoc {R : Ring} (I J K : Ideal R)
   : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
 Proof.
-  snrapply ideal_subset_antisymm.
-  - intros x.
+  assert (f : forall (R : Ring) (I J K : Ideal R), I ⋅ (J ⋅ K) ⊆ (I ⋅ J) ⋅ K).
+  - clear R I J K; intros R I J K.
+    intros x.
     apply Trunc_rec. 
     intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
     + strip_truncations.
@@ -921,19 +967,16 @@ Proof.
         by apply ideal_in_plus_negate.
     + apply ideal_in_zero.
     + by apply ideal_in_plus_negate.
-  - intros x.
-    apply Trunc_rec.
-    intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
-    + strip_truncations.
-      induction p as [t [y w r s] | | t k p1 IHp1 p2 IHp2].
-      * rewrite <- rng_mult_assoc.
-        by apply tr, sgt_in, ipn_in; [ | apply tr, sgt_in, ipn_in ].
-      * rewrite rng_mult_zero_l.
-        apply ideal_in_zero.
-      * rewrite rng_dist_r_negate.
-        by apply ideal_in_plus_negate.
-    + apply ideal_in_zero.
-    + by apply ideal_in_plus_negate.
+  - apply ideal_subset_antisymm; only 1: apply f.
+    intros x i.
+    apply ideal_product_op.
+    nrapply (ideal_product_subset_pres_l (R:=rng_op R)).
+    1: rapply ideal_product_op.
+    apply f.
+    apply (ideal_product_op (R:=rng_op R)).
+    nrapply (ideal_product_subset_pres_l (R:=R)).
+    1: rapply (ideal_product_op (R:=rng_op R)).
+    exact i.
 Defined.
 
 (** Products of ideals are subsets of their intersection. *)
@@ -957,7 +1000,8 @@ Proof.
 Defined.
 
 (** Ideals absorb themselves under sum. *)
-Lemma ideal_sum_self {R : Ring} (I : Ideal R) : I + I ↔ I.
+Lemma ideal_sum_self {R : Ring} (I : Ideal R)
+  : I + I ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: by rapply ideal_sum_smallest.

From 5f3d2b531f284ae656f38b13186952ecdec25651 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 18 Nov 2024 11:51:35 +0000
Subject: [PATCH 04/11] change Lemma to Definition

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 80 +++++++++++++++++-----------------
 1 file changed, 40 insertions(+), 40 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index cc559f2d715..a7c941f13c0 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -151,7 +151,7 @@ End IdealElements.
 Definition ideal_eq {R : Ring} (I J : Subgroup R) := forall x, I x <-> J x.
 
 (** With univalence we can characterize equality of ideals. *)
-Lemma equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R} : ideal_eq I J <~> I = J.
+Definition equiv_path_ideal `{Univalence} {R : Ring} {I J : Ideal R} : ideal_eq I J <~> I = J.
 Proof.
   refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _).
   refine (equiv_path_sigma_hprop _ _ oE _).
@@ -759,7 +759,7 @@ Proof.
     exact _.
 Defined.
 
-Lemma equiv_coprime_sum `{Funext} {R : Ring} (I J : Ideal R)
+Definition equiv_coprime_sum `{Funext} {R : Ring} (I J : Ideal R)
   : Coprime I J
   <~> hexists (fun '(((i ; p) , (j ; q)) : sig I * sig J)
       => i + j = ring_one).
@@ -828,48 +828,48 @@ Module Import Notation.
   Notation Ann := ideal_annihilator.
 End Notation.
 
-(** *** Ideal lemmas *)
+(** *** Ideal Lemmas *)
 
 (** Subset relation is antisymmetric. *)
-Lemma ideal_subset_antisymm {R : Ring} (I J : Subgroup R)
+Definition ideal_subset_antisymm {R : Ring} (I J : Subgroup R)
   : I ⊆ J -> J ⊆ I -> I ↔ J.
 Proof.
   intros p q x; split; by revert x.
 Defined.
 
 (** The zero ideal is contained in all ideals. *)
-Lemma ideal_zero_subset {R : Ring} (I : Subgroup R) : ideal_zero R ⊆ I.
+Definition ideal_zero_subset {R : Ring} (I : Subgroup R) : ideal_zero R ⊆ I.
 Proof.
   intros x p; rewrite p; apply ideal_in_zero.
 Defined.
 
 (** The unit ideal contains all ideals. *)
-Lemma ideal_unit_subset {R : Ring} (I : Subgroup R) : I ⊆ ideal_unit R.
+Definition ideal_unit_subset {R : Ring} (I : Subgroup R) : I ⊆ ideal_unit R.
 Proof.
   hnf; cbn; trivial.
 Defined.
 
 (** Intersection includes into the left *)
-Lemma ideal_intersection_subset_l {R : Ring} (I J : Ideal R) : I ∩ J ⊆ I.
+Definition ideal_intersection_subset_l {R : Ring} (I J : Ideal R) : I ∩ J ⊆ I.
 Proof.
   intro; exact fst.
 Defined.
 
 (** Intersection includes into the right *)
-Lemma ideal_intersection_subset_r {R : Ring} (I J : Ideal R) : I ∩ J ⊆ J.
+Definition ideal_intersection_subset_r {R : Ring} (I J : Ideal R) : I ∩ J ⊆ J.
 Proof.
   intro; exact snd.
 Defined.
 
 (** Subsets of intersections *)
-Lemma ideal_intersection_subset {R : Ring} (I J K : Ideal R)
+Definition ideal_intersection_subset {R : Ring} (I J K : Ideal R)
   : K ⊆ I -> K ⊆ J -> K ⊆ I ∩ J.
 Proof.
   intros p q x r; specialize (p x r); specialize (q x r); by split.
 Defined.
 
 (** Ideals include into their sum on the left *)
-Lemma ideal_sum_subset_l {R : Ring} (I J : Ideal R) : I ⊆ (I + J).
+Definition ideal_sum_subset_l {R : Ring} (I J : Ideal R) : I ⊆ (I + J).
 Proof.
   intros x p.
   apply tr, sgt_in.
@@ -877,7 +877,7 @@ Proof.
 Defined.
 
 (** Ideals include into their sum on the right *)
-Lemma ideal_sum_subset_r {R : Ring} (I J : Ideal R) : J ⊆ (I + J).
+Definition ideal_sum_subset_r {R : Ring} (I J : Ideal R) : J ⊆ (I + J).
 Proof.
   intros x p.
   apply tr, sgt_in.
@@ -887,7 +887,7 @@ Defined.
 #[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
 
 (** Products of ideals are included in their left factor *)
-Lemma ideal_product_subset_l {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ I.
+Definition ideal_product_subset_l {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ I.
 Proof.
   intros r p.
   strip_truncations.
@@ -899,7 +899,7 @@ Proof.
 Defined.
 
 (** Products of ideals are included in their right factor. *)
-Lemma ideal_product_subset_r {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ J.
+Definition ideal_product_subset_r {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ J.
 Proof.
   intros r p.
   strip_truncations.
@@ -911,7 +911,7 @@ Proof.
 Defined.
 
 (** Products of ideals preserve subsets on the left *)
-Lemma ideal_product_subset_pres_l {R : Ring} (I J K : Ideal R)
+Definition ideal_product_subset_pres_l {R : Ring} (I J K : Ideal R)
   : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
 Proof.
   intros p r q.
@@ -926,7 +926,7 @@ Proof.
 Defined.
 
 (** Products of ideals preserve subsets on the right *)
-Lemma ideal_product_subset_pres_r {R : Ring} (I J K : Ideal R)
+Definition ideal_product_subset_pres_r {R : Ring} (I J K : Ideal R)
   : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
 Proof.
   intros p r q.
@@ -949,7 +949,7 @@ Proof.
 Defined.
 
 (** The product of ideals is an associative operation. *)
-Lemma ideal_product_assoc {R : Ring} (I J K : Ideal R)
+Definition ideal_product_assoc {R : Ring} (I J K : Ideal R)
   : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
 Proof.
   assert (f : forall (R : Ring) (I J K : Ideal R), I ⋅ (J ⋅ K) ⊆ (I ⋅ J) ⋅ K).
@@ -980,7 +980,7 @@ Proof.
 Defined.
 
 (** Products of ideals are subsets of their intersection. *)
-Lemma ideal_product_subset_intersection {R : Ring} (I J : Ideal R)
+Definition ideal_product_subset_intersection {R : Ring} (I J : Ideal R)
   : I ⋅ J ⊆ I ∩ J.
 Proof.
   apply ideal_intersection_subset.
@@ -989,7 +989,7 @@ Proof.
 Defined.
 
 (** Sums of ideals are the smallest ideal containing the summands. *)
-Lemma ideal_sum_smallest {R : Ring} (I J K : Ideal R)
+Definition ideal_sum_smallest {R : Ring} (I J K : Ideal R)
   : I ⊆ K -> J ⊆ K -> (I + J) ⊆ K.
 Proof.
   intros p q.
@@ -1000,7 +1000,7 @@ Proof.
 Defined.
 
 (** Ideals absorb themselves under sum. *)
-Lemma ideal_sum_self {R : Ring} (I : Ideal R)
+Definition ideal_sum_self {R : Ring} (I : Ideal R)
   : I + I ↔ I.
 Proof.
   apply ideal_subset_antisymm.
@@ -1009,7 +1009,7 @@ Proof.
 Defined.
 
 (** Sums preserve inclusions in the left summand. *)
-Lemma ideal_sum_subset_pres_l {R : Ring} (I J K : Ideal R)
+Definition ideal_sum_subset_pres_l {R : Ring} (I J K : Ideal R)
   : I ⊆ J -> (I + K) ⊆ (J + K).
 Proof.
   intros p.
@@ -1021,7 +1021,7 @@ Proof.
 Defined.
 
 (** Sums preserve inclusions in the right summand. *)
-Lemma ideal_sum_subset_pres_r {R : Ring} (I J K : Ideal R)
+Definition ideal_sum_subset_pres_r {R : Ring} (I J K : Ideal R)
   : I ⊆ J -> (K + I) ⊆ (K + J).
 Proof.
   intros p.
@@ -1034,7 +1034,7 @@ Defined.
 
 (** Products left distribute over sums *)
 (** Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
-Lemma ideal_dist_l {R : Ring} (I J K : Ideal R)
+Definition ideal_dist_l {R : Ring} (I J K : Ideal R)
   : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
 Proof.
   (** We split into two directions. *)
@@ -1058,7 +1058,7 @@ Proof.
         by apply ideal_in_plus_negate.
     - apply ideal_in_zero.
     - by apply ideal_in_plus_negate. }
-  (** This is the easy direction which can use previous lemmas. *)
+  (** This is the easy direction which can use previous Definitions. *)
   apply ideal_sum_smallest.
   1,2: apply ideal_product_subset_pres_r.
   1: apply ideal_sum_subset_l.
@@ -1067,7 +1067,7 @@ Defined.
 
 (** Products distribute over sums on the right. *)
 (** The proof is very similar to the left version *)
-Lemma ideal_dist_r {R : Ring} (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
+Definition ideal_dist_r {R : Ring} (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
 Proof.
   apply ideal_subset_antisymm.
   { intros r p.
@@ -1095,7 +1095,7 @@ Proof.
 Defined.
 
 (** Ideal sums are commutative *)
-Lemma ideal_sum_comm {R : Ring} (I J : Ideal R) : I + J ↔ J + I.
+Definition ideal_sum_comm {R : Ring} (I J : Ideal R) : I + J ↔ J + I.
 Proof.
   apply ideal_subset_antisymm; apply ideal_sum_smallest.
   1,3: apply ideal_sum_subset_r.
@@ -1103,7 +1103,7 @@ Proof.
 Defined.
 
 (** Zero ideal is left additive identity. *) 
-Lemma ideal_sum_zero_l {R : Ring} I : ideal_zero R + I ↔ I.
+Definition ideal_sum_zero_l {R : Ring} I : ideal_zero R + I ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: apply ideal_sum_smallest.
@@ -1113,7 +1113,7 @@ Proof.
 Defined.
 
 (** Zero ideal is right additive identity. *)
-Lemma ideal_sum_zero_r {R : Ring} I : I + ideal_zero R ↔ I.
+Definition ideal_sum_zero_r {R : Ring} I : I + ideal_zero R ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: apply ideal_sum_smallest.
@@ -1123,7 +1123,7 @@ Proof.
 Defined.
 
 (** Unit ideal is left multiplicative identity. *)
-Lemma ideal_product_unit_l {R : Ring} I : ideal_unit R ⋅ I ↔ I.
+Definition ideal_product_unit_l {R : Ring} I : ideal_unit R ⋅ I ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: apply ideal_product_subset_r.
@@ -1133,7 +1133,7 @@ Proof.
 Defined.
 
 (** Unit ideal is right multiplicative identity. *)
-Lemma ideal_product_unit_r {R : Ring} I : I ⋅ ideal_unit R ↔ I.
+Definition ideal_product_unit_r {R : Ring} I : I ⋅ ideal_unit R ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: apply ideal_product_subset_l.
@@ -1143,7 +1143,7 @@ Proof.
 Defined.
 
 (** Intersecting with unit ideal on the left does nothing. *)
-Lemma ideal_intresection_unit_l {R : Ring} I : ideal_unit R ∩ I ↔ I.
+Definition ideal_intresection_unit_l {R : Ring} I : ideal_unit R ∩ I ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: apply ideal_intersection_subset_r.
@@ -1153,7 +1153,7 @@ Proof.
 Defined.
 
 (** Intersecting with unit ideal on right does nothing. *)
-Lemma ideal_intersection_unit_r {R : Ring} I : I ∩ ideal_unit R ↔ I.
+Definition ideal_intersection_unit_r {R : Ring} I : I ∩ ideal_unit R ↔ I.
 Proof.
   apply ideal_subset_antisymm.
   1: apply ideal_intersection_subset_l.
@@ -1163,7 +1163,7 @@ Proof.
 Defined.
 
 (** Product of intersection and sum is subset of sum of products *)
-Lemma ideal_product_intersection_sum_subset {R : Ring} (I J : Ideal R)
+Definition ideal_product_intersection_sum_subset {R : Ring} (I J : Ideal R)
   : (I ∩ J) ⋅ (I + J) ⊆ (I ⋅ J + J ⋅ I).
 Proof.
   etransitivity.
@@ -1180,7 +1180,7 @@ Proof.
 Defined.
 
 (** Ideals are subsets of their ideal quotients *)
-Lemma ideal_quotient_subset {R : Ring} (I J : Ideal R) : I ⊆ (I :: J).
+Definition ideal_quotient_subset {R : Ring} (I J : Ideal R) : I ⊆ (I :: J).
 Proof.
   intros x i; split; apply tr; intros r j; cbn.
   - by rapply isrightideal.
@@ -1188,7 +1188,7 @@ Proof.
 Defined.
 
 (** If J divides I then the ideal quotient of J by I is trivial. *)
-Lemma ideal_quotient_trivial {R : Ring} (I J : Ideal R)
+Definition ideal_quotient_trivial {R : Ring} (I J : Ideal R)
   : I ⊆ J -> J :: I ↔ ideal_unit R.
 Proof.
   intros p.
@@ -1201,7 +1201,7 @@ Proof.
 Defined.
 
 (** The ideal quotient of I by unit is I. *)
-Lemma ideal_quotient_unit_bottom {R : Ring} (I : Ideal R)
+Definition ideal_quotient_unit_bottom {R : Ring} (I : Ideal R)
   : (I :: ideal_unit R) ↔ I.
 Proof.
   apply ideal_subset_antisymm.
@@ -1213,7 +1213,7 @@ Proof.
 Defined.
 
 (** The ideal quotient of unit by I is unit. *)
-Lemma ideal_quotient_unit_top {R : Ring} (I : Ideal R)
+Definition ideal_quotient_unit_top {R : Ring} (I : Ideal R)
   : (ideal_unit R :: I) ↔ ideal_unit R.
 Proof.
   split.
@@ -1223,7 +1223,7 @@ Proof.
 Defined.
 
 (** The ideal quotient by a sum is an intersection of ideal quotients. *)
-Lemma ideal_quotient_sum {R : Ring} (I J K : Ideal R)
+Definition ideal_quotient_sum {R : Ring} (I J K : Ideal R)
   : (I :: (J + K)) ↔ (I :: J) ∩ (I :: K).
 Proof.
   apply ideal_subset_antisymm.
@@ -1252,7 +1252,7 @@ Proof.
 Defined.
 
 (** Ideal quotients distribute over intersections. *)
-Lemma ideal_quotient_intersection {R : Ring} (I J K : Ideal R)
+Definition ideal_quotient_intersection {R : Ring} (I J K : Ideal R)
   : (I ∩ J :: K) ↔ (I :: K) ∩ (J :: K).
 Proof.
   apply ideal_subset_antisymm.
@@ -1268,7 +1268,7 @@ Proof.
 Defined.
 
 (** Annihilators reverse the order of inclusion. *)
-Lemma ideal_annihilator_subset {R : Ring} (I J : Ideal R)
+Definition ideal_annihilator_subset {R : Ring} (I J : Ideal R)
   : I ⊆ J -> Ann J ⊆ Ann I.
 Proof.
   intros p x [q q']; hnf in q, q'; strip_truncations;
@@ -1278,7 +1278,7 @@ Proof.
 Defined.
 
 (** The annihilator of an ideal is equal to a quotient of zero. *)
-Lemma ideal_annihilator_zero_quotient {R : Ring} (I : Ideal R)
+Definition ideal_annihilator_zero_quotient {R : Ring} (I : Ideal R)
   : Ann I ↔ ideal_zero R :: I.
 Proof.
   intros x; split.

From 0c5da333a8d3fd3e6e28a3d7d10af29cb2c09515 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 18 Nov 2024 11:53:31 +0000
Subject: [PATCH 05/11] fix typo

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index a7c941f13c0..fc4666b6581 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -158,7 +158,7 @@ Proof.
   rapply equiv_path_subgroup'.
 Defined.
 
-(** Under funext, ideal equiality is a proposition. *)
+(** Under funext, ideal equality is a proposition. *)
 Global Instance ishprop_ideal_eq `{Funext} {R : Ring} (I J : Ideal R)
   : IsHProp (ideal_eq I J) := _.
 

From d225245492c8ca1d2f5f4eb2363aa4f007835070 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 18 Nov 2024 11:55:50 +0000
Subject: [PATCH 06/11] make leftideal_op and rightideal_op into idmap

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index fc4666b6581..b9c4b5c0de1 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -77,10 +77,10 @@ Definition ideal_op (R : Ring) : Ideal R -> Ideal (rng_op R)
 Coercion ideal_op : Ideal >-> Ideal.
 
 Definition rightideal_op (R : Ring) : LeftIdeal R -> RightIdeal (rng_op R)
-  := fun I => Build_RightIdeal (rng_op R) I _.
+  := idmap.
 
 Definition leftideal_op (R : Ring) : RightIdeal R -> LeftIdeal (rng_op R)
-  := fun I => Build_LeftIdeal (rng_op R) I _.
+  := idmap.
 
 (** *** Truncatedness properties *)
 

From b1919ae52353ca1b071fedd490e6a75eb5e7d56d Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 18 Nov 2024 21:03:21 -0500
Subject: [PATCH 07/11] Subgroup: add subgroup_generated_subset_subgroup

(Also adds subgroup_preimage, which is already in master.)
---
 theories/Algebra/Groups/Subgroup.v | 42 +++++++++++++++++++++++-------
 1 file changed, 33 insertions(+), 9 deletions(-)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 7bab540f3a3..888c4457bfc 100644
--- a/theories/Algebra/Groups/Subgroup.v
+++ b/theories/Algebra/Groups/Subgroup.v
@@ -188,6 +188,22 @@ Proof.
   apply negate_mon_unit.
 Defined.
 
+(** The preimage of a subgroup under a group homomorphism is a subgroup. *)
+Definition subgroup_preimage {G H : Group} (f : G $-> H) (S : Subgroup H)
+  : Subgroup G.
+Proof.
+  snrapply Build_Subgroup'.
+  - exact (S o f).
+  - hnf; exact _.
+  - nrefine (transport S (grp_homo_unit f)^ _).
+    apply subgroup_in_unit.
+  - hnf; intros x y Sfx Sfy.
+    nrefine (transport S (grp_homo_op f _ _)^ _).
+    nrapply subgroup_in_op; only 1: assumption.
+    nrefine (transport S (grp_homo_inv f _)^ _).
+    by apply subgroup_in_inv.
+Defined.
+
 (** Every group is a (maximal) subgroup of itself *)
 Definition maximal_subgroup {G} : Subgroup G.
 Proof.
@@ -537,20 +553,28 @@ Definition subgroup_generated_gen_incl {G : Group} {X : G -> Type} (g : G) (H :
   : subgroup_generated X
   := (g; tr (sgt_in H)).
 
+(** If generators are contained in another subgroup [H], then the subgroup they generate is contained in [H]. *)
+Definition subgroup_generated_subset_subgroup {G : Group} (X : G -> Type)
+  (H : Subgroup G)
+  (gen_in : forall g, X g -> H g)
+  : forall g, subgroup_generated X g -> H g.
+Proof.
+  intro g.
+  rapply Trunc_rec.
+  intro p; induction p as [g i | | g h p1 IHp1 p2 IHp2].
+  - apply gen_in, i.
+  - apply issubgroup_in_unit.
+  - by apply issubgroup_in_op_inv.
+Defined.
+
 (** If [f : G $-> H] is a group homomorphism and [X] and [Y] are subsets of [G] and [H] such that [f] maps [X] into [Y], then [f] sends the subgroup generated by [X] into the subgroup generated by [Y]. *)
 Definition functor_subgroup_generated {G H : Group} (X : G -> Type) (Y : H -> Type)
   (f : G $-> H) (preserves : forall g, X g -> Y (f g))
   : forall g, subgroup_generated X g -> subgroup_generated Y (f g).
 Proof.
-  intro g.
-  apply Trunc_functor.
-  intro p.
-  induction p as [g i | | g h p1 IHp1 p2 IHp2].
-  - apply sgt_in, preserves, i.
-  - rewrite grp_homo_unit.
-    apply sgt_unit.
-  - rewrite grp_homo_op, grp_homo_inv.
-    by apply sgt_op.
+  apply (subgroup_generated_subset_subgroup X (subgroup_preimage f (subgroup_generated Y))).
+  intros g p; cbn.
+  apply tr, sgt_in, preserves, p.
 Defined.
 
 (** The product of two subgroups. *)

From 6ecda53eff44c017e5157b5c8a0287182c3772d8 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 18 Nov 2024 21:04:21 -0500
Subject: [PATCH 08/11] Ideal: use subgroup_generated_subset_subgroup and
 functor_subgroup_generated

---
 theories/Algebra/Rings/Ideal.v | 70 ++++++++++++----------------------
 1 file changed, 25 insertions(+), 45 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index b9c4b5c0de1..e3f0ba1c345 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -889,55 +889,41 @@ Defined.
 (** Products of ideals are included in their left factor *)
 Definition ideal_product_subset_l {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ I.
 Proof.
-  intros r p.
-  strip_truncations.
-  induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
-  + destruct i as [s t].
-    by rapply isrightideal.
-  + rapply ideal_in_zero.
-  + by rapply ideal_in_plus_negate.
+  nrapply subgroup_generated_subset_subgroup.
+  intros _ [].
+  by rapply isrightideal.
 Defined.
 
 (** Products of ideals are included in their right factor. *)
 Definition ideal_product_subset_r {R : Ring} (I J : Ideal R) : I ⋅ J ⊆ J.
 Proof.
-  intros r p.
-  strip_truncations.
-  induction p as [r i | | r s p1 IHp1 p2 IHp2 ].
-  + destruct i as [s t].
-    by apply isleftideal.
-  + rapply ideal_in_zero.
-  + by rapply ideal_in_plus_negate.
+  nrapply subgroup_generated_subset_subgroup.
+  intros _ [].
+  by rapply isleftideal.
 Defined.
 
 (** Products of ideals preserve subsets on the left *)
 Definition ideal_product_subset_pres_l {R : Ring} (I J K : Ideal R)
   : I ⊆ J -> I ⋅ K ⊆ J ⋅ K.
 Proof.
-  intros p r q.
-  strip_truncations.
-  induction q as [r i | | r s ].
-  + destruct i.
-    apply tr, sgt_in, ipn_in.
-    1: apply p.
-    1,2: assumption.
-  + apply ideal_in_zero.
-  + by apply ideal_in_plus_negate.
+  intros p.
+  rapply (functor_subgroup_generated _ _ (Id _)).
+  intros _ [].
+  apply ipn_in.
+  1: apply p.
+  1,2: assumption.
 Defined.
 
 (** Products of ideals preserve subsets on the right *)
 Definition ideal_product_subset_pres_r {R : Ring} (I J K : Ideal R)
   : I ⊆ J -> K ⋅ I ⊆ K ⋅ J.
 Proof.
-  intros p r q.
-  strip_truncations.
-  induction q as [r i | | r s ].
-  + destruct i.
-    apply tr, sgt_in, ipn_in.
-    2: apply p.
-    1,2: assumption.
-  + apply ideal_in_zero.
-  + by apply ideal_in_plus_negate.
+  intros p.
+  rapply (functor_subgroup_generated _ _ (Id _)).
+  intros _ [].
+  apply ipn_in.
+  2: apply p.
+  1,2: assumption.
 Defined.
 
 (** The product of opposite ideals is the opposite of the reversed product. *)
@@ -954,19 +940,13 @@ Definition ideal_product_assoc {R : Ring} (I J K : Ideal R)
 Proof.
   assert (f : forall (R : Ring) (I J K : Ideal R), I ⋅ (J ⋅ K) ⊆ (I ⋅ J) ⋅ K).
   - clear R I J K; intros R I J K.
-    intros x.
-    apply Trunc_rec. 
-    intros p; induction p as [g [y z p q] | | g h p1 IHp1 p2 IHp2].
-    + strip_truncations.
-      induction q as [t [z w r s] | | t k p1 IHp1 p2 IHp2].
-      * rewrite rng_mult_assoc.
-        by apply tr, sgt_in, ipn_in; [ apply tr, sgt_in, ipn_in | ].
-      * rewrite rng_mult_zero_r.
-        apply ideal_in_zero.
-      * rewrite rng_dist_l_negate.
-        by apply ideal_in_plus_negate.
-    + apply ideal_in_zero.
-    + by apply ideal_in_plus_negate.
+    nrapply subgroup_generated_subset_subgroup.
+    intros _ [r s IHr IHs].
+    revert IHs.
+    rapply (functor_subgroup_generated _ _ (grp_homo_rng_left_mult r)); clear s.
+    intros _ [s t IHs IHt]; cbn.
+    rewrite rng_mult_assoc.
+    by apply ipn_in; [ apply tr, sgt_in, ipn_in | ].
   - apply ideal_subset_antisymm; only 1: apply f.
     intros x i.
     apply ideal_product_op.

From f155213ed43366185167612f4823a88ba35c16df Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 18 Nov 2024 21:05:04 -0500
Subject: [PATCH 09/11] Ideal: add and use ideal_product_op_triple

---
 theories/Algebra/Rings/Ideal.v | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index e3f0ba1c345..73f617dde0e 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -934,6 +934,17 @@ Proof.
   rapply ideal_product_type_op.
 Defined.
 
+Definition ideal_product_op_triple {R : Ring} (I J K : Ideal R)
+  : ideal_op R ((K ⋅ J) ⋅ I)
+      ⊆ (ideal_op R I) ⋅ ((ideal_op R J) ⋅ (ideal_op R K)).
+Proof.
+  intros x i.
+  apply (ideal_product_op (R:=rng_op R)).
+  nrapply (ideal_product_subset_pres_l (R:=R)).
+  1: nrapply (ideal_product_op (R:=rng_op R)).
+  apply i.
+Defined.
+
 (** The product of ideals is an associative operation. *)
 Definition ideal_product_assoc {R : Ring} (I J K : Ideal R)
   : I ⋅ (J ⋅ K) ↔ (I ⋅ J) ⋅ K.
@@ -949,13 +960,9 @@ Proof.
     by apply ipn_in; [ apply tr, sgt_in, ipn_in | ].
   - apply ideal_subset_antisymm; only 1: apply f.
     intros x i.
-    apply ideal_product_op.
-    nrapply (ideal_product_subset_pres_l (R:=rng_op R)).
-    1: rapply ideal_product_op.
-    apply f.
-    apply (ideal_product_op (R:=rng_op R)).
-    nrapply (ideal_product_subset_pres_l (R:=R)).
-    1: rapply (ideal_product_op (R:=rng_op R)).
+    apply (ideal_product_op_triple (R:=rng_op R) I J K).
+    nrapply f.
+    apply ideal_product_op_triple.
     exact i.
 Defined.
 

From 8c17c5a32d68a8eb68862340fb4c9b098e64a566 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 19 Nov 2024 09:12:54 +0000
Subject: [PATCH 10/11] fix overzealous replacement

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 73f617dde0e..e7cd33103f5 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -1045,7 +1045,7 @@ Proof.
         by apply ideal_in_plus_negate.
     - apply ideal_in_zero.
     - by apply ideal_in_plus_negate. }
-  (** This is the easy direction which can use previous Definitions. *)
+  (** This is the easy direction which can use previous lemmas. *)
   apply ideal_sum_smallest.
   1,2: apply ideal_product_subset_pres_r.
   1: apply ideal_sum_subset_l.

From 5dac549a731d71b9f5dbca8a84d506dacc75dc6f Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 19 Nov 2024 12:12:19 +0000
Subject: [PATCH 11/11] prove ideal_dist_r in terms of ideal_dist_l

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Ideal.v | 63 +++++++++++++++++++---------------
 1 file changed, 36 insertions(+), 27 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index e7cd33103f5..19933246e52 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -1019,8 +1019,30 @@ Proof.
   apply ideal_sum_subset_r.
 Defined.
 
-(** Products left distribute over sums *)
-(** Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
+(** Sums preserve inclusions in both summands. *)
+Definition ideal_sum_subset_pres {R : Ring} (I J K L : Ideal R)
+  : I ⊆ J -> K ⊆ L -> (I + K) ⊆ (J + L).
+Proof.
+  intros p q.
+  transitivity (J + K).
+  1: by apply ideal_sum_subset_pres_l.
+  by apply ideal_sum_subset_pres_r.
+Defined.
+
+(** Sums preserve ideal equality in both summands. *)
+Definition ideal_sum_eq {R : Ring} (I J K L : Ideal R)
+  : I ↔ J -> K ↔ L -> (I + K) ↔ (J + L).
+Proof.
+  intros p q.
+  by apply ideal_subset_antisymm; apply ideal_sum_subset_pres; apply ideal_eq_subset.
+Defined.
+
+(** The sum of two opposite ideals is the opposite of their sum. *)
+Definition ideal_sum_op {R : Ring} (I J : Ideal R)
+  : ideal_op R I + ideal_op R J ↔ ideal_op R (I + J)
+  := reflexive_ideal_eq _.
+
+(** Products left distribute over sums. Note that this follows from left adjoints preserving colimits. The product of ideals is a functor whose right adjoint is the quotient ideal. *)
 Definition ideal_dist_l {R : Ring} (I J K : Ideal R)
   : I ⋅ (J + K) ↔ I ⋅ J + I ⋅ K.
 Proof.
@@ -1053,32 +1075,19 @@ Proof.
 Defined.
 
 (** Products distribute over sums on the right. *)
-(** The proof is very similar to the left version *)
-Definition ideal_dist_r {R : Ring} (I J K : Ideal R) : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
+Definition ideal_dist_r {R : Ring} (I J K : Ideal R)
+  : (I + J) ⋅ K ↔ I ⋅ K + J ⋅ K.
 Proof.
-  apply ideal_subset_antisymm.
-  { intros r p.
-    strip_truncations.
-    induction p as [ r i | | r s p1 IHp1 p2 IHp2].
-    - destruct i as [r s p q].
-      strip_truncations.
-      induction p as [ t k | | t k p1 IHp1 p2 IHp2 ].
-      + apply tr, sgt_in.
-        destruct k as [j | k].
-        * left; by apply tr, sgt_in, ipn_in.
-        * right; by apply tr, sgt_in, ipn_in.
-      + apply tr, sgt_in; left.
-        rewrite rng_mult_zero_l.
-        apply ideal_in_zero.
-      + rewrite rng_dist_r.
-        rewrite rng_mult_negate_l.
-        by apply ideal_in_plus_negate.
-    - apply ideal_in_zero.
-    - by apply ideal_in_plus_negate. }
-  apply ideal_sum_smallest.
-  1,2: apply ideal_product_subset_pres_l.
-  1: apply ideal_sum_subset_l.
-  apply ideal_sum_subset_r.
+  change I with (ideal_op _ (ideal_op R I)).
+  change J with (ideal_op _ (ideal_op R J)).
+  change K with (ideal_op _ (ideal_op R K)).
+  etransitivity.
+  2: rapply ideal_sum_eq; symmetry; apply (ideal_product_op (R:=rng_op R)).
+  etransitivity.
+  2: apply (ideal_dist_l (R:=rng_op R)).
+  etransitivity.
+  2: apply (ideal_product_op (R:=rng_op R)).
+  reflexivity.
 Defined.
 
 (** Ideal sums are commutative *)