Subalgebras over Commutative Semiring

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

The Algebra.adjoin operation and complete lattice structure can be found in Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean.

structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] extends Subsemiring A : 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

@[implicit_reducible]

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

@[implicit_reducible]

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

Equations

• Subalgebra.instPartialOrder = PartialOrder.ofSetLike (Subalgebra R A) A

@[simp]

theorem Subalgebra.coe_mk {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Subsemiring A) (h : ∀ (r : R), (algebraMap R A) r ∈ s.carrier) : ↑{ toSubsemiring := s, algebraMap_mem' := h } = ↑s

@[simp]

theorem Subalgebra.mem_mk {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (s : Subsemiring A) (h : ∀ (r : R), (algebraMap R A) r ∈ s.carrier) (x : A) : x ∈ { toSubsemiring := s, algebraMap_mem' := h } ↔ x ∈ s

def Subalgebra.ofClass {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] [SMulMemClass S R A] (s : S) : Subalgebra R A

The actual Subalgebra obtained from an element of a type satisfying SubsemiringClass and SMulMemClass.

Equations

• Subalgebra.ofClass s = { carrier := ↑s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

@[simp]

theorem Subalgebra.coe_ofClass {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] [SMulMemClass S R A] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance Subalgebra.instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : CanLift (Set A) (Subalgebra R A) SetLike.coe fun (s : Set A) => (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R), (algebraMap R A) r ∈ s

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

@[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 T : Subalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) : S = T

theorem Subalgebra.ext_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} : S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ 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 toSubsemiring

theorem Subalgebra.toSubsemiring_inj {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S 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.copy_toSubsemiring {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).toSubsemiring = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_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

@[simp]

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

@[reducible]

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

Turn a Subalgebra into a NonUnitalSubalgebra by forgetting that it contains 1.

Equations

• S.toNonUnitalSubalgebra = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

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

@[simp]

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

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

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

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

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

@[reducible]

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

@[reducible]

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

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

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 toSubring

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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 ∈ 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) : ↑(toSubmodule S) = ↑S

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

Subalgebras inherit structure from their Submodule coercions.

@[implicit_reducible, 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' = inferInstance

@[implicit_reducible]

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 = inferInstance

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

@[implicit_reducible, 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' = { toSMul := DistribMulAction.toDistribSMul.toSMul, algebraMap := (algebraMap R' A).codRestrict S ⋯, commutes' := ⋯, smul_def' := ⋯ }

@[implicit_reducible]

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'

@[simp]

theorem Subalgebra.mk_algebraMap {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S : Subalgebra R A} (r : R) (hr : (algebraMap R A) r ∈ S) : ⟨(algebraMap R A) r, hr⟩ = (algebraMap R ↥S) r

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

theorem Subalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) (x 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 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 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) [SMul R' R] [SMul 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) : ↥(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' := ⋯ }

@[simp]

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] (f : A →ₐ[R] B) (S : Subalgebra R A) : (map f S).toSubsemiring = Subsemiring.map (↑f) 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] (f : A →ₐ[R] B) (S : Subalgebra R A) : ↑(map f S) = ⇑f '' ↑S

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₁ S₂ : Subalgebra R A} {f : A →ₐ[R] B} : S₁ ≤ S₂ → map f S₁ ≤ 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 (map f)

@[simp]

theorem Subalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) : 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) : map g (map f S) = 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 ∈ 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} : toSubmodule (map f S) = Submodule.map f.toLinearMap (toSubmodule 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' := ⋯ }

@[simp]

theorem Subalgebra.comap_toSubsemiring {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) : (comap f S).toSubsemiring = Subsemiring.comap (↑f) S.toSubsemiring

@[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] (f : A →ₐ[R] B) (S : Subalgebra R B) : ↑(comap f S) = ⇑f ⁻¹' ↑S

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} : map f S ≤ U ↔ S ≤ 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 (map f) (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 ∈ comap f S ↔ f x ∈ 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

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

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

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

@[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) : ⇑(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.toSubalgebra_toSubsemiring {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).toSubsemiring = { carrier := p.carrier, mul_mem' := ⋯, one_mem' := h_one, add_mem' := ⋯, zero_mem' := ⋯ }

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

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

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) : (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.range_toSubsemiring {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.toSubsemiring = (↑φ).rangeS

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

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

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.val_comp_rangeRestrict {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.val.comp φ.rangeRestrict = φ

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

@[implicit_reducible]

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) : ↑((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) : (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) : ↑((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_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

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

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

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

def Subalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S 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 T : Subalgebra R A} (h : S ≤ T) : Function.Injective ⇑(inclusion h)

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Subalgebra.val_comp_inclusion {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (hst : S ≤ T) : T.val.comp (inclusion hst) = S.val

@[simp]

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

theorem Subalgebra.inclusion.isScalarTower_left {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S ≤ T) (X : Type u_1) [SMul X R] [SMul X A] [IsScalarTower X R A] : IsScalarTower X ↥S ↥T

theorem Subalgebra.inclusion.isScalarTower_right {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {S T : Subalgebra R A} (h : S ≤ T) (X : Type u_1) [MulAction A X] : IsScalarTower (↥S) (↥T) X

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

def Subalgebra.equivOfEq {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (S 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.setCongr.

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 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 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 T 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 = map f S

def AlgHom.subalgebraMap {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) : ↥S →ₐ[R] ↥(Subalgebra.map f S)

An AlgHom between two rings restricts to an AlgHom from any subalgebra of the domain onto the image of that subalgebra.

Equations

• AlgHom.subalgebraMap S f = (f.comp S.val).codRestrict (Subalgebra.map f S) ⋯

@[simp]

theorem AlgHom.subalgebraMap_coe_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) (x : ↥S) : ↑((subalgebraMap S f) x) = f ↑x

theorem AlgHom.subalgebraMap_surjective {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) : Function.Surjective ⇑(subalgebraMap S f)

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] ↥(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.

@[implicit_reducible]

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 = { smul := fun (m : ↥S.toSubsemiring) (a : α) => ↑m • a }

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) α β

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

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

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

@[instance 100]

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

@[instance 100]

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

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

@[implicit_reducible]

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 = { toSemigroupAction := (Submonoid.instMulActionSubtypeMem S).toSemigroupAction, one_smul := ⋯ }

@[implicit_reducible]

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 = { toMulAction := S.instMulActionSubtypeMem, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

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 = { toSMulZeroClass := (Subsemiring.instSMulWithZeroSubtypeMem S).toSMulZeroClass, zero_smul := ⋯ }

@[implicit_reducible]

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 = { toMulAction := S.instMulActionSubtypeMem, smul_zero := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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 = { toDistribMulAction := S.instDistribMulActionSubtypeMem, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

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

theorem Subalgebra.algebraMap_def {α : 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} (s : ↥S) : (algebraMap (↥S) α) s = (algebraMap A α) ↑s

@[simp]

theorem Subalgebra.algebraMap_mk {α : 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} (a : A) (ha : a ∈ S) : (algebraMap (↥S) α) ⟨a, ha⟩ = (algebraMap A α) a

@[simp]

theorem Subalgebra.algebraMap_apply {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) (x : ↥S) : (algebraMap (↥S) A) x = ↑x

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

@[simp]

theorem Subalgebra.setRange_algebraMap {R : Type u_3} {A : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Subalgebra R A) : Set.range ⇑(algebraMap (↥S) A) = ↑S

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

theorem Set.algebraMap_mem_center {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R A) r ∈ 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' := ⋯ }

@[simp]

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

@[simp]

theorem Subalgebra.center_toSubsemiring (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : (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] : (center R A).toSubring = Subring.center A

@[implicit_reducible]

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

Equations

• Subalgebra.instCommSemiringSubtypeMemCenter = { toSemiring := (Subalgebra.center R A).toSemiring, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

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

theorem Subalgebra.mem_center_iff {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] {a : A} : a ∈ 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) : ↑(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 ∈ 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) : center R A ≤ centralizer R s

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

@[simp]

theorem Subalgebra.centralizer_univ (R : Type u) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : centralizer R Set.univ = 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 ≤ centralizer R ↑(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} : centralizer R s.centralizer.centralizer = 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 subalgebraOfSubsemiring_toSubsemiring {R : Type u_1} [Semiring R] (S : Subsemiring R) : (subalgebraOfSubsemiring S).toSubsemiring = S

@[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 subalgebraOfSubring_toSubsemiring {R : Type u_1} [Ring R] (S : Subring R) : (subalgebraOfSubring S).toSubsemiring = S.toSubsemiring

@[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) [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.coe_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) [FunLike F A B] [AlgHomClass F R A B] : ↑(equalizer ϕ ψ) = {a : A | ϕ a = ψ a}

@[simp]

theorem AlgHom.equalizer_toSubsemiring {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) [FunLike F A B] [AlgHomClass F R A B] : (equalizer ϕ ψ).toSubsemiring = { carrier := {a : A | ϕ a = ψ a}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_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) (x : A) : x ∈ 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} : Subalgebra.toSubmodule (equalizer φ ψ) = LinearMap.eqLocus φ ψ

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} {S : Subalgebra R A} : S ≤ equalizer φ ψ ↔ Set.EqOn ⇑φ ⇑ψ ↑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) : comap f (map f S) = S

def NonUnitalSubalgebra.toSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : NonUnitalSubalgebra R A) (h1 : 1 ∈ S) : Subalgebra R A

Turn a non-unital subalgebra containing 1 into a subalgebra.

Equations

• S.toSubalgebra h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

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

theorem NonUnitalSubalgebra.toSubalgebra_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : NonUnitalSubalgebra R A) (h1 : 1 ∈ S) : (S.toSubalgebra h1).toNonUnitalSubalgebra = S