feat: add comap_map for sub(semi)ring, subalgebra, subfield and intermediate fields (#15193)

Generalizes `Subgroup.comap_map_eq`, `Subgroup.comap_map_eq_self`, `Subgroup.comap_map_eq_self_of_injective`, and `Subgroup.map_comap_eq`, `Subgroup.map_comap_eq_self`, `Subgroup.map_comap_eq_self_of_surjective`.

Author: acmepjz

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -1170,3 +1170,28 @@ theorem ext_on_codisjoint {φ ψ : F} {S T : Subalgebra R A} (hST : Codisjoint S
 end AlgHom
 
 end Equalizer
+
+section MapComap
+
+namespace Subalgebra
+
+variable {R A B : Type*} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B]
+
+theorem map_comap_eq (f : A →ₐ[R] B) (S : Subalgebra R B) : (S.comap f).map f = S ⊓ f.range :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+theorem map_comap_eq_self
+    {f : A →ₐ[R] B} {S : Subalgebra R B} (h : S ≤ f.range) : (S.comap f).map f = S := by
+  simpa only [inf_of_le_left h] using map_comap_eq f S
+
+theorem map_comap_eq_self_of_surjective
+    {f : A →ₐ[R] B} (hf : Function.Surjective f) (S : Subalgebra R B) : (S.comap f).map f = S :=
+  map_comap_eq_self <| by simp [(Algebra.range_top_iff_surjective f).2 hf]
+
+theorem comap_map_eq_self_of_injective
+    {f : A →ₐ[R] B} (hf : Function.Injective f) (S : Subalgebra R A) : (S.map f).comap f = S :=
+  SetLike.coe_injective (Set.preimage_image_eq _ hf)
+
+end Subalgebra
+
+end MapComap

Mathlib/Algebra/Field/Subfield.lean

@@ -840,3 +840,21 @@ theorem mem_closure_iff {s : Set K} {x} :
 end Commutative
 
 end Subfield
+
+namespace Subfield
+
+theorem map_comap_eq (f : K →+* L) (s : Subfield L) : (s.comap f).map f = s ⊓ f.fieldRange :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+theorem map_comap_eq_self
+    {f : K →+* L} {s : Subfield L} (h : s ≤ f.fieldRange) : (s.comap f).map f = s := by
+  simpa only [inf_of_le_left h] using map_comap_eq f s
+
+theorem map_comap_eq_self_of_surjective
+    {f : K →+* L} (hf : Function.Surjective f) (s : Subfield L) : (s.comap f).map f = s :=
+  SetLike.coe_injective (Set.image_preimage_eq _ hf)
+
+theorem comap_map (f : K →+* L) (s : Subfield K) : (s.map f).comap f = s :=
+  SetLike.coe_injective (Set.preimage_image_eq _ f.injective)
+
+end Subfield

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -1182,3 +1182,18 @@ namespace Nat
   exact fun n hn ↦ AddSubmonoid.add_mem _ hn <| subset_closure <| Set.mem_singleton _
 
 end Nat
+
+namespace Submonoid
+
+variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N]
+
+@[to_additive]
+theorem map_comap_eq (f : F) (S : Submonoid N) : (S.comap f).map f = S ⊓ MonoidHom.mrange f :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+@[to_additive]
+theorem map_comap_eq_self {f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) :
+    (S.comap f).map f = S := by
+  simpa only [inf_of_le_left h] using map_comap_eq f S
+
+end Submonoid

Mathlib/Algebra/Group/Subsemigroup/Operations.lean

@@ -772,3 +772,18 @@ def subsemigroupMap (e : M ≃* N) (S : Subsemigroup M) : S ≃* S.map (e : M 
     invFun := fun x => ⟨e.symm x, _⟩ }
 
 end MulEquiv
+
+namespace Subsemigroup
+
+variable [Mul M] [Mul N]
+
+@[to_additive]
+theorem map_comap_eq (f : M →ₙ* N) (S : Subsemigroup N) : (S.comap f).map f = S ⊓ f.srange :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+@[to_additive]
+theorem map_comap_eq_self {f : M →ₙ* N} {S : Subsemigroup N} (h : S ≤ f.srange) :
+    (S.comap f).map f = S := by
+  simpa only [inf_of_le_left h] using map_comap_eq f S
+
+end Subsemigroup

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -1286,3 +1286,41 @@ instance center.smulCommClass_right : SMulCommClass R (center R) R :=
 end Subring
 
 end Actions
+
+namespace Subring
+
+theorem map_comap_eq (f : R →+* S) (t : Subring S) : (t.comap f).map f = t ⊓ f.range :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+theorem map_comap_eq_self
+    {f : R →+* S} {t : Subring S} (h : t ≤ f.range) : (t.comap f).map f = t := by
+  simpa only [inf_of_le_left h] using Subring.map_comap_eq f t
+
+theorem map_comap_eq_self_of_surjective
+    {f : R →+* S} (hf : Function.Surjective f) (t : Subring S) : (t.comap f).map f = t :=
+  map_comap_eq_self <| by simp [hf]
+
+theorem comap_map_eq (f : R →+* S) (s : Subring R) :
+    (s.map f).comap f = s ⊔ closure (f ⁻¹' {0}) := by
+  apply le_antisymm
+  · intro x hx
+    rw [mem_comap, mem_map] at hx
+    obtain ⟨y, hy, hxy⟩ := hx
+    replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
+    rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]
+    exact Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)
+  · rw [← map_le_iff_le_comap, map_sup, f.map_closure]
+    apply le_of_eq
+    rw [sup_eq_left, closure_le]
+    exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)
+
+theorem comap_map_eq_self {f : R →+* S} {s : Subring R}
+    (h : f ⁻¹' {0} ⊆ s) : (s.map f).comap f = s := by
+  convert comap_map_eq f s
+  rwa [left_eq_sup, closure_le]
+
+theorem comap_map_eq_self_of_injective
+    {f : R →+* S} (hf : Function.Injective f) (s : Subring R) : (s.map f).comap f = s :=
+  SetLike.coe_injective (Set.preimage_image_eq _ hf)
+
+end Subring

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

@@ -1195,3 +1195,22 @@ def closureCommSemiringOfComm {s : Set R'} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a
 end Subsemiring
 
 end Actions
+
+namespace Subsemiring
+
+theorem map_comap_eq (f : R →+* S) (t : Subsemiring S) : (t.comap f).map f = t ⊓ f.rangeS :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+theorem map_comap_eq_self
+    {f : R →+* S} {t : Subsemiring S} (h : t ≤ f.rangeS) : (t.comap f).map f = t := by
+  simpa only [inf_of_le_left h] using map_comap_eq f t
+
+theorem map_comap_eq_self_of_surjective
+    {f : R →+* S} (hf : Function.Surjective f) (t : Subsemiring S) : (t.comap f).map f = t :=
+  map_comap_eq_self <| by simp [hf]
+
+theorem comap_map_eq_self_of_injective
+    {f : R →+* S} (hf : Function.Injective f) (s : Subsemiring R) : (s.map f).comap f = s :=
+  SetLike.coe_injective (Set.preimage_image_eq _ hf)
+
+end Subsemiring

Mathlib/FieldTheory/Adjoin.lean

@@ -1399,3 +1399,24 @@ theorem equivAdjoinSimple_symm_gen (pb : PowerBasis K L) :
   rw [equivAdjoinSimple, equivOfMinpoly_symm, equivOfMinpoly_gen, adjoin.powerBasis_gen]
 
 end PowerBasis
+
+namespace IntermediateField
+
+variable {K L L' : Type*} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L']
+
+theorem map_comap_eq (f : L →ₐ[K] L') (S : IntermediateField K L') :
+    (S.comap f).map f = S ⊓ f.fieldRange :=
+  SetLike.coe_injective Set.image_preimage_eq_inter_range
+
+theorem map_comap_eq_self {f : L →ₐ[K] L'} {S : IntermediateField K L'} (h : S ≤ f.fieldRange) :
+    (S.comap f).map f = S := by
+  simpa only [inf_of_le_left h] using map_comap_eq f S
+
+theorem map_comap_eq_self_of_surjective {f : L →ₐ[K] L'} (hf : Function.Surjective f)
+    (S : IntermediateField K L') : (S.comap f).map f = S :=
+  SetLike.coe_injective (Set.image_preimage_eq _ hf)
+
+theorem comap_map (f : L →ₐ[K] L') (S : IntermediateField K L) : (S.map f).comap f = S :=
+  SetLike.coe_injective (Set.preimage_image_eq _ f.injective)
+
+end IntermediateField

Mathlib/RingTheory/Adjoin/Basic.lean

@@ -516,3 +516,29 @@ theorem Algebra.restrictScalars_adjoin_of_algEquiv
   erw [hi, Set.range_comp, i.toEquiv.range_eq_univ, Set.image_univ]
 
 end
+
+namespace Subalgebra
+
+variable [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
+
+theorem comap_map_eq (f : A →ₐ[R] B) (S : Subalgebra R A) :
+    (S.map f).comap f = S ⊔ Algebra.adjoin R (f ⁻¹' {0}) := by
+  apply le_antisymm
+  · intro x hx
+    rw [mem_comap, mem_map] at hx
+    obtain ⟨y, hy, hxy⟩ := hx
+    replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
+    rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]
+    exact Subalgebra.add_mem _
+      (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)
+  · rw [← map_le, Algebra.map_sup, f.map_adjoin]
+    apply le_of_eq
+    rw [sup_eq_left, Algebra.adjoin_le_iff]
+    exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)
+
+theorem comap_map_eq_self {f : A →ₐ[R] B} {S : Subalgebra R A}
+    (h : f ⁻¹' {0} ⊆ S) : (S.map f).comap f = S := by
+  convert comap_map_eq f S
+  rwa [left_eq_sup, Algebra.adjoin_le_iff]
+
+end Subalgebra