Complete lattice structure of subalgebras #

In this file we define Algebra.adjoin and the complete lattice structure on subalgebras.

More lemmas about adjoin can be found in Mathlib/RingTheory/Adjoin/Basic.lean.

source

def Algebra.adjoin (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

Subalgebra R A

The minimal subalgebra that includes s.

Equations

Algebra.adjoin R s = { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s), algebraMap_mem' := ⋯ }

Instances For

source

theorem Algebra.adjoin_toSubsemiring (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

(adjoin R s).toSubsemiring = Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s)

source

theorem Algebra.gc {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

GaloisConnection (adjoin R) SetLike.coe

source

def Algebra.gi {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

GaloisInsertion (adjoin R) SetLike.coe

Galois insertion between adjoin and coe.

Equations

Algebra.gi = { choice := fun (s : Set A) (hs : ↑(Algebra.adjoin R s) ≤ s) => (Algebra.adjoin R s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For

source

@[implicit_reducible]

instance Algebra.instCompleteLatticeSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

CompleteLattice (Subalgebra R A)

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance Algebra.instSubtypeMemSubalgebraMin {R : Type u} [CommSemiring R] {C : Type u_1} [CommSemiring C] [Algebra R C] (S₁ S₂ : Subalgebra R C) :

Algebra ↥(S₁ ⊓ S₂) ↥S₁

Equations

Algebra.instSubtypeMemSubalgebraMin S₁ S₂ = (Subalgebra.inclusion ⋯).toAlgebra

source

@[implicit_reducible]

instance Algebra.instSubtypeMemSubalgebraMin_1 {R : Type u} [CommSemiring R] {C : Type u_1} [CommSemiring C] [Algebra R C] (S₁ S₂ : Subalgebra R C) :

Algebra ↥(S₁ ⊓ S₂) ↥S₂

Equations

Algebra.instSubtypeMemSubalgebraMin_1 S₁ S₂ = (Subalgebra.inclusion ⋯).toAlgebra

source

theorem Algebra.sup_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) :

S ⊔ T = adjoin R (↑S ∪ ↑T)

source

theorem Algebra.sSup_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :

sSup S = adjoin R (⋃₀ (SetLike.coe '' S))

source

@[simp]

theorem Algebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

↑⊤ = Set.univ

source

@[simp]

theorem Algebra.mem_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} :

x ∈ ⊤

source

@[simp]

theorem Algebra.top_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

Subalgebra.toSubmodule ⊤ = ⊤

source

@[simp]

theorem Algebra.top_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

⊤.toSubsemiring = ⊤

source

@[simp]

theorem Algebra.top_toSubring {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] :

⊤.toSubring = ⊤

source

@[simp]

theorem Algebra.toSubmodule_eq_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :

Subalgebra.toSubmodule S = ⊤ ↔ S = ⊤

source

@[simp]

theorem Algebra.toSubsemiring_eq_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :

S.toSubsemiring = ⊤ ↔ S = ⊤

source

@[simp]

theorem Algebra.toSubring_eq_top {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} :

S.toSubring = ⊤ ↔ S = ⊤

source

theorem Algebra.mem_sup_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} {x : A} :

x ∈ S → x ∈ S ⊔ T

source

theorem Algebra.mem_sup_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} {x : A} :

x ∈ T → x ∈ S ⊔ T

source

theorem Algebra.mul_mem_sup {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) :

x * y ∈ S ⊔ T

source

theorem Algebra.map_sup {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S T : Subalgebra R A) :

Subalgebra.map f (S ⊔ T) = Subalgebra.map f S ⊔ Subalgebra.map f T

source

theorem Algebra.map_inf {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (S T : Subalgebra R A) :

Subalgebra.map f (S ⊓ T) = Subalgebra.map f S ⊓ Subalgebra.map f T

source

@[simp]

theorem Algebra.coe_inf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) :

↑(S ⊓ T) = ↑S ∩ ↑T

source

@[simp]

theorem Algebra.mem_inf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} {x : A} :

x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

source

@[simp]

theorem Algebra.inf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) :

Subalgebra.toSubmodule (S ⊓ T) = Subalgebra.toSubmodule S ⊓ Subalgebra.toSubmodule T

source

@[simp]

theorem Algebra.inf_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) :

(S ⊓ T).toSubsemiring = S.toSubsemiring ⊓ T.toSubsemiring

source

@[simp]

theorem Algebra.sup_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S T : Subalgebra R A) :

(S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring

source

@[simp]

theorem Algebra.coe_sInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :

↑(sInf S) = ⋂ s ∈ S, ↑s

source

@[simp]

theorem Algebra.mem_sInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Set (Subalgebra R A)} {x : A} :

x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

source

@[simp]

theorem Algebra.sInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :

Subalgebra.toSubmodule (sInf S) = sInf (⇑Subalgebra.toSubmodule '' S)

source

@[simp]

theorem Algebra.sInf_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) :

(sInf S).toSubsemiring = sInf (Subalgebra.toSubsemiring '' S)

source

@[simp]

theorem Algebra.sSup_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) (hS : S.Nonempty) :

(sSup S).toSubsemiring = sSup (Subalgebra.toSubsemiring '' S)

source

@[simp]

theorem Algebra.coe_iInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} {S : ι → Subalgebra R A} :

↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

source

@[simp]

theorem Algebra.mem_iInf {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} {S : ι → Subalgebra R A} {x : A} :

x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

source

theorem Algebra.map_iInf {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {ι : Sort u_1} [Nonempty ι] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (s : ι → Subalgebra R A) :

Subalgebra.map f (iInf s) = ⨅ (i : ι), Subalgebra.map f (s i)

source

@[simp]

theorem Algebra.iInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} (S : ι → Subalgebra R A) :

Subalgebra.toSubmodule (⨅ (i : ι), S i) = ⨅ (i : ι), Subalgebra.toSubmodule (S i)

source

@[simp]

theorem Algebra.iInf_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} (S : ι → Subalgebra R A) :

(iInf S).toSubsemiring = ⨅ (i : ι), (S i).toSubsemiring

source

@[simp]

theorem Algebra.iSup_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} [Nonempty ι] (S : ι → Subalgebra R A) :

(iSup S).toSubsemiring = ⨆ (i : ι), (S i).toSubsemiring

source

theorem Algebra.mem_iSup_of_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} {S : ι → Subalgebra R A} (i : ι) {x : A} (hx : x ∈ S i) :

x ∈ iSup S

source

theorem Algebra.iSup_induction {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} (S : ι → Subalgebra R A) {motive : A → Prop} {x : A} (mem : x ∈ ⨆ (i : ι), S i) (basic : ∀ (i : ι), ∀ a ∈ S i, motive a) (add : ∀ (a b : A), motive a → motive b → motive (a + b)) (mul : ∀ (a b : A), motive a → motive b → motive (a * b)) (algebraMap : ∀ (r : R), motive ((algebraMap R A) r)) :

motive x

source

theorem Algebra.iSup_induction' {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {ι : Sort u_1} (S : ι → Subalgebra R A) {motive : (x : A) → x ∈ ⨆ (i : ι), S i → Prop} {x : A} (mem : x ∈ ⨆ (i : ι), S i) (basic : ∀ (i : ι) (x : A) (hx : x ∈ S i), motive x ⋯) (add : ∀ (x y : A) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), motive x hx → motive y hy → motive (x + y) ⋯) (mul : ∀ (x y : A) (hx : x ∈ ⨆ (i : ι), S i) (hy : y ∈ ⨆ (i : ι), S i), motive x hx → motive y hy → motive (x * y) ⋯) (algebraMap : ∀ (r : R), motive ((algebraMap R A) r) ⋯) :

motive x mem

A dependent version of Subalgebra.iSup_induction.

source

@[implicit_reducible]

instance Algebra.instInhabitedSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

Inhabited (Subalgebra R A)

Equations

Algebra.instInhabitedSubalgebra = { default := ⊥ }

source

theorem Algebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {x : A} :

x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R A)

source

theorem Algebra.toSubmodule_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

Subalgebra.toSubmodule ⊥ = 1

TODO: change proof to rfl when fixing https://github.com/leanprover-community/mathlib4/issues/18110.

source

@[simp]

theorem Algebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

↑⊥ = Set.range ⇑(algebraMap R A)

source

@[simp]

theorem Algebra.toSubring_bot (A : Type u_1) [CommRing A] (R : Subring A) :

⊥.toSubring = R

source

theorem Algebra.eq_top_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} :

S = ⊤ ↔ ∀ (x : A), x ∈ S

source

theorem AlgHom.range_eq_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

f.range = ⊤ ↔ Function.Surjective ⇑f

source

@[simp]

theorem Algebra.range_ofId {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

(ofId R A).range = ⊥

source

@[simp]

theorem Algebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

(AlgHom.id R A).range = ⊤

source

@[simp]

theorem Algebra.map_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

Subalgebra.map f ⊤ = f.range

source

@[simp]

theorem Algebra.map_bot {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

Subalgebra.map f ⊥ = ⊥

source

@[simp]

theorem Algebra.comap_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :

Subalgebra.comap f ⊤ = ⊤

source

def Algebra.toTop {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

A →ₐ[R] ↥⊤

AlgHom to ⊤ : Subalgebra R A.

Equations

Algebra.toTop = (AlgHom.id R A).codRestrict ⊤ ⋯

Instances For

source

theorem Algebra.surjective_algebraMap_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

Function.Surjective ⇑(algebraMap R A) ↔ ⊤ = ⊥

source

theorem Algebra.bijective_algebraMap_iff {R : Type u_1} {A : Type u_2} [Field R] [Semiring A] [Nontrivial A] [Algebra R A] :

Function.Bijective ⇑(algebraMap R A) ↔ ⊤ = ⊥

source

noncomputable def Algebra.botEquivOfInjective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Injective ⇑(algebraMap R A)) :

↥⊥ ≃ₐ[R] R

The bottom subalgebra is isomorphic to the base ring.

Equations

Algebra.botEquivOfInjective h = (AlgEquiv.ofBijective (Algebra.ofId R ↥⊥) ⋯).symm

Instances For

source

noncomputable def Algebra.botEquiv (F : Type u_1) (R : Type u_2) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] :

↥⊥ ≃ₐ[F] F

The bottom subalgebra is isomorphic to the field.

Equations

Algebra.botEquiv F R = Algebra.botEquivOfInjective ⋯

Instances For

source

@[simp]

theorem Algebra.botEquiv_symm_apply (F : Type u_1) (R : Type u_2) [Field F] [Semiring R] [Nontrivial R] [Algebra F R] (a✝ : F) :

(botEquiv F R).symm a✝ = (algebraMap F ↥⊥) a✝

source

def Subalgebra.topEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :

↥⊤ ≃ₐ[R] A

The top subalgebra is isomorphic to the algebra.

This is the algebra version of Submodule.topEquiv.

Equations

Subalgebra.topEquiv = AlgEquiv.ofAlgHom ⊤.val Algebra.toTop ⋯ ⋯

Instances For

source

@[simp]

theorem Subalgebra.topEquiv_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : ↥⊤) :

topEquiv a = ↑a

source

@[simp]

theorem Subalgebra.topEquiv_symm_apply_coe {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

↑(topEquiv.symm a) = a

source

instance AlgHom.subsingleton {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Subsingleton (Subalgebra R A)] :

Subsingleton (A →ₐ[R] B)

source

instance AlgEquiv.subsingleton_left {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Subsingleton (Subalgebra R A)] :

Subsingleton (A ≃ₐ[R] B)

source

instance AlgEquiv.subsingleton_right {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Subsingleton (Subalgebra R B)] :

Subsingleton (A ≃ₐ[R] B)

source

@[implicit_reducible]

instance Subalgebra.instUnique {R : Type u} [CommSemiring R] :

Unique (Subalgebra R R)

Equations

Subalgebra.instUnique = { toInhabited := inferInstance, uniq := ⋯ }

source

@[simp]

theorem Subalgebra.center_eq_top (R : Type u) [CommSemiring R] (A : Type u_1) [CommSemiring A] [Algebra R A] :

center R A = ⊤

source

@[simp]

theorem Subalgebra.centralizer_eq_top_iff_subset (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} :

centralizer R s = ⊤ ↔ s ⊆ ↑(center R A)

source

@[simp]

theorem AlgHom.equalizer_eq_top {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] {φ ψ : F} :

equalizer φ ψ = ⊤ ↔ φ = ψ

source

@[simp]

theorem AlgHom.equalizer_same {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] (φ : F) :

equalizer φ φ = ⊤

source

theorem AlgHom.eqOn_sup {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] {φ ψ : F} {S T : Subalgebra R A} (hS : Set.EqOn ⇑φ ⇑ψ ↑S) (hT : Set.EqOn ⇑φ ⇑ψ ↑T) :

Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)

source

theorem AlgHom.ext_on_codisjoint {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {F : Type u_4} [FunLike F A B] [AlgHomClass F R A B] {φ ψ : F} {S T : Subalgebra R A} (hST : Codisjoint S T) (hS : Set.EqOn ⇑φ ⇑ψ ↑S) (hT : Set.EqOn ⇑φ ⇑ψ ↑T) :

φ = ψ

source

theorem Subalgebra.map_comap_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) :

map f (comap f S) = S ⊓ f.range

source

theorem Subalgebra.map_comap_eq_self {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₐ[R] B} {S : Subalgebra R B} (h : S ≤ f.range) :

map f (comap f S) = S

source

theorem Subalgebra.map_comap_eq_self_of_surjective {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {f : A →ₐ[R] B} (hf : Function.Surjective ⇑f) (S : Subalgebra R B) :

map f (comap f S) = S

source

def Subalgebra.saturation {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (s : Subalgebra R S) (M : Submonoid S) (H : M ≤ s.toSubmonoid) :

Subalgebra R S

The saturation of a subalgebra s with respect to a submonoid M is the smallest subalgebra closed under division by s.

Equations

s.saturation M H = { carrier := {x : S | ∃ m ∈ M, m * x ∈ s}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

Instances For

source

@[simp]

theorem Subalgebra.mem_saturation_iff {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} {x : S} :

x ∈ s.saturation M H ↔ ∃ m ∈ M, m • x ∈ s

source

theorem Subalgebra.le_saturation {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} :

s ≤ s.saturation M H

source

@[simp]

theorem Subalgebra.saturation_saturation {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} :

(s.saturation M H).saturation M ⋯ = s.saturation M H

source

theorem Subalgebra.mem_saturation_of_mul_mem_left {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} {x y : S} (hxy : x * y ∈ s.saturation M H) (hx : x ∈ M) :

y ∈ s.saturation M H

source

theorem Subalgebra.mem_saturation_of_mul_mem_right {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} {x y : S} (hxy : x * y ∈ s.saturation M H) (hy : y ∈ M) :

x ∈ s.saturation M H

source

@[simp]

theorem Algebra.subset_adjoin {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} :

s ⊆ ↑(adjoin R s)

source

theorem Algebra.mem_adjoin_of_mem {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {x : A} (hx : x ∈ s) :

x ∈ adjoin R s

source

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) :

adjoin R s ≤ S

source

theorem Algebra.adjoin_singleton_le {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {a : A} (H : a ∈ S) :

adjoin R {a} ≤ S

source

theorem Algebra.adjoin_eq_sInf {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} :

adjoin R s = sInf {p : Subalgebra R A | s ⊆ ↑p}

source

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} :

adjoin R s ≤ S ↔ s ⊆ ↑S

source

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

adjoin R s ≤ adjoin R t

source

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 ≤ adjoin R s) :

adjoin R s = S

source

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

adjoin R ↑S = S

source

theorem Algebra.adjoin_iUnion {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} (s : α → Set A) :

adjoin R (Set.iUnion s) = ⨆ (i : α), adjoin R (s i)

source

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 : ↥s → Finset A) :

adjoin R ↑(s.attach.biUnion f) = ⨆ (x : ↥s), adjoin R ↑(f x)

source

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

p x hx

source

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 ∈ adjoin R s → y ∈ 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 ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ 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 ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ 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 ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ 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 ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) {x y : A} (hx : x ∈ adjoin R s) (hy : y ∈ 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.

source

@[simp]

theorem Algebra.adjoin_adjoin_coe_preimage {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} :

adjoin R (Subtype.val ⁻¹' s) = ⊤

source

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

adjoin R (s ∪ t) = adjoin R s ⊔ adjoin R t

source

@[simp]

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

adjoin R ∅ = ⊥

source

@[simp]

theorem Algebra.adjoin_univ (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] :

adjoin R Set.univ = ⊤

source

@[simp]

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

adjoin R {(algebraMap R A) x} = ⊥

source

@[simp]

theorem Algebra.adjoin_singleton_natCast (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) :

adjoin R {↑n} = ⊥

source

@[simp]

theorem Algebra.adjoin_singleton_zero (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] :

adjoin R {0} = ⊥

source

@[simp]

theorem Algebra.adjoin_singleton_one (R : Type uR) (A : Type uA) [CommSemiring R] [Semiring A] [Algebra R A] :

adjoin R {1} = ⊥

source

@[simp]

theorem Algebra.adjoin_insert_algebraMap {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (x : R) (s : Set A) :

adjoin R (insert ((algebraMap R A) x) s) = adjoin R s

source

@[simp]

theorem Algebra.adjoin_insert_natCast (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) (s : Set A) :

adjoin R (insert (↑n) s) = adjoin R s

source

@[simp]

theorem Algebra.adjoin_insert_zero (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

adjoin R (insert 0 s) = adjoin R s

source

@[simp]

theorem Algebra.adjoin_insert_one (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

adjoin R (insert 1 s) = adjoin R s

source

theorem Algebra.adjoin_eq_span (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

Subalgebra.toSubmodule (adjoin R s) = Submodule.span R ↑(Submonoid.closure s)

source

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 (adjoin R s)

source

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 (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t

source

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 (adjoin R s) = Submodule.span R s

source

@[simp]

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

adjoin R ↑(Submodule.span R s) = adjoin R s

source

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) :

adjoin R (⇑f '' s) = Subalgebra.map f (adjoin R s)

source

@[simp]

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

adjoin R (insert x ↑(adjoin R s)) = adjoin R (insert x s)

source

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 ∈ adjoin R s) :

f x ∈ adjoin R (⇑f '' (s ∪ {1}))

source

theorem Algebra.adjoin_le_centralizer_centralizer (R : Type uR) {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) :

adjoin R s ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R s)

source

@[reducible, inline]

abbrev 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 ↥(adjoin R s)

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

Equations

Algebra.adjoinCommSemiringOfComm R hcomm = { toSemiring := (Algebra.adjoin R s).toSemiring, mul_comm := ⋯ }

Instances For

source

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

Commute a b

source

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

Commute a c

source

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

Commute a b

source

@[simp]

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

x ∈ adjoin R {x}

source

theorem Algebra.adjoin_union_coe_submodule (R : Type uR) {A : Type uA} [CommSemiring R] [CommSemiring A] [Algebra R A] (s t : Set A) :

Subalgebra.toSubmodule (adjoin R (s ∪ t)) = Subalgebra.toSubmodule (adjoin R s) * Subalgebra.toSubmodule (adjoin R t)

source

@[simp]

theorem Algebra.adjoin_singleton_intCast {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (n : ℤ) :

adjoin R {↑n} = ⊥

source

@[simp]

theorem Algebra.adjoin_insert_intCast {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (n : ℤ) (s : Set A) :

adjoin R (insert (↑n) s) = adjoin R s

source

theorem Algebra.adjoin_eq_ring_closure {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] (s : Set A) :

(adjoin R s).toSubring = Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)

source

theorem Algebra.mem_adjoin_iff {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {s : Set A} {x : A} :

x ∈ adjoin R s ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)

source

@[reducible, inline]

abbrev 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 ↥(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 = { toRing := (Algebra.adjoin R s).toRing, mul_comm := ⋯ }

Instances For

source

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)

source

@[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}

source

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) {s : Set A} (h : Set.EqOn (⇑φ₁) (⇑φ₂) s) :

Algebra.adjoin R s ≤ equalizer φ₁ φ₂

source

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⦄ (hs : Set.EqOn (⇑φ₁) (⇑φ₂) s) :

φ₁ = φ₂

source

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} {s : Set A} :

Set.EqOn ⇑φ ⇑ψ ↑(Algebra.adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

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

source

theorem AlgHom.adjoin_ext {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {s : Set A} ⦃φ₁ φ₂ : ↥(Algebra.adjoin R s) →ₐ[R] B⦄ (h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) :

φ₁ = φ₂

source

theorem AlgHom.ext_of_eq_adjoin {R : Type uR} {A : Type uA} {B : Type uB} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {S : Subalgebra R A} {s : Set A} (hS : S = Algebra.adjoin R s) ⦃φ₁ φ₂ : ↥S →ₐ[R] B⦄ (h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩) :

φ₁ = φ₂

source

theorem Algebra.forall_mem_adjoin_smul_eq_self_iff {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set A) {M : Type u_1} [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A] (m : M) :

(∀ x ∈ adjoin R S, m • x = x) ↔ ∀ x ∈ S, m • x = x

source

theorem Algebra.adjoin_nat {R : Type u_1} [Semiring R] (s : Set R) :

adjoin ℕ s = subalgebraOfSubsemiring (Subsemiring.closure s)

source

theorem Algebra.adjoin_int {R : Type u_1} [Ring R] (s : Set R) :

adjoin ℤ s = subalgebraOfSubring (Subring.closure s)

source

def Subsemiring.closureEquivAdjoinNat {R : Type u_1} [Semiring R] (s : Set R) :

↥(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) ⋯

Instances For

source

def Subring.closureEquivAdjoinInt {R : Type u_1} [Ring R] (s : Set R) :

↥(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) ⋯

Instances For

source

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.

source

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 : toSubmodule L = Submodule.span F S) :

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.

source

theorem NonUnitalAlgebra.adjoin_le_algebra_adjoin (R : Type uR) {A : Type uA} [CommSemiring R] [Ring A] [Algebra R A] (s : Set A) :

adjoin R s ≤ (Algebra.adjoin R s).toNonUnitalSubalgebra

source

theorem Algebra.adjoin_nonUnitalSubalgebra (R : Type uR) {A : Type uA} [CommSemiring R] [Ring A] [Algebra R A] (s : Set A) :

adjoin R ↑(NonUnitalAlgebra.adjoin R s) = adjoin R s

source

def Subalgebra.toNonUnitalSubalgebraOrderEmbedding {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] :

Subalgebra R A ↪o NonUnitalSubalgebra R A

The forgetful map from subalgebras to non-unital subalgebras, as an order embedding.

Equations

Subalgebra.toNonUnitalSubalgebraOrderEmbedding = { toFun := Subalgebra.toNonUnitalSubalgebra, inj' := ⋯, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem Subalgebra.toNonUnitalSubalgebra_le_toNonUnitalSubalgebra {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} :

S.toNonUnitalSubalgebra ≤ T.toNonUnitalSubalgebra ↔ S ≤ T

source

theorem Subalgebra.toNonUnitalSubalgebra_mono {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} :

S ≤ T → S.toNonUnitalSubalgebra ≤ T.toNonUnitalSubalgebra

Alias of the reverse direction of Subalgebra.toNonUnitalSubalgebra_le_toNonUnitalSubalgebra.

source

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) :

comap f (map f S) = S ⊔ Algebra.adjoin R (⇑f ⁻¹' {0})

source

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) :

comap f (map f S) = S

Documentation

Mathlib.Algebra.Algebra.Subalgebra.Lattice

Complete lattice structure of subalgebras #