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.

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

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

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

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

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

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

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

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

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

@[simp]

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

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.toSubring_toSubsemiring {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) : S.toSubring.toSubsemiring = S.toSubsemiring

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

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

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

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

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

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

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

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

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

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

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

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

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

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] {α : 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.

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

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

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

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.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.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_toSubring (R : Type u_1) (A : Type u_2) [CommRing R] [Ring A] [Algebra R A] : (center R A).toSubring = Subring.center A

instance Subalgebra.instCommSemiringSubtypeMemCenter {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : CommSemiring ↥(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 ↥(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 ∈ 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