From 2aa39ca434a3c20369b7d68706abde3e47d327cb Mon Sep 17 00:00:00 2001 From: Jz Pan Date: Mon, 23 Sep 2024 15:47:58 +0000 Subject: [PATCH] feat: add `map_i[I]nf` for sub(semi)ring, subalgebra, subfield etc. (#15113) ... which require that the map in question is injective (this automatically holds for fields). Added for: - sub(semi)group, submonoid, and their additive counterpart - sub(semi)ring, (star)subalgebra, and their non-unital counterpart - subfield and intermediate fields. Also add `(coe|mem)_iInf` for subfield and (non-unital)subsemiring. --- .../Algebra/Algebra/NonUnitalSubalgebra.lean | 12 ++++++++++++ Mathlib/Algebra/Algebra/Subalgebra/Basic.lean | 8 ++++++++ Mathlib/Algebra/Field/Subfield.lean | 15 +++++++++++++++ Mathlib/Algebra/Group/Subgroup/Basic.lean | 10 ++++++++++ .../Algebra/Group/Submonoid/Operations.lean | 10 ++++++++++ .../Group/Subsemigroup/Operations.lean | 10 ++++++++++ Mathlib/Algebra/Ring/Subring/Basic.lean | 8 ++++++++ Mathlib/Algebra/Ring/Subsemiring/Basic.lean | 15 +++++++++++++++ Mathlib/Algebra/Star/NonUnitalSubalgebra.lean | 12 ++++++++++++ Mathlib/Algebra/Star/Subalgebra.lean | 8 ++++++++ Mathlib/FieldTheory/Adjoin.lean | 8 ++++++++ .../RingTheory/NonUnitalSubring/Basic.lean | 8 ++++++++ .../NonUnitalSubsemiring/Basic.lean | 19 +++++++++++++++++++ 13 files changed, 143 insertions(+) diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean index ce534b664d2fa..d7beda182c549 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean @@ -726,6 +726,11 @@ theorem map_sup [IsScalarTower R B B] [SMulCommClass R B B] ((S ⊔ T).map f : NonUnitalSubalgebra R B) = S.map f ⊔ T.map f := (NonUnitalSubalgebra.gc_map_comap f).l_sup +theorem map_inf [IsScalarTower R B B] [SMulCommClass R B B] + (f : F) (hf : Function.Injective f) (S T : NonUnitalSubalgebra R A) : + ((S ⊓ T).map f : NonUnitalSubalgebra R B) = S.map f ⊓ T.map f := + SetLike.coe_injective (Set.image_inter hf) + @[simp, norm_cast] theorem coe_inf (S T : NonUnitalSubalgebra R A) : (↑(S ⊓ T) : Set A) = (S : Set A) ∩ T := rfl @@ -768,6 +773,13 @@ theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} : theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range] +theorem map_iInf {ι : Sort*} [Nonempty ι] + [IsScalarTower R B B] [SMulCommClass R B B] (f : F) + (hf : Function.Injective f) (S : ι → NonUnitalSubalgebra R A) : + ((⨅ i, S i).map f : NonUnitalSubalgebra R B) = ⨅ i, (S i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S) + @[simp] theorem iInf_toSubmodule {ι : Sort*} (S : ι → NonUnitalSubalgebra R A) : (⨅ i, S i).toSubmodule = ⨅ i, (S i).toSubmodule := diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean index 854c9922cd13d..311a49067acad 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean @@ -678,6 +678,9 @@ theorem mul_mem_sup {S T : Subalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ theorem map_sup (f : A →ₐ[R] B) (S T : Subalgebra R A) : (S ⊔ T).map f = S.map f ⊔ T.map f := (Subalgebra.gc_map_comap f).l_sup +theorem map_inf (f : A →ₐ[R] B) (hf : Function.Injective f) (S T : Subalgebra R A) : + (S ⊓ T).map f = S.map f ⊓ T.map f := SetLike.coe_injective (Set.image_inter hf) + @[simp, norm_cast] theorem coe_inf (S T : Subalgebra R A) : (↑(S ⊓ T) : Set A) = (S ∩ T : Set A) := rfl @@ -718,6 +721,11 @@ theorem coe_iInf {ι : Sort*} {S : ι → Subalgebra R A} : (↑(⨅ i, S i) : S theorem mem_iInf {ι : Sort*} {S : ι → Subalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range] +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : A →ₐ[R] B) (hf : Function.Injective f) + (s : ι → Subalgebra R A) : (iInf s).map f = ⨅ (i : ι), (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + open Subalgebra in @[simp] theorem iInf_toSubmodule {ι : Sort*} (S : ι → Subalgebra R A) : diff --git a/Mathlib/Algebra/Field/Subfield.lean b/Mathlib/Algebra/Field/Subfield.lean index 8d57654e441ac..63adf4ac50a55 100644 --- a/Mathlib/Algebra/Field/Subfield.lean +++ b/Mathlib/Algebra/Field/Subfield.lean @@ -545,6 +545,13 @@ theorem mem_sInf {S : Set (Subfield K)} {x : K} : x ∈ sInf S ↔ ∀ p ∈ S, Subring.mem_sInf.trans ⟨fun h p hp => h p.toSubring ⟨p, hp, rfl⟩, fun h _ ⟨p', hp', p_eq⟩ => p_eq ▸ h p' hp'⟩ +@[simp, norm_cast] +theorem coe_iInf {ι : Sort*} {S : ι → Subfield K} : (↑(⨅ i, S i) : Set K) = ⋂ i, S i := by + simp only [iInf, coe_sInf, Set.biInter_range] + +theorem mem_iInf {ι : Sort*} {S : ι → Subfield K} {x : K} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by + simp only [iInf, mem_sInf, Set.forall_mem_range] + @[simp] theorem sInf_toSubring (s : Set (Subfield K)) : (sInf s).toSubring = ⨅ t ∈ s, Subfield.toSubring t := by @@ -659,6 +666,14 @@ theorem map_iSup {ι : Sort*} (f : K →+* L) (s : ι → Subfield K) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +theorem map_inf (s t : Subfield K) (f : K →+* L) : (s ⊓ t).map f = s.map f ⊓ t.map f := + SetLike.coe_injective (Set.image_inter f.injective) + +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : K →+* L) (s : ι → Subfield K) : + (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s) + theorem comap_inf (s t : Subfield L) (f : K →+* L) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f := (gc_map_comap f).u_inf diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean index 7881c95bcec47..9a542a9b6014d 100644 --- a/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean @@ -1205,6 +1205,16 @@ theorem map_iSup {ι : Sort*} (f : G →* N) (s : ι → Subgroup G) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +@[to_additive] +theorem map_inf (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) : + (H ⊓ K).map f = H.map f ⊓ K.map f := SetLike.coe_injective (Set.image_inter hf) + +@[to_additive] +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : G →* N) (hf : Function.Injective f) + (s : ι → Subgroup G) : (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + @[to_additive] theorem comap_sup_comap_le (H K : Subgroup N) (f : G →* N) : comap f H ⊔ comap f K ≤ comap f (H ⊔ K) := diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean index e410115baf4ec..a0ee1b9441d79 100644 --- a/Mathlib/Algebra/Group/Submonoid/Operations.lean +++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean @@ -274,6 +274,16 @@ theorem map_sup (S T : Submonoid M) (f : F) : (S ⊔ T).map f = S.map f ⊔ T.ma theorem map_iSup {ι : Sort*} (f : F) (s : ι → Submonoid M) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f : GaloisConnection (map f) (comap f)).l_iSup +@[to_additive] +theorem map_inf (S T : Submonoid M) (f : F) (hf : Function.Injective f) : + (S ⊓ T).map f = S.map f ⊓ T.map f := SetLike.coe_injective (Set.image_inter hf) + +@[to_additive] +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) + (s : ι → Submonoid M) : (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + @[to_additive] theorem comap_inf (S T : Submonoid N) (f : F) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f := (gc_map_comap f : GaloisConnection (map f) (comap f)).u_inf diff --git a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean index 4f86ed34a4d25..05de353785319 100644 --- a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean +++ b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean @@ -278,6 +278,16 @@ theorem map_iSup {ι : Sort*} (f : M →ₙ* N) (s : ι → Subsemigroup M) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +@[to_additive] +theorem map_inf (S T : Subsemigroup M) (f : M →ₙ* N) (hf : Function.Injective f) : + (S ⊓ T).map f = S.map f ⊓ T.map f := SetLike.coe_injective (Set.image_inter hf) + +@[to_additive] +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : M →ₙ* N) (hf : Function.Injective f) + (s : ι → Subsemigroup M) : (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + @[to_additive] theorem comap_inf (S T : Subsemigroup N) (f : M →ₙ* N) : (S ⊓ T).comap f = S.comap f ⊓ T.comap f := (gc_map_comap f).u_inf diff --git a/Mathlib/Algebra/Ring/Subring/Basic.lean b/Mathlib/Algebra/Ring/Subring/Basic.lean index c93d933e50864..dece9ec6923b9 100644 --- a/Mathlib/Algebra/Ring/Subring/Basic.lean +++ b/Mathlib/Algebra/Ring/Subring/Basic.lean @@ -897,6 +897,14 @@ theorem map_iSup {ι : Sort*} (f : R →+* S) (s : ι → Subring R) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +theorem map_inf (s t : Subring R) (f : R →+* S) (hf : Function.Injective f) : + (s ⊓ t).map f = s.map f ⊓ t.map f := SetLike.coe_injective (Set.image_inter hf) + +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f) + (s : ι → Subring R) : (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + theorem comap_inf (s t : Subring S) (f : R →+* S) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f := (gc_map_comap f).u_inf diff --git a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean index 72f996c586990..03dc4ba71c416 100644 --- a/Mathlib/Algebra/Ring/Subsemiring/Basic.lean +++ b/Mathlib/Algebra/Ring/Subsemiring/Basic.lean @@ -500,6 +500,13 @@ theorem coe_sInf (S : Set (Subsemiring R)) : ((sInf S : Subsemiring R) : Set R) theorem mem_sInf {S : Set (Subsemiring R)} {x : R} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p := Set.mem_iInter₂ +@[simp, norm_cast] +theorem coe_iInf {ι : Sort*} {S : ι → Subsemiring R} : (↑(⨅ i, S i) : Set R) = ⋂ i, S i := by + simp only [iInf, coe_sInf, Set.biInter_range] + +theorem mem_iInf {ι : Sort*} {S : ι → Subsemiring R} {x : R} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by + simp only [iInf, mem_sInf, Set.forall_mem_range] + @[simp] theorem sInf_toSubmonoid (s : Set (Subsemiring R)) : (sInf s).toSubmonoid = ⨅ t ∈ s, Subsemiring.toSubmonoid t := @@ -835,6 +842,14 @@ theorem map_iSup {ι : Sort*} (f : R →+* S) (s : ι → Subsemiring R) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +theorem map_inf (s t : Subsemiring R) (f : R →+* S) (hf : Function.Injective f) : + (s ⊓ t).map f = s.map f ⊓ t.map f := SetLike.coe_injective (Set.image_inter hf) + +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : R →+* S) (hf : Function.Injective f) + (s : ι → Subsemiring R) : (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + theorem comap_inf (s t : Subsemiring S) (f : R →+* S) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f := (gc_map_comap f).u_inf diff --git a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean index 88ae6784d80a8..61e7ac629195f 100644 --- a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean +++ b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean @@ -733,6 +733,11 @@ theorem map_sup [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f ((S ⊔ T).map f : NonUnitalStarSubalgebra R B) = S.map f ⊔ T.map f := (NonUnitalStarSubalgebra.gc_map_comap f).l_sup +theorem map_inf [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) + (hf : Function.Injective f) (S T : NonUnitalStarSubalgebra R A) : + ((S ⊓ T).map f : NonUnitalStarSubalgebra R B) = S.map f ⊓ T.map f := + SetLike.coe_injective (Set.image_inter hf) + @[simp, norm_cast] theorem coe_inf (S T : NonUnitalStarSubalgebra R A) : (↑(S ⊓ T) : Set A) = (S : Set A) ∩ T := rfl @@ -766,6 +771,13 @@ theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalStarSubalgebra R A} : theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalStarSubalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range] +theorem map_iInf {ι : Sort*} [Nonempty ι] + [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F) + (hf : Function.Injective f) (S : ι → NonUnitalStarSubalgebra R A) : + ((⨅ i, S i).map f : NonUnitalStarSubalgebra R B) = ⨅ i, (S i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S) + @[simp] theorem iInf_toNonUnitalSubalgebra {ι : Sort*} (S : ι → NonUnitalStarSubalgebra R A) : (⨅ i, S i).toNonUnitalSubalgebra = ⨅ i, (S i).toNonUnitalSubalgebra := diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean index 2de08d5c7ac4d..b0dc2097f565e 100644 --- a/Mathlib/Algebra/Star/Subalgebra.lean +++ b/Mathlib/Algebra/Star/Subalgebra.lean @@ -594,6 +594,9 @@ theorem mul_mem_sup {S T : StarSubalgebra R A} {x y : A} (hx : x ∈ S) (hy : y theorem map_sup (f : A →⋆ₐ[R] B) (S T : StarSubalgebra R A) : map f (S ⊔ T) = map f S ⊔ map f T := (StarSubalgebra.gc_map_comap f).l_sup +theorem map_inf (f : A →⋆ₐ[R] B) (hf : Function.Injective f) (S T : StarSubalgebra R A) : + map f (S ⊓ T) = map f S ⊓ map f T := SetLike.coe_injective (Set.image_inter hf) + @[simp, norm_cast] theorem coe_inf (S T : StarSubalgebra R A) : (↑(S ⊓ T) : Set A) = (S : Set A) ∩ T := rfl @@ -627,6 +630,11 @@ theorem coe_iInf {ι : Sort*} {S : ι → StarSubalgebra R A} : (↑(⨅ i, S i) theorem mem_iInf {ι : Sort*} {S : ι → StarSubalgebra R A} {x : A} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by simp only [iInf, mem_sInf, Set.forall_mem_range] +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : A →⋆ₐ[R] B) (hf : Function.Injective f) + (s : ι → StarSubalgebra R A) : map f (iInf s) = ⨅ (i : ι), map f (s i) := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + @[simp] theorem iInf_toSubalgebra {ι : Sort*} (S : ι → StarSubalgebra R A) : (⨅ i, S i).toSubalgebra = ⨅ i, (S i).toSubalgebra := diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index 525d7d0c62b82..07881787d2645 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -252,6 +252,14 @@ theorem map_iSup {ι : Sort*} (f : E →ₐ[F] K) (s : ι → IntermediateField (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +theorem map_inf (s t : IntermediateField F E) (f : E →ₐ[F] K) : + (s ⊓ t).map f = s.map f ⊓ t.map f := SetLike.coe_injective (Set.image_inter f.injective) + +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : E →ₐ[F] K) (s : ι → IntermediateField F E) : + (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s) + theorem _root_.AlgHom.fieldRange_eq_map (f : E →ₐ[F] K) : f.fieldRange = IntermediateField.map f ⊤ := SetLike.ext' Set.image_univ.symm diff --git a/Mathlib/RingTheory/NonUnitalSubring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubring/Basic.lean index 3d5642917f222..69c9fcd2931b4 100644 --- a/Mathlib/RingTheory/NonUnitalSubring/Basic.lean +++ b/Mathlib/RingTheory/NonUnitalSubring/Basic.lean @@ -800,6 +800,14 @@ theorem map_iSup {ι : Sort*} (f : F) (s : ι → NonUnitalSubring R) : (iSup s).map f = ⨆ i, (s i).map f := (gc_map_comap f).l_iSup +theorem map_inf (s t : NonUnitalSubring R) (f : F) (hf : Function.Injective f) : + (s ⊓ t).map f = s.map f ⊓ t.map f := SetLike.coe_injective (Set.image_inter hf) + +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) + (s : ι → NonUnitalSubring R) : (iInf s).map f = ⨅ i, (s i).map f := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + theorem comap_inf (s t : NonUnitalSubring S) (f : F) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f := (gc_map_comap f).u_inf diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean index 3e465645af7db..55bb7d2fd0d44 100644 --- a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean +++ b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean @@ -379,6 +379,15 @@ theorem coe_sInf (S : Set (NonUnitalSubsemiring R)) : theorem mem_sInf {S : Set (NonUnitalSubsemiring R)} {x : R} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p := Set.mem_iInter₂ +@[simp, norm_cast] +theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubsemiring R} : + (↑(⨅ i, S i) : Set R) = ⋂ i, S i := by + simp only [iInf, coe_sInf, Set.biInter_range] + +theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubsemiring R} {x : R} : + (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by + simp only [iInf, mem_sInf, Set.forall_mem_range] + @[simp] theorem sInf_toSubsemigroup (s : Set (NonUnitalSubsemiring R)) : (sInf s).toSubsemigroup = ⨅ t ∈ s, NonUnitalSubsemiring.toSubsemigroup t := @@ -670,6 +679,16 @@ theorem map_iSup {ι : Sort*} (f : F) (s : ι → NonUnitalSubsemiring R) : (map f (iSup s) : NonUnitalSubsemiring S) = ⨆ i, map f (s i) := @GaloisConnection.l_iSup _ _ _ _ _ _ _ (gc_map_comap f) s +theorem map_inf (s t : NonUnitalSubsemiring R) (f : F) (hf : Function.Injective f) : + (map f (s ⊓ t) : NonUnitalSubsemiring S) = map f s ⊓ map f t := + SetLike.coe_injective (Set.image_inter hf) + +theorem map_iInf {ι : Sort*} [Nonempty ι] (f : F) (hf : Function.Injective f) + (s : ι → NonUnitalSubsemiring R) : + (map f (iInf s) : NonUnitalSubsemiring S) = ⨅ i, map f (s i) := by + apply SetLike.coe_injective + simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s) + theorem comap_inf (s t : NonUnitalSubsemiring S) (f : F) : (comap f (s ⊓ t) : NonUnitalSubsemiring R) = comap f s ⊓ comap f t := @GaloisConnection.u_inf _ _ s t _ _ _ _ (gc_map_comap f)