From 48a77e34f580effdb89e6301c6cf683013fd3c6c Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 17 Sep 2024 23:12:25 +0200
Subject: [PATCH] subgroup and ideal preimage

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

<!-- ps-id: 55f3b1a6-ee1b-4c43-96b2-53a917e538d8 -->
---
 theories/Algebra/Groups/Subgroup.v | 16 +++++++++
 theories/Algebra/Rings/Ideal.v     | 52 ++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+)

diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
index 7bab540f3a3..75d84d2b641 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.
diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 160c1205786..827ca182ab2 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -1217,6 +1217,58 @@ Section IdealLemmas.
   
 End IdealLemmas.
 
+(** ** Preimage of ideals under ring homomorphisms *)
+
+(** The preimage of an ideal under a ring homomorphism is also itself an ideal. This is also known as the contraction of an ideal. *)
+
+Global Instance isleftideal_preimage {R S : Ring} (f : R $-> S)
+  (I : Subgroup S) `{IsLeftIdeal S I}
+  : IsLeftIdeal (subgroup_preimage f I).
+Proof.
+  intros r x Ifx.
+  nrefine (transport I (rng_homo_mult f _ _)^ _).
+  rapply isleftideal.
+  exact Ifx.
+Defined.
+
+Global Instance isrightideal_preimage {R S : Ring} (f : R $-> S)
+  (I : Subgroup S) `{IsRightIdeal S I}
+  : IsRightIdeal (subgroup_preimage f I)
+  := isleftideal_preimage (R:=rng_op R) (S:=rng_op S)
+      (fmap rng_op f) I.
+
+Global Instance isideal_preimage {R S : Ring} (f : R $-> S)
+  (I : Subgroup S) `{IsIdeal S I}
+  : IsIdeal (subgroup_preimage f I)
+  := {}.
+
+Definition ideal_preimage {R S : Ring} (f : R $-> S) (I : Ideal S)
+  : Ideal R
+  := Build_Ideal R (subgroup_preimage f I) _.
+
+(** ** Extensions of ideals *)
+
+(** The extension of an ideal under a ring homomorphism is the ideal generated by the image of the ideal. *)
+Definition ideal_extension {R S : Ring} (f : R $-> S) (I : Ideal R) : Ideal S
+  := ideal_generated (fun s => exists r, I r /\ f r = s).
+
+(** The extension of a preimage is always a subset of the original ideal. *)
+Definition ideal_subset_extension_preimage {R S : Ring} (f : R $-> S)
+  (I : Ideal S)
+  : ideal_extension f (ideal_preimage f I) ⊆ I.
+Proof.
+  intros x.
+  apply Trunc_rec.
+  intros y.
+  induction y.
+  + destruct x as [s [p q]].
+    destruct q; exact p.
+  + apply ideal_in_zero.
+  + by apply ideal_in_plus_negate.
+  + by rapply isleftideal.
+  + by rapply isrightideal.
+Defined.
+
 (** TODO: Maximal ideals *)
 (** TODO: Principal ideal *)
 (** TODO: Prime ideals *)