Subalgebras over Commutative Semiring

In this file we define Subalgebras and the usual operations on them (map, comap).

More lemmas about adjoin can be found in RingTheory.Adjoin.

structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] extends Subsemiring : Type v

A subalgebra is a sub(semi)ring that includes the range of algebraMap.

• carrier : Set A
• mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• add_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• algebraMap_mem' : ∀ (r : R), (algebraMap R A) r ∈ self.carrier

  The image of algebraMap is contained in the underlying set of the subalgebra

theorem Subalgebra.algebraMap_mem' {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (self : Subalgebra R A) (r : R) : (algebraMap R A) r ∈ self.carrier

The image of algebraMap is contained in the underlying set of the subalgebra

instance Subalgebra.instSetLike {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : SetLike (Subalgebra R A) A

Equations

• Subalgebra.instSetLike = { coe := fun (s : Subalgebra R A) => s.carrier, coe_injective' := ⋯ }

instance Subalgebra.SubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : SubsemiringClass (Subalgebra R A) A

Equations

• ⋯ = ⋯

@[simp]

theorem Subalgebra.mem_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {x : A} : x ∈ S.toSubsemiring ↔ x ∈ S

theorem Subalgebra.mem_carrier {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Subalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s

theorem Subalgebra.ext {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) : S = T

@[simp]

theorem Subalgebra.coe_toSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↑S.toSubsemiring = ↑S

theorem Subalgebra.toSubsemiring_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Function.Injective Subalgebra.toSubsemiring

theorem Subalgebra.toSubsemiring_inj {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {U : Subalgebra R A} : S.toSubsemiring = U.toSubsemiring ↔ S = U

def Subalgebra.copy {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = ↑S) : Subalgebra R A

Copy of a subalgebra with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem Subalgebra.coe_copy {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem Subalgebra.copy_eq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (s : Set A) (hs : s = ↑S) : S.copy s hs = S

instance Subalgebra.instSMulMemClass {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : SMulMemClass (Subalgebra R A) R A

Equations

• ⋯ = ⋯

theorem algebraMap_mem {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R) : (algebraMap R A) r ∈ s

theorem Subalgebra.algebraMap_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (r : R) : (algebraMap R A) r ∈ S

theorem Subalgebra.rangeS_le {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : (algebraMap R A).rangeS ≤ S.toSubsemiring

theorem Subalgebra.range_subset {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Set.range ⇑(algebraMap R A) ⊆ ↑S

theorem Subalgebra.range_le {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Set.range ⇑(algebraMap R A) ≤ ↑S

theorem Subalgebra.smul_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x ∈ S) (r : R) : r • x ∈ S

theorem Subalgebra.one_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : 1 ∈ S

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

theorem Subalgebra.pow_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S

theorem Subalgebra.zero_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : 0 ∈ S

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

theorem Subalgebra.nsmul_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x ∈ S) (n : ℕ) : n • x ∈ S

theorem Subalgebra.natCast_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (n : ℕ) : ↑n ∈ S

theorem Subalgebra.list_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {L : List A} (h : ∀ x ∈ L, x ∈ S) : L.prod ∈ S

theorem Subalgebra.list_sum_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {L : List A} (h : ∀ x ∈ L, x ∈ S) : L.sum ∈ S

theorem Subalgebra.multiset_sum_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {m : Multiset A} (h : ∀ x ∈ m, x ∈ S) : m.sum ∈ S

theorem Subalgebra.sum_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) : ∑ x ∈ t, f x ∈ S

theorem Subalgebra.multiset_prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) {m : Multiset A} (h : ∀ x ∈ m, x ∈ S) : m.prod ∈ S

theorem Subalgebra.prod_mem {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) {ι : Type w} {t : Finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) : ∏ x ∈ t, f x ∈ S

instance Subalgebra.instSubringClass {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] : SubringClass (Subalgebra R A) A

Equations

• ⋯ = ⋯

theorem Subalgebra.neg_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x ∈ S) : -x ∈ S

theorem Subalgebra.sub_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) {x : A} {y : A} (hx : x ∈ S) (hy : y ∈ S) : x - y ∈ S

theorem Subalgebra.zsmul_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) {x : A} (hx : x ∈ S) (n : ℤ) : n • x ∈ S

theorem Subalgebra.intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) (n : ℤ) : ↑n ∈ S

@[deprecated natCast_mem]

theorem Subalgebra.coe_nat_mem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (n : ℕ) : ↑n ∈ S

Alias of Subalgebra.natCast_mem.

@[deprecated intCast_mem]

theorem Subalgebra.coe_int_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) (n : ℤ) : ↑n ∈ S

Alias of Subalgebra.intCast_mem.

def Subalgebra.toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : AddSubmonoid A

The projection from a subalgebra of A to an additive submonoid of A.

Equations

• S.toAddSubmonoid = S.toAddSubmonoid

def Subalgebra.toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Subring A

A subalgebra over a ring is also a Subring.

Equations

• S.toSubring = { toSubsemiring := S.toSubsemiring, neg_mem' := ⋯ }

@[simp]

theorem Subalgebra.mem_toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} {x : A} : x ∈ S.toSubring ↔ x ∈ S

@[simp]

theorem Subalgebra.coe_toSubring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : ↑S.toSubring = ↑S

theorem Subalgebra.toSubring_injective {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] : Function.Injective Subalgebra.toSubring

theorem Subalgebra.toSubring_inj {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} {U : Subalgebra R A} : S.toSubring = U.toSubring ↔ S = U

instance Subalgebra.instInhabitedSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Inhabited ↥S

Equations

• S.instInhabitedSubtypeMem = { default := 0 }

Subalgebras inherit structure from their Subsemiring / Semiring coercions.

instance Subalgebra.toSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Semiring ↥S

Equations

• S.toSemiring = S.toSemiring

instance Subalgebra.toCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) : CommSemiring ↥S

Equations

• S.toCommSemiring = S.toCommSemiring

instance Subalgebra.toRing {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : Ring ↥S

Equations

• S.toRing = S.toSubring.toRing

instance Subalgebra.toCommRing {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) : CommRing ↥S

Equations

• S.toCommRing = S.toSubring.toCommRing

def Subalgebra.toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra R A ↪o Submodule R A

The forgetful map from Subalgebra to Submodule as an OrderEmbedding

Equations

• Subalgebra.toSubmodule = { toFun := fun (S : Subalgebra R A) => { carrier := ↑S, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem Subalgebra.mem_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : A} : x ∈ Subalgebra.toSubmodule S ↔ x ∈ S

@[simp]

theorem Subalgebra.coe_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↑(Subalgebra.toSubmodule S) = ↑S

theorem Subalgebra.toSubmodule_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Function.Injective ⇑Subalgebra.toSubmodule

Subalgebras inherit structure from their Submodule coercions.

@[instance 100]

instance Subalgebra.module' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : Module R' ↥S

Equations

• S.module' = (Subalgebra.toSubmodule S).module'

instance Subalgebra.instModuleSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Module R ↥S

Equations

• S.instModuleSubtypeMem = S.module'

instance Subalgebra.instIsScalarTowerSubtypeMem {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : IsScalarTower R' R ↥S

Equations

• ⋯ = ⋯

@[instance 500]

instance Subalgebra.algebra' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] : Algebra R' ↥S

Equations

• S.algebra' = Algebra.mk ((algebraMap R' A).codRestrict S ⋯) ⋯ ⋯

instance Subalgebra.algebra {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Algebra R ↥S

Equations

• S.algebra = S.algebra'

instance Subalgebra.noZeroSMulDivisors_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R ↥S

Equations

• ⋯ = ⋯

theorem Subalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (y : ↥S) : ↑(x + y) = ↑x + ↑y

theorem Subalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (y : ↥S) : ↑(x * y) = ↑x * ↑y

theorem Subalgebra.coe_zero {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↑0 = 0

theorem Subalgebra.coe_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↑1 = 1

theorem Subalgebra.coe_neg {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (x : ↥S) : ↑(-x) = -↑x

theorem Subalgebra.coe_sub {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (x : ↥S) (y : ↥S) : ↑(x - y) = ↑x - ↑y

@[simp]

theorem Subalgebra.coe_smul {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : ↥S) : ↑(r • x) = r • ↑x

@[simp]

theorem Subalgebra.coe_algebraMap {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [CommSemiring R'] [SMul R' R] [Algebra R' A] [IsScalarTower R' R A] (r : R') : ↑((algebraMap R' ↥S) r) = (algebraMap R' A) r

theorem Subalgebra.coe_pow {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem Subalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : ↥S} : ↑x = 0 ↔ x = 0

theorem Subalgebra.coe_eq_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) {x : ↥S} : ↑x = 1 ↔ x = 1

def Subalgebra.val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↥S →ₐ[R] A

Embedding of a subalgebra into the algebra.

Equations

• S.val = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Subalgebra.coe_val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ⇑S.val = Subtype.val

theorem Subalgebra.val_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) : S.val x = ↑x

@[simp]

theorem Subalgebra.toSubsemiring_subtype {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.subtype = ↑S.val

@[simp]

theorem Subalgebra.toSubring_subtype {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : S.toSubring.subtype = ↑S.val

def Subalgebra.toSubmoduleEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : ↥(Subalgebra.toSubmodule S) ≃ₗ[R] ↥S

Linear equivalence between S : Submodule R A and S. Though these types are equal, we define it as a LinearEquiv to avoid type equalities.

Equations

• S.toSubmoduleEquiv = LinearEquiv.ofEq (Subalgebra.toSubmodule S) (Subalgebra.toSubmodule S) ⋯

def Subalgebra.map {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 : Subalgebra R A) : Subalgebra R B

Transport a subalgebra via an algebra homomorphism.

Equations

• Subalgebra.map f S = { toSubsemiring := Subsemiring.map (↑f) S.toSubsemiring, algebraMap_mem' := ⋯ }

theorem Subalgebra.map_mono {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S₁ : Subalgebra R A} {S₂ : Subalgebra R A} {f : A →ₐ[R] B} : S₁ ≤ S₂ → Subalgebra.map f S₁ ≤ Subalgebra.map f S₂

theorem Subalgebra.map_injective {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) : Function.Injective (Subalgebra.map f)

@[simp]

theorem Subalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : Subalgebra.map (AlgHom.id R A) S = S

theorem Subalgebra.map_map {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (S : Subalgebra R A) (g : B →ₐ[R] C) (f : A →ₐ[R] B) : Subalgebra.map g (Subalgebra.map f S) = Subalgebra.map (g.comp f) S

@[simp]

theorem Subalgebra.mem_map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} {y : B} : y ∈ Subalgebra.map f S ↔ ∃ x ∈ S, f x = y

theorem Subalgebra.map_toSubmodule {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} : Subalgebra.toSubmodule (Subalgebra.map f S) = Submodule.map f.toLinearMap (Subalgebra.toSubmodule S)

theorem Subalgebra.map_toSubsemiring {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} : (Subalgebra.map f S).toSubsemiring = Subsemiring.map f.toRingHom S.toSubsemiring

@[simp]

theorem Subalgebra.coe_map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) : ↑(Subalgebra.map f S) = ⇑f '' ↑S

def Subalgebra.comap {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 : Subalgebra R B) : Subalgebra R A

Preimage of a subalgebra under an algebra homomorphism.

Equations

• Subalgebra.comap f S = { toSubsemiring := Subsemiring.comap (↑f) S.toSubsemiring, algebraMap_mem' := ⋯ }

theorem Subalgebra.map_le {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] {S : Subalgebra R A} {f : A →ₐ[R] B} {U : Subalgebra R B} : Subalgebra.map f S ≤ U ↔ S ≤ Subalgebra.comap f U

theorem Subalgebra.gc_map_comap {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) : GaloisConnection (Subalgebra.map f) (Subalgebra.comap f)

@[simp]

theorem Subalgebra.mem_comap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R B) (f : A →ₐ[R] B) (x : A) : x ∈ Subalgebra.comap f S ↔ f x ∈ S

@[simp]

theorem Subalgebra.coe_comap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R B) (f : A →ₐ[R] B) : ↑(Subalgebra.comap f S) = ⇑f ⁻¹' ↑S

instance Subalgebra.noZeroDivisors {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [NoZeroDivisors A] [Algebra R A] (S : Subalgebra R A) : NoZeroDivisors ↥S

Equations

• ⋯ = ⋯

instance Subalgebra.isDomain {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [IsDomain A] [Algebra R A] (S : Subalgebra R A) : IsDomain ↥S

Equations

• ⋯ = ⋯

@[instance 75]

instance SubalgebraClass.toAlgebra {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : Algebra R ↥s

Equations

• SubalgebraClass.toAlgebra s = Algebra.mk { toFun := fun (r : R) => ⟨(algebraMap R A) r, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[simp]

theorem SubalgebraClass.coe_algebraMap {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) (r : R) : ↑((algebraMap R ↥s) r) = (algebraMap R A) r

def SubalgebraClass.val {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : ↥s →ₐ[R] A

Embedding of a subalgebra into the algebra, as an algebra homomorphism.

Equations

• SubalgebraClass.val s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem SubalgebraClass.coe_val {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [SetLike S A] [SubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : ⇑(SubalgebraClass.val s) = Subtype.val

def Submodule.toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : Subalgebra R A

A submodule containing 1 and closed under multiplication is a subalgebra.

Equations

• p.toSubalgebra h_one h_mul = { carrier := p.carrier, mul_mem' := ⋯, one_mem' := h_one, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem Submodule.mem_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] {p : Submodule R A} {h_one : 1 ∈ p} {h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p} {x : A} : x ∈ p.toSubalgebra h_one h_mul ↔ x ∈ p

@[simp]

theorem Submodule.coe_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : ↑(p.toSubalgebra h_one h_mul) = ↑p

theorem Submodule.toSubalgebra_mk {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (s : Submodule R A) (h1 : 1 ∈ s) (hmul : ∀ (x y : A), x ∈ s → y ∈ s → x * y ∈ s) : s.toSubalgebra h1 hmul = { carrier := ↑s, mul_mem' := hmul, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem Submodule.toSubalgebra_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (p : Submodule R A) (h_one : 1 ∈ p) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : Subalgebra.toSubmodule (p.toSubalgebra h_one h_mul) = p

@[simp]

theorem Subalgebra.toSubmodule_toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : (Subalgebra.toSubmodule S).toSubalgebra ⋯ ⋯ = S

def AlgHom.range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) : Subalgebra R B

Range of an AlgHom as a subalgebra.

Equations

• φ.range = { toSubsemiring := φ.rangeS, algebraMap_mem' := ⋯ }

@[simp]

theorem AlgHom.mem_range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) {y : B} : y ∈ φ.range ↔ ∃ (x : A), φ x = y

theorem AlgHom.mem_range_self {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) (x : A) : φ x ∈ φ.range

@[simp]

theorem AlgHom.coe_range {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (φ : A →ₐ[R] B) : ↑φ.range = Set.range ⇑φ

theorem AlgHom.range_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) : (g.comp f).range = Subalgebra.map g f.range

theorem AlgHom.range_comp_le_range {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) : (g.comp f).range ≤ g.range

def AlgHom.codRestrict {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 : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S) : A →ₐ[R] ↥S

Restrict the codomain of an algebra homomorphism.

Equations

• f.codRestrict S hf = { toRingHom := (↑f).codRestrict S hf, commutes' := ⋯ }

@[simp]

theorem AlgHom.val_comp_codRestrict {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 : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S) : S.val.comp (f.codRestrict S hf) = f

@[simp]

theorem AlgHom.coe_codRestrict {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 : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A) : ↑((f.codRestrict S hf) x) = f x

theorem AlgHom.injective_codRestrict {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 : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S) : Function.Injective ⇑(f.codRestrict S hf) ↔ Function.Injective ⇑f

@[reducible, inline]

abbrev AlgHom.rangeRestrict {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) : A →ₐ[R] ↥f.range

Restrict the codomain of an AlgHom f to f.range.

This is the bundled version of Set.rangeFactorization.

Equations

• f.rangeRestrict = f.codRestrict f.range ⋯

theorem AlgHom.rangeRestrict_surjective {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) : Function.Surjective ⇑f.rangeRestrict

instance AlgHom.fintypeRange {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Fintype A] [DecidableEq B] (φ : A →ₐ[R] B) : Fintype ↥φ.range

The range of a morphism of algebras is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with Subtype.fintype if B is also a fintype.

Equations

• φ.fintypeRange = Set.fintypeRange ⇑φ

def AlgEquiv.ofLeftInverse {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g ⇑f) : A ≃ₐ[R] ↥f.range

Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.

This is a computable alternative to AlgEquiv.ofInjective.

Equations

• AlgEquiv.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := g ∘ ⇑f.range.val, left_inv := h, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.ofLeftInverse_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g ⇑f) (x : A) : ↑((AlgEquiv.ofLeftInverse h) x) = f x

@[simp]

theorem AlgEquiv.ofLeftInverse_symm_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g ⇑f) (x : ↥f.range) : (AlgEquiv.ofLeftInverse h).symm x = g ↑x

noncomputable def AlgEquiv.ofInjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) : A ≃ₐ[R] ↥f.range

Restrict an injective algebra homomorphism to an algebra isomorphism

Equations

• AlgEquiv.ofInjective f hf = AlgEquiv.ofLeftInverse ⋯

@[simp]

theorem AlgEquiv.ofInjective_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (x : A) : ↑((AlgEquiv.ofInjective f hf) x) = f x

noncomputable def AlgEquiv.ofInjectiveField {R : Type u} [CommSemiring R] {E : Type u_1} {F : Type u_2} [DivisionRing E] [Semiring F] [Nontrivial F] [Algebra R E] [Algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] ↥f.range

Restrict an algebra homomorphism between fields to an algebra isomorphism

Equations

• AlgEquiv.ofInjectiveField f = AlgEquiv.ofInjective f ⋯

def AlgEquiv.subalgebraMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) : ↥S ≃ₐ[R] ↥(Subalgebra.map (↑e) S)

Given an equivalence e : A ≃ₐ[R] B of R-algebras and a subalgebra S of A, subalgebraMap is the induced equivalence between S and S.map e

Equations

• e.subalgebraMap S = { toEquiv := (e.toRingEquiv.subsemiringMap S.toSubsemiring).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.subalgebraMap_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (x : ↑↑S.toAddSubmonoid) : ↑((e.subalgebraMap S) x) = e ↑x

@[simp]

theorem AlgEquiv.subalgebraMap_symm_apply_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A) (y : ↑(⇑↑e.toRingEquiv.toAddEquiv '' ↑S.toAddSubmonoid)) : ↑((e.subalgebraMap S).symm y) = (↑↑e).symm ↑y

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' := ⋯ }

@[simp]

theorem Algebra.adjoin_toSubsemiring (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) : (Algebra.adjoin R s).toSubsemiring = Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s)

theorem Algebra.gc {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : GaloisConnection (Algebra.adjoin R) SetLike.coe

def Algebra.gi {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : GaloisInsertion (Algebra.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 := ⋯ }

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

Equations

• Algebra.instCompleteLatticeSubalgebra = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

theorem Algebra.sSup_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Set (Subalgebra R A)) : sSup S = Algebra.adjoin R (⋃₀ (SetLike.coe '' S))

@[simp]

theorem Algebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : ↑⊤ = Set.univ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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 = ⊤

@[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 = ⊤

@[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 = ⊤

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

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

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

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 : Subalgebra R A) (T : Subalgebra R A) : Subalgebra.map f (S ⊔ T) = Subalgebra.map f S ⊔ Subalgebra.map f T

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 : Subalgebra R A) (T : Subalgebra R A) : Subalgebra.map f (S ⊓ T) = Subalgebra.map f S ⊓ Subalgebra.map f T

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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)

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

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

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

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

Equations

• Algebra.instInhabitedSubalgebra = { default := ⊥ }

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)

theorem Algebra.toSubmodule_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra.toSubmodule ⊥ = 1

@[simp]

theorem Algebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : ↑⊥ = Set.range ⇑(algebraMap R A)

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

theorem Algebra.range_top_iff_surjective {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

@[simp]

theorem Algebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : (AlgHom.id R A).range = ⊤

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

@[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 ⊥ = ⊥

@[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 ⊤ = ⊤

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 ⊤ ⋯

theorem Algebra.surjective_algebraMap_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Function.Surjective ⇑(algebraMap R A) ↔ ⊤ = ⊥

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) ↔ ⊤ = ⊥

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

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 ⋯

@[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), (Algebra.botEquiv F R).symm a = (Algebra.ofId F ↥⊥) a

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 ⋯ ⋯

@[simp]

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

@[simp]

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

instance Subalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [Subsingleton A] : Subsingleton (Subalgebra R A)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

theorem Subalgebra.range_val {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.val.range = S

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

Equations

• Subalgebra.instUnique = { toInhabited := inferInstanceAs (Inhabited (Subalgebra R R)), uniq := ⋯ }

def Subalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S ≤ T) : ↥S →ₐ[R] ↥T

The map S → T when S is a subalgebra contained in the subalgebra T.

This is the subalgebra version of Submodule.inclusion, or Subring.inclusion

Equations

• Subalgebra.inclusion h = { toFun := Set.inclusion h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem Subalgebra.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S ≤ T) : Function.Injective ⇑(Subalgebra.inclusion h)

@[simp]

theorem Subalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} : Subalgebra.inclusion ⋯ = AlgHom.id R ↥S

@[simp]

theorem Subalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) : (Subalgebra.inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩

theorem Subalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S) : (Subalgebra.inclusion h) ⟨↑x, m⟩ = x

@[simp]

theorem Subalgebra.inclusion_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} {U : Subalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S) : (Subalgebra.inclusion htu) ((Subalgebra.inclusion hst) x) = (Subalgebra.inclusion ⋯) x

@[simp]

theorem Subalgebra.coe_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} {T : Subalgebra R A} (h : S ≤ T) (s : ↥S) : ↑((Subalgebra.inclusion h) s) = ↑s

def Subalgebra.equivOfEq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (h : S = T) : ↥S ≃ₐ[R] ↥T

Two subalgebras that are equal are also equivalent as algebras.

This is the Subalgebra version of LinearEquiv.ofEq and Equiv.Set.ofEq.

Equations

• S.equivOfEq T h = { toFun := fun (x : ↥S) => ⟨↑x, ⋯⟩, invFun := fun (x : ↥T) => ⟨↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Subalgebra.equivOfEq_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (h : S = T) (x : ↥S) : (S.equivOfEq T h) x = ⟨↑x, ⋯⟩

@[simp]

theorem Subalgebra.equivOfEq_symm {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (h : S = T) : (S.equivOfEq T h).symm = T.equivOfEq S ⋯

@[simp]

theorem Subalgebra.equivOfEq_rfl {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : S.equivOfEq S ⋯ = AlgEquiv.refl

@[simp]

theorem Subalgebra.equivOfEq_trans {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (T : Subalgebra R A) (U : Subalgebra R A) (hST : S = T) (hTU : T = U) : (S.equivOfEq T hST).trans (T.equivOfEq U hTU) = S.equivOfEq U ⋯

theorem Subalgebra.range_comp_val {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) : (f.comp S.val).range = Subalgebra.map f S

noncomputable def Subalgebra.equivMapOfInjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) : ↥S ≃ₐ[R] ↥(Subalgebra.map f S)

A subalgebra is isomorphic to its image under an injective AlgHom

Equations

• S.equivMapOfInjective f hf = (AlgEquiv.ofInjective (f.comp S.val) ⋯).trans ((f.comp S.val).range.equivOfEq (Subalgebra.map f S) ⋯)

@[simp]

theorem Subalgebra.coe_equivMapOfInjective_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (S : Subalgebra R A) (f : A →ₐ[R] B) (hf : Function.Injective ⇑f) (x : ↥S) : ↑((S.equivMapOfInjective f hf) x) = f ↑x

Actions by Subalgebras

These are just copies of the definitions about Subsemiring starting from Subring.mulAction.

instance Subalgebra.instSMulSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] (S : Subalgebra R A) : SMul (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.instSMulSubtypeMem = inferInstanceAs (SMul (↥S.toSubsemiring) α)

theorem Subalgebra.smul_def {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] {S : Subalgebra R A} (g : ↥S) (m : α) : g • m = ↑g • m

instance Subalgebra.smulCommClass_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} {β : Type u_2} [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) : SMulCommClass (↥S) α β

Equations

• ⋯ = ⋯

instance Subalgebra.smulCommClass_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} {β : Type u_2} [SMul α β] [SMul A β] [SMulCommClass α A β] (S : Subalgebra R A) : SMulCommClass α (↥S) β

Equations

• ⋯ = ⋯

instance Subalgebra.isScalarTower_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} {β : Type u_2} [SMul α β] [SMul A α] [SMul A β] [IsScalarTower A α β] (S : Subalgebra R A) : IsScalarTower (↥S) α β

Note that this provides IsScalarTower S R R which is needed by smul_mul_assoc.

Equations

• ⋯ = ⋯

instance Subalgebra.isScalarTower_mid {R : Type u_3} {S : Type u_4} {T : Type u_5} [CommSemiring R] [Semiring S] [AddCommMonoid T] [Algebra R S] [Module R T] [Module S T] [IsScalarTower R S T] (S' : Subalgebra R S) : IsScalarTower R (↥S') T

Equations

• ⋯ = ⋯

instance Subalgebra.instFaithfulSMulSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [SMul A α] [FaithfulSMul A α] (S : Subalgebra R A) : FaithfulSMul (↥S) α

Equations

• ⋯ = ⋯

instance Subalgebra.instMulActionSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [MulAction A α] (S : Subalgebra R A) : MulAction (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.instMulActionSubtypeMem = inferInstanceAs (MulAction (↥S.toSubsemiring) α)

instance Subalgebra.instDistribMulActionSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [AddMonoid α] [DistribMulAction A α] (S : Subalgebra R A) : DistribMulAction (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.instDistribMulActionSubtypeMem = inferInstanceAs (DistribMulAction (↥S.toSubsemiring) α)

instance Subalgebra.instSMulWithZeroSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [Zero α] [SMulWithZero A α] (S : Subalgebra R A) : SMulWithZero (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.instSMulWithZeroSubtypeMem = inferInstanceAs (SMulWithZero (↥S.toSubsemiring) α)

instance Subalgebra.instMulActionWithZeroSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [Zero α] [MulActionWithZero A α] (S : Subalgebra R A) : MulActionWithZero (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.instMulActionWithZeroSubtypeMem = inferInstanceAs (MulActionWithZero (↥S.toSubsemiring) α)

instance Subalgebra.moduleLeft {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_1} [AddCommMonoid α] [Module A α] (S : Subalgebra R A) : Module (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.moduleLeft = inferInstanceAs (Module (↥S.toSubsemiring) α)

instance Subalgebra.toAlgebra {α : Type u_1} {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α] (S : Subalgebra R A) : Algebra (↥S) α

The action by a subalgebra is the action by the underlying algebra.

Equations

• S.toAlgebra = Algebra.ofSubsemiring S.toSubsemiring

theorem Subalgebra.algebraMap_eq {α : Type u_1} {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring α] [Algebra R A] [Algebra A α] (S : Subalgebra R A) : algebraMap (↥S) α = (algebraMap A α).comp ↑S.val

@[simp]

theorem Subalgebra.rangeS_algebraMap {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) : (algebraMap (↥S) A).rangeS = S.toSubsemiring

@[simp]

theorem Subalgebra.range_algebraMap {R : Type u_3} {A : Type u_4} [CommRing R] [CommRing A] [Algebra R A] (S : Subalgebra R A) : (algebraMap (↥S) A).range = S.toSubring

instance Subalgebra.noZeroSMulDivisors_top {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] [NoZeroDivisors A] (S : Subalgebra R A) : NoZeroSMulDivisors (↥S) A

Equations

• ⋯ = ⋯

theorem Set.algebraMap_mem_center {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R A) r ∈ Set.center A

def Subalgebra.center (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra R A

The center of an algebra is the set of elements which commute with every element. They form a subalgebra.

Equations

• Subalgebra.center R A = { toSubsemiring := Subsemiring.center A, algebraMap_mem' := ⋯ }

theorem Subalgebra.coe_center (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : ↑(Subalgebra.center R A) = Set.center A

@[simp]

theorem Subalgebra.center_toSubsemiring (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : (Subalgebra.center R A).toSubsemiring = Subsemiring.center A

@[simp]

theorem Subalgebra.center_toSubring (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] : (Subalgebra.center R A).toSubring = Subring.center A

@[simp]

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

instance Subalgebra.instCommSemiringSubtypeMemCenter {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : CommSemiring ↥(Subalgebra.center R A)

Equations

• Subalgebra.instCommSemiringSubtypeMemCenter = inferInstanceAs (CommSemiring ↥(Subsemiring.center A))

instance Subalgebra.instCommRingSubtypeMemCenter {R : Type u} [CommSemiring R] {A : Type u_1} [Ring A] [Algebra R A] : CommRing ↥(Subalgebra.center R A)

Equations

• Subalgebra.instCommRingSubtypeMemCenter = inferInstanceAs (CommRing ↥(Subring.center A))

theorem Subalgebra.mem_center_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} : a ∈ Subalgebra.center R A ↔ ∀ (b : A), b * a = a * b

@[simp]

theorem Set.algebraMap_mem_centralizer {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} (r : R) : (algebraMap R A) r ∈ s.centralizer

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

The centralizer of a set as a subalgebra.

Equations

• Subalgebra.centralizer R s = { toSubsemiring := Subsemiring.centralizer s, algebraMap_mem' := ⋯ }

@[simp]

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

theorem Subalgebra.mem_centralizer_iff (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} {z : A} : z ∈ Subalgebra.centralizer R s ↔ ∀ g ∈ s, g * z = z * g

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

theorem Subalgebra.centralizer_le (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Set A) (t : Set A) (h : s ⊆ t) : Subalgebra.centralizer R t ≤ Subalgebra.centralizer R s

@[simp]

theorem Subalgebra.centralizer_eq_top_iff_subset (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : Subalgebra.centralizer R s = ⊤ ↔ s ⊆ ↑(Subalgebra.center R A)

@[simp]

theorem Subalgebra.centralizer_univ (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : Subalgebra.centralizer R Set.univ = Subalgebra.center R A

theorem Subalgebra.le_centralizer_centralizer (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {s : Subalgebra R A} : s ≤ Subalgebra.centralizer R ↑(Subalgebra.centralizer R ↑s)

@[simp]

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

def subalgebraOfSubsemiring {R : Type u_1} [Semiring R] (S : Subsemiring R) : Subalgebra ℕ R

A subsemiring is an ℕ-subalgebra.

Equations

• subalgebraOfSubsemiring S = { toSubsemiring := S, algebraMap_mem' := ⋯ }

@[simp]

theorem mem_subalgebraOfSubsemiring {R : Type u_1} [Semiring R] {x : R} {S : Subsemiring R} : x ∈ subalgebraOfSubsemiring S ↔ x ∈ S

def subalgebraOfSubring {R : Type u_1} [Ring R] (S : Subring R) : Subalgebra ℤ R

A subring is a ℤ-subalgebra.

Equations

• subalgebraOfSubring S = { toSubsemiring := S.toSubsemiring, algebraMap_mem' := ⋯ }

@[simp]

theorem mem_subalgebraOfSubring {R : Type u_1} [Ring R] {x : R} {S : Subring R} : x ∈ subalgebraOfSubring S ↔ x ∈ S

def AlgHom.equalizer {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} (ϕ : F) (ψ : F) [FunLike F A B] [AlgHomClass F R A B] : Subalgebra R A

The equalizer of two R-algebra homomorphisms

Equations

• AlgHom.equalizer ϕ ψ = { carrier := {a : A | ϕ a = ψ a}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem AlgHom.mem_equalizer {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) (ψ : F) (x : A) : x ∈ AlgHom.equalizer φ ψ ↔ φ x = ψ x

theorem AlgHom.equalizer_toSubmodule {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} {ψ : F} : Subalgebra.toSubmodule (AlgHom.equalizer φ ψ) = LinearMap.eqLocus φ ψ

@[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} {ψ : F} : AlgHom.equalizer φ ψ = ⊤ ↔ φ = ψ

@[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) : AlgHom.equalizer φ φ = ⊤

theorem AlgHom.le_equalizer {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} {ψ : F} {S : Subalgebra R A} : S ≤ AlgHom.equalizer φ ψ ↔ Set.EqOn ⇑φ ⇑ψ ↑S

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} {ψ : F} {S : Subalgebra R A} {T : Subalgebra R A} (hS : Set.EqOn ⇑φ ⇑ψ ↑S) (hT : Set.EqOn ⇑φ ⇑ψ ↑T) : Set.EqOn ⇑φ ⇑ψ ↑(S ⊔ T)

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} {ψ : F} {S : Subalgebra R A} {T : Subalgebra R A} (hST : Codisjoint S T) (hS : Set.EqOn ⇑φ ⇑ψ ↑S) (hT : Set.EqOn ⇑φ ⇑ψ ↑T) : φ = ψ

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) : Subalgebra.map f (Subalgebra.comap f S) = S ⊓ f.range

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) : Subalgebra.map f (Subalgebra.comap f S) = S

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) : Subalgebra.map f (Subalgebra.comap f S) = S

theorem Subalgebra.comap_map_eq_self_of_injective {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.Injective ⇑f) (S : Subalgebra R A) : Subalgebra.comap f (Subalgebra.map f S) = S