Adjoining elements to form subalgebras

This file develops the basic theory of subalgebras of an R-algebra generated by a set of elements. A basic interface for adjoin is set up.

Tags

adjoin, algebra

theorem Algebra.subset_adjoin {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : s ⊆ ↑(Algebra.adjoin R s)

theorem Algebra.adjoin_le {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {S : Subalgebra R A} (H : s ⊆ ↑S) : Algebra.adjoin R s ≤ S

theorem Algebra.adjoin_eq_sInf {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : Algebra.adjoin R s = sInf {p : Subalgebra R A | s ⊆ ↑p}

theorem Algebra.adjoin_le_iff {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {S : Subalgebra R A} : Algebra.adjoin R s ≤ S ↔ s ⊆ ↑S

theorem Algebra.adjoin_mono {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {t : Set A} (H : s ⊆ t) : Algebra.adjoin R s ≤ Algebra.adjoin R t

theorem Algebra.adjoin_eq_of_le {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} (S : Subalgebra R A) (h₁ : s ⊆ ↑S) (h₂ : S ≤ Algebra.adjoin R s) : Algebra.adjoin R s = S

theorem Algebra.adjoin_eq {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Algebra.adjoin R ↑S = S

theorem Algebra.adjoin_iUnion {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} (s : α → Set A) : Algebra.adjoin R (Set.iUnion s) = ⨆ (i : α), Algebra.adjoin R (s i)

theorem Algebra.adjoin_attach_biUnion {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq A] {α : Type u_1} {s : Finset α} (f : { x : α // x ∈ s } → Finset A) : Algebra.adjoin R ↑(s.attach.biUnion f) = ⨆ (x : { x : α // x ∈ s }), Algebra.adjoin R ↑(f x)

theorem Algebra.adjoin_induction {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {p : (x : A) → x ∈ Algebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯) (add : ∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) {x : A} (hx : x ∈ Algebra.adjoin R s) : p x hx

@[deprecated Algebra.adjoin_induction]

theorem Algebra.adjoin_induction'' {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {p : (x : A) → x ∈ Algebra.adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R A) r) ⋯) (add : ∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) {x : A} (hx : x ∈ Algebra.adjoin R s) : p x hx

Alias of Algebra.adjoin_induction.

theorem Algebra.adjoin_induction₂ {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {p : (x y : A) → x ∈ Algebra.adjoin R s → y ∈ Algebra.adjoin R s → Prop} (mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯) (algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯) (algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯) (add_left : ∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) (hz : z ∈ Algebra.adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x : A} {y : A} (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s) : p x y hx hy

Induction principle for the algebra generated by a set s: show that p x y holds for any x y ∈ adjoin R s given that it holds for x y ∈ s and that it satisfies a number of natural properties.

@[deprecated Algebra.adjoin_induction]

theorem Algebra.adjoin_induction' {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {p : ↥(Algebra.adjoin R s) → Prop} (mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) (algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(Algebra.adjoin R s)) r)) (add : ∀ (x y : ↥(Algebra.adjoin R s)), p x → p y → p (x + y)) (mul : ∀ (x y : ↥(Algebra.adjoin R s)), p x → p y → p (x * y)) (x : ↥(Algebra.adjoin R s)) : p x

The difference with Algebra.adjoin_induction is that this acts on the subtype.

@[simp]

theorem Algebra.adjoin_adjoin_coe_preimage {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : Algebra.adjoin R (Subtype.val ⁻¹' s) = ⊤

theorem Algebra.adjoin_union {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) (t : Set A) : Algebra.adjoin R (s ∪ t) = Algebra.adjoin R s ⊔ Algebra.adjoin R t

@[simp]

theorem Algebra.adjoin_empty (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.adjoin R ∅ = ⊥

@[simp]

theorem Algebra.adjoin_univ (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.adjoin R Set.univ = ⊤

theorem Algebra.adjoin_eq_span (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R ↑(Submonoid.closure s)

theorem Algebra.span_le_adjoin (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : Submodule.span R s ≤ Subalgebra.toSubmodule (Algebra.adjoin R s)

theorem Algebra.adjoin_toSubmodule_le (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {t : Submodule R A} : Subalgebra.toSubmodule (Algebra.adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t

theorem Algebra.adjoin_eq_span_of_subset (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} (hs : ↑(Submonoid.closure s) ⊆ ↑(Submodule.span R s)) : Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R s

@[simp]

theorem Algebra.adjoin_span (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : Algebra.adjoin R ↑(Submodule.span R s) = Algebra.adjoin R s

theorem Algebra.adjoin_image (R : Type uR) {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (s : Set A) : Algebra.adjoin R (⇑f '' s) = Subalgebra.map f (Algebra.adjoin R s)

@[simp]

theorem Algebra.adjoin_insert_adjoin (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) (x : A) : Algebra.adjoin R (insert x ↑(Algebra.adjoin R s)) = Algebra.adjoin R (insert x s)

theorem Algebra.adjoin_prod_le (R : Type uR) {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (s : Set A) (t : Set B) : Algebra.adjoin R (s ×ˢ t) ≤ (Algebra.adjoin R s).prod (Algebra.adjoin R t)

theorem Algebra.mem_adjoin_of_map_mul (R : Type uR) {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {s : Set A} {x : A} {f : A →ₗ[R] B} (hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂) (h : x ∈ Algebra.adjoin R s) : f x ∈ Algebra.adjoin R (⇑f '' (s ∪ {1}))

theorem Algebra.adjoin_inl_union_inr_eq_prod (R : Type uR) {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (s : Set A) (t : Set B) : Algebra.adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) = (Algebra.adjoin R s).prod (Algebra.adjoin R t)

def Algebra.adjoinCommSemiringOfComm (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommSemiring ↥(Algebra.adjoin R s)

If all elements of s : Set A commute pairwise, then adjoin R s is a commutative semiring.

Equations

• Algebra.adjoinCommSemiringOfComm R hcomm = CommSemiring.mk ⋯

theorem Algebra.commute_of_mem_adjoin_of_forall_mem_commute {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {b : A} {s : Set A} (hb : b ∈ Algebra.adjoin R s) (h : ∀ b ∈ s, Commute a b) : Commute a b

theorem Algebra.commute_of_mem_adjoin_singleton_of_commute {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {b : A} {c : A} (hc : c ∈ Algebra.adjoin R {b}) (h : Commute a b) : Commute a c

theorem Algebra.commute_of_mem_adjoin_self {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} {b : A} (hb : b ∈ Algebra.adjoin R {a}) : Commute a b

theorem Algebra.adjoin_singleton_one (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.adjoin R {1} = ⊥

theorem Algebra.self_mem_adjoin_singleton (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : x ∈ Algebra.adjoin R {x}

theorem Algebra.adjoin_algebraMap (R : Type uR) {S : Type uS} (A : Type uA) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (s : Set S) : Algebra.adjoin R (⇑(algebraMap S A) '' s) = Subalgebra.map (IsScalarTower.toAlgHom R S A) (Algebra.adjoin R s)

theorem Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin (R : Type uR) {S : Type uS} {A : Type uA} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (s : Set S) (t : Set A) : Algebra.adjoin R (⇑(algebraMap S A) '' s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin (↥(Algebra.adjoin R s)) t)

theorem Algebra.adjoin_adjoin_of_tower (R : Type uR) {S : Type uS} {A : Type uA} [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] (s : Set A) : Algebra.adjoin S ↑(Algebra.adjoin R s) = Algebra.adjoin S s

@[simp]

theorem Algebra.adjoin_top (R : Type uR) {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] {A : Type u_1} [Semiring A] [Algebra S A] (t : Set A) : Algebra.adjoin (↥⊤) t = Subalgebra.restrictScalars (↥⊤) (Algebra.adjoin S t)

theorem Algebra.adjoin_union_eq_adjoin_adjoin (R : Type uR) {A : Type uA} [CommSemiring R] [CommSemiring A] [Algebra R A] (s : Set A) (t : Set A) : Algebra.adjoin R (s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin (↥(Algebra.adjoin R s)) t)

theorem Algebra.adjoin_union_coe_submodule (R : Type uR) {A : Type uA} [CommSemiring R] [CommSemiring A] [Algebra R A] (s : Set A) (t : Set A) : Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t)) = Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule (Algebra.adjoin R t)

theorem Algebra.pow_smul_mem_of_smul_subset_of_mem_adjoin {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [CommSemiring A] [Algebra R A] [CommSemiring B] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (r : A) (s : Set B) (B' : Subalgebra R B) (hs : r • s ⊆ ↑B') {x : B} (hx : x ∈ Algebra.adjoin R s) (hr : (algebraMap A B) r ∈ B') : ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ B'

theorem Algebra.pow_smul_mem_adjoin_smul {R : Type uR} {A : Type uA} [CommSemiring R] [CommSemiring A] [Algebra R A] (r : R) (s : Set A) {x : A} (hx : x ∈ Algebra.adjoin R s) : ∃ (n₀ : ℕ), ∀ n ≥ n₀, r ^ n • x ∈ Algebra.adjoin R (r • s)

theorem Algebra.mem_adjoin_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {s : Set A} {x : A} : x ∈ Algebra.adjoin R s ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)

theorem Algebra.adjoin_eq_ring_closure {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (s : Set A) : (Algebra.adjoin R s).toSubring = Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)

def Algebra.adjoinCommRingOfComm (R : Type uR) {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : CommRing ↥(Algebra.adjoin R s)

If all elements of s : Set A commute pairwise, then adjoin R s is a commutative ring.

Equations

• Algebra.adjoinCommRingOfComm R hcomm = CommRing.mk ⋯

theorem AlgHom.map_adjoin {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : Set A) : Subalgebra.map φ (Algebra.adjoin R s) = Algebra.adjoin R (⇑φ '' s)

@[simp]

theorem AlgHom.map_adjoin_singleton {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A →ₐ[R] B) (x : A) : Subalgebra.map e (Algebra.adjoin R {x}) = Algebra.adjoin R {e x}

theorem AlgHom.adjoin_le_equalizer {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ₁ : A →ₐ[R] B) (φ₂ : A →ₐ[R] B) {s : Set A} (h : Set.EqOn (⇑φ₁) (⇑φ₂) s) : Algebra.adjoin R s ≤ AlgHom.equalizer φ₁ φ₂

theorem AlgHom.ext_of_adjoin_eq_top {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {s : Set A} (h : Algebra.adjoin R s = ⊤) ⦃φ₁ : A →ₐ[R] B⦄ ⦃φ₂ : A →ₐ[R] B⦄ (hs : Set.EqOn (⇑φ₁) (⇑φ₂) s) : φ₁ = φ₂

theorem AlgHom.eqOn_adjoin_iff {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ : A →ₐ[R] B} {ψ : A →ₐ[R] B} {s : Set A} : Set.EqOn ⇑φ ⇑ψ ↑(Algebra.adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

Two algebra morphisms are equal on Algebra.span siff they are equal on s

theorem Algebra.adjoin_nat {R : Type u_1} [Semiring R] (s : Set R) : Algebra.adjoin ℕ s = subalgebraOfSubsemiring (Subsemiring.closure s)

theorem Algebra.adjoin_int {R : Type u_1} [Ring R] (s : Set R) : Algebra.adjoin ℤ s = subalgebraOfSubring (Subring.closure s)

def Subsemiring.closureEquivAdjoinNat {R : Type u_1} [Semiring R] (s : Set R) : ↥(Subsemiring.closure s) ≃ₐ[ℕ] ↥(Algebra.adjoin ℕ s)

The ℕ-algebra equivalence between Subsemiring.closure s and Algebra.adjoin ℕ s given by the identity map.

Equations

• Subsemiring.closureEquivAdjoinNat s = (subalgebraOfSubsemiring (Subsemiring.closure s)).equivOfEq (Algebra.adjoin ℕ s) ⋯

def Subring.closureEquivAdjoinInt {R : Type u_1} [Ring R] (s : Set R) : ↥(Subring.closure s) ≃ₐ[ℤ] ↥(Algebra.adjoin ℤ s)

The ℤ-algebra equivalence between Subring.closure s and Algebra.adjoin ℤ s given by the identity map.

Equations

• Subring.closureEquivAdjoinInt s = (subalgebraOfSubring (Subring.closure s)).equivOfEq (Algebra.adjoin ℤ s) ⋯

theorem Submonoid.adjoin_eq_span_of_eq_span (F : Type u_1) (E : Type u_2) {K : Type u_3} [CommSemiring E] [Semiring K] [SMul F E] [Algebra E K] [Semiring F] [Module F K] [IsScalarTower F E K] (L : Submonoid K) {S : Set K} (h : ↑L = ↑(Submodule.span F S)) : Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S

If K / E / F is a ring extension tower, L is a submonoid of K / F which is generated by S as an F-module, then E[L] is generated by S as an E-module.

theorem Subalgebra.adjoin_eq_span_of_eq_span {F : Type u_1} (E : Type u_2) {K : Type u_3} [CommSemiring E] [Semiring K] [SMul F E] [Algebra E K] [CommSemiring F] [Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K) {S : Set K} (h : Subalgebra.toSubmodule L = Submodule.span F S) : Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S

If K / E / F is a ring extension tower, L is a subalgebra of K / F which is generated by S as an F-module, then E[L] is generated by S as an E-module.

theorem Subalgebra.adjoin_eq_span_basis {F : Type u_1} (E : Type u_2) {K : Type u_3} [CommSemiring E] [Semiring K] [SMul F E] [Algebra E K] [CommSemiring F] [Algebra F K] [IsScalarTower F E K] (L : Subalgebra F K) {ι : Type u_4} (bL : Basis ι F ↥L) : Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E (Set.range fun (i : ι) => ↑(bL i))

If K / E / F is a ring extension tower, L is a subalgebra of K / F, then E[L] is generated by any basis of L / F as an E-module.

theorem Algebra.restrictScalars_adjoin (F : Type u_4) [CommSemiring F] {E : Type u_5} [CommSemiring E] [Algebra F E] (K : Subalgebra F E) (S : Set E) : Subalgebra.restrictScalars F (Algebra.adjoin (↥K) S) = Algebra.adjoin F (↑K ∪ S)

theorem Algebra.restrictScalars_adjoin_of_algEquiv {F : Type u_4} {E : Type u_5} {L : Type u_6} {L' : Type u_7} [CommSemiring F] [CommSemiring L] [CommSemiring L'] [Semiring E] [Algebra F L] [Algebra L E] [Algebra F L'] [Algebra L' E] [Algebra F E] [IsScalarTower F L E] [IsScalarTower F L' E] (i : L ≃ₐ[F] L') (hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i) (S : Set E) : Subalgebra.restrictScalars F (Algebra.adjoin L S) = Subalgebra.restrictScalars F (Algebra.adjoin L' S)

If E / L / F and E / L' / F are two ring extension towers, L ≃ₐ[F] L' is an isomorphism compatible with E / L and E / L', then for any subset S of E, L[S] and L'[S] are equal as subalgebras of E / F.

theorem Subalgebra.comap_map_eq {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R A) : Subalgebra.comap f (Subalgebra.map f S) = S ⊔ Algebra.adjoin R (⇑f ⁻¹' {0})

theorem Subalgebra.comap_map_eq_self {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B] {f : A →ₐ[R] B} {S : Subalgebra R A} (h : ⇑f ⁻¹' {0} ⊆ ↑S) : Subalgebra.comap f (Subalgebra.map f S) = S