Non-unital Subalgebras over Commutative Semirings

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

TODO

• once we have scalar actions by semigroups (as opposed to monoids), implement the action of a non-unital subalgebra on the larger algebra.

def NonUnitalSubalgebraClass.subtype {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : ↥s →ₙₐ[R] A

Embedding of a non-unital subalgebra into the non-unital algebra.

Equations

• NonUnitalSubalgebraClass.subtype s = { toFun := Subtype.val, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalSubalgebraClass.subtype_apply {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] {s : S} (x : ↥s) : (subtype s) x = ↑x

theorem NonUnitalSubalgebraClass.subtype_injective {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : Function.Injective ⇑(subtype s)

@[simp]

theorem NonUnitalSubalgebraClass.coe_subtype {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A] (s : S) : ⇑(subtype s) = Subtype.val

structure NonUnitalSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] extends NonUnitalSubsemiring A, Submodule R A : Type v

A non-unital subalgebra is a sub(semi)ring that is also a submodule.

• carrier : Set A
• add_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• smul_mem' (c : R) {x : A} : x ∈ self.carrier → c • x ∈ self.carrier

theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective toNonUnitalSubsemiring

@[simp]

theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s t : NonUnitalSubalgebra R A} : s.toNonUnitalSubsemiring = t.toNonUnitalSubsemiring ↔ s = t

instance NonUnitalSubalgebra.instSetLike {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : SetLike (NonUnitalSubalgebra R A) A

Equations

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

theorem NonUnitalSubalgebra.toSubmodule_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective toSubmodule

theorem NonUnitalSubalgebra.toSubmodule_inj {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s t : NonUnitalSubalgebra R A} : s.toSubmodule = t.toSubmodule ↔ s = t

def NonUnitalSubalgebra.ofClass {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [SMulMemClass S R A] (s : S) : NonUnitalSubalgebra R A

The actual NonUnitalSubalgebra obtained from an element of a type satisfying NonUnitalSubsemiringClass and SMulMemClass.

Equations

• NonUnitalSubalgebra.ofClass s = { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem NonUnitalSubalgebra.ofClass_carrier {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SetLike S A] [NonUnitalSubsemiringClass S A] [SMulMemClass S R A] (s : S) : ↑(ofClass s) = ↑s

@[instance 100]

instance NonUnitalSubalgebra.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallForallHSMul {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : CanLift (Set A) (NonUnitalSubalgebra R A) SetLike.coe fun (s : Set A) => 0 ∈ s ∧ (∀ {x y : A}, x ∈ s → y ∈ s → x + y ∈ s) ∧ (∀ {x y : A}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ (r : R) {x : A}, x ∈ s → r • x ∈ s

instance NonUnitalSubalgebra.instNonUnitalSubsemiringClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubsemiringClass (NonUnitalSubalgebra R A) A

instance NonUnitalSubalgebra.instSMulMemClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : SMulMemClass (NonUnitalSubalgebra R A) R A

theorem NonUnitalSubalgebra.mem_carrier {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {s : NonUnitalSubalgebra R A} {x : A} : x ∈ s.carrier ↔ x ∈ s

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

theorem NonUnitalSubalgebra.ext_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S T : NonUnitalSubalgebra R A} : S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T

@[simp]

theorem NonUnitalSubalgebra.mem_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} : x ∈ S.toNonUnitalSubsemiring ↔ x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toNonUnitalSubsemiring = ↑S

theorem NonUnitalSubalgebra.mem_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) {x : A} : x ∈ S.toSubmodule ↔ x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toSubmodule = ↑S

def NonUnitalSubalgebra.copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : NonUnitalSubalgebra R A

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

Equations

• S.copy s hs = { toNonUnitalSubsemiring := S.copy s hs, smul_mem' := ⋯ }

@[simp]

theorem NonUnitalSubalgebra.coe_copy {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : ↑(S.copy s hs) = s

theorem NonUnitalSubalgebra.copy_eq {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) (s : Set A) (hs : s = ↑S) : S.copy s hs = S

instance NonUnitalSubalgebra.instInhabitedSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : Inhabited ↥S

Equations

• S.instInhabitedSubtypeMem = { default := 0 }

instance NonUnitalSubalgebra.instNonUnitalSubringClass {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : NonUnitalSubringClass (NonUnitalSubalgebra R A) A

def NonUnitalSubalgebra.toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubring A

A non-unital subalgebra over a ring is also a Subring.

Equations

• S.toNonUnitalSubring = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, neg_mem' := ⋯ }

@[simp]

theorem NonUnitalSubalgebra.mem_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S : NonUnitalSubalgebra R A} {x : A} : x ∈ S.toNonUnitalSubring ↔ x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_toNonUnitalSubring {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) : ↑S.toNonUnitalSubring = ↑S

theorem NonUnitalSubalgebra.toNonUnitalSubring_injective {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : Function.Injective toNonUnitalSubring

theorem NonUnitalSubalgebra.toNonUnitalSubring_inj {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S U : NonUnitalSubalgebra R A} : S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U

NonUnitalSubalgebras inherit structure from their NonUnitalSubsemiring / Semiring coercions.

instance NonUnitalSubalgebra.toNonUnitalNonAssocSemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalNonAssocSemiring ↥S

Equations

• S.toNonUnitalNonAssocSemiring = inferInstance

instance NonUnitalSubalgebra.toNonUnitalSemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSemiring ↥S

Equations

• S.toNonUnitalSemiring = inferInstance

instance NonUnitalSubalgebra.toNonUnitalCommSemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalCommSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalCommSemiring ↥S

Equations

• S.toNonUnitalCommSemiring = inferInstance

instance NonUnitalSubalgebra.toNonUnitalNonAssocRing {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalNonAssocRing ↥S

Equations

• S.toNonUnitalNonAssocRing = inferInstance

instance NonUnitalSubalgebra.toNonUnitalRing {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalRing ↥S

Equations

• S.toNonUnitalRing = inferInstance

instance NonUnitalSubalgebra.toNonUnitalCommRing {R : Type u} {A : Type v} [CommRing R] [NonUnitalCommRing A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalCommRing ↥S

Equations

• S.toNonUnitalCommRing = inferInstance

def NonUnitalSubalgebra.toSubmodule' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o Submodule R A

The forgetful map from NonUnitalSubalgebra to Submodule as an OrderEmbedding

Equations

• NonUnitalSubalgebra.toSubmodule' = { toFun := fun (S : NonUnitalSubalgebra R A) => S.toSubmodule, inj' := ⋯, map_rel_iff' := ⋯ }

def NonUnitalSubalgebra.toNonUnitalSubsemiring' {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : NonUnitalSubalgebra R A ↪o NonUnitalSubsemiring A

The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring as an OrderEmbedding

Equations

• NonUnitalSubalgebra.toNonUnitalSubsemiring' = { toFun := fun (S : NonUnitalSubalgebra R A) => S.toNonUnitalSubsemiring, inj' := ⋯, map_rel_iff' := ⋯ }

def NonUnitalSubalgebra.toNonUnitalSubring' {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] : NonUnitalSubalgebra R A ↪o NonUnitalSubring A

The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring as an OrderEmbedding

Equations

• NonUnitalSubalgebra.toNonUnitalSubring' = { toFun := fun (S : NonUnitalSubalgebra R A) => S.toNonUnitalSubring, inj' := ⋯, map_rel_iff' := ⋯ }

NonUnitalSubalgebras inherit structure from their Submodule coercions.

instance NonUnitalSubalgebra.instModule' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : Module R' ↥S

Equations

• NonUnitalSubalgebra.instModule' = SMulMemClass.toModule' (NonUnitalSubalgebra R A) R' R A S

instance NonUnitalSubalgebra.instModule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : Module R ↥S

Equations

• NonUnitalSubalgebra.instModule = NonUnitalSubalgebra.instModule'

instance NonUnitalSubalgebra.instIsScalarTower' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : IsScalarTower R' R ↥S

instance NonUnitalSubalgebra.instIsScalarTowerSubtypeMem {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [IsScalarTower R A A] : IsScalarTower R ↥S ↥S

instance NonUnitalSubalgebra.instSMulCommClass' {R' : Type u'} {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SMulCommClass R' R A] : SMulCommClass R' R ↥S

instance NonUnitalSubalgebra.instSMulCommClass {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [SMulCommClass R A A] : SMulCommClass R ↥S ↥S

instance NonUnitalSubalgebra.instIsTorsionFree {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [Module.IsTorsionFree R A] : Module.IsTorsionFree R ↥S

theorem NonUnitalSubalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x y : ↥S) : ↑(x + y) = ↑x + ↑y

theorem NonUnitalSubalgebra.coe_mul {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x y : ↥S) : ↑(x * y) = ↑x * ↑y

theorem NonUnitalSubalgebra.coe_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : ↑0 = 0

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

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

@[simp]

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

theorem NonUnitalSubalgebra.coe_eq_zero {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {x : ↥S} : ↑x = 0 ↔ x = 0

@[simp]

theorem NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} : NonUnitalSubsemiringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)

@[simp]

theorem NonUnitalSubalgebra.toSubring_subtype {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubringClass.subtype S = ↑(NonUnitalSubalgebraClass.subtype S)

def NonUnitalSubalgebra.toSubmoduleEquiv {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : ↥S.toSubmodule ≃ₗ[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 S.toSubmodule S.toSubmodule ⋯

def NonUnitalSubalgebra.map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra R B

Transport a non-unital subalgebra via an algebra homomorphism.

Equations

• NonUnitalSubalgebra.map f S = { toNonUnitalSubsemiring := NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring, smul_mem' := ⋯ }

theorem NonUnitalSubalgebra.map_mono {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S₁ S₂ : NonUnitalSubalgebra R A} {f : F} : S₁ ≤ S₂ → map f S₁ ≤ map f S₂

theorem NonUnitalSubalgebra.map_injective {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {f : F} (hf : Function.Injective ⇑f) : Function.Injective (map f)

@[simp]

theorem NonUnitalSubalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : map (NonUnitalAlgHom.id R A) S = S

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

@[simp]

theorem NonUnitalSubalgebra.mem_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {y : B} : y ∈ map f S ↔ ∃ x ∈ S, f x = y

theorem NonUnitalSubalgebra.map_toSubmodule {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule

theorem NonUnitalSubalgebra.map_toNonUnitalSubsemiring {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} : (map f S).toNonUnitalSubsemiring = NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring

@[simp]

theorem NonUnitalSubalgebra.coe_map {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R A) (f : F) : ↑(map f S) = ⇑f '' ↑S

def NonUnitalSubalgebra.comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R A

Preimage of a non-unital subalgebra under an algebra homomorphism.

Equations

• NonUnitalSubalgebra.comap f S = { toNonUnitalSubsemiring := NonUnitalSubsemiring.comap (↑f) S.toNonUnitalSubsemiring, smul_mem' := ⋯ }

theorem NonUnitalSubalgebra.map_le {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F} {U : NonUnitalSubalgebra R B} : map f S ≤ U ↔ S ≤ comap f U

theorem NonUnitalSubalgebra.gc_map_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : GaloisConnection (map f) (comap f)

@[simp]

theorem NonUnitalSubalgebra.mem_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) (x : A) : x ∈ comap f S ↔ f x ∈ S

@[simp]

theorem NonUnitalSubalgebra.coe_comap {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (S : NonUnitalSubalgebra R B) (f : F) : ↑(comap f S) = ⇑f ⁻¹' ↑S

instance NonUnitalSubalgebra.noZeroDivisors {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [NoZeroDivisors A] [Module R A] (S : NonUnitalSubalgebra R A) : NoZeroDivisors ↥S

def Submodule.toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : NonUnitalSubalgebra R A

A submodule closed under multiplication is a non-unital subalgebra.

Equations

• p.toNonUnitalSubalgebra h_mul = { toAddSubmonoid := p.toAddSubmonoid, mul_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Submodule.mem_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {p : Submodule R A} {h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p} {x : A} : x ∈ p.toNonUnitalSubalgebra h_mul ↔ x ∈ p

@[simp]

theorem Submodule.coe_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : ↑(p.toNonUnitalSubalgebra h_mul) = ↑p

theorem Submodule.toNonUnitalSubalgebra_mk {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (hmul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : p.toNonUnitalSubalgebra hmul = { carrier := ↑p, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Submodule.toNonUnitalSubalgebra_toSubmodule {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) : (p.toNonUnitalSubalgebra h_mul).toSubmodule = p

@[simp]

theorem NonUnitalSubalgebra.toSubmodule_toNonUnitalSubalgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : S.toSubmodule.toNonUnitalSubalgebra ⋯ = S

def NonUnitalAlgHom.range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) : NonUnitalSubalgebra R B

Range of an NonUnitalAlgHom as a non-unital subalgebra.

Equations

• NonUnitalAlgHom.range φ = { toNonUnitalSubsemiring := NonUnitalRingHom.srange ↑φ, smul_mem' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.mem_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) {y : B} : y ∈ NonUnitalAlgHom.range φ ↔ ∃ (x : A), φ x = y

theorem NonUnitalAlgHom.mem_range_self {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (x : A) : φ x ∈ NonUnitalAlgHom.range φ

@[simp]

theorem NonUnitalAlgHom.coe_range {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) : ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ

theorem NonUnitalAlgHom.range_comp {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalNonAssocSemiring C] [Module R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) : NonUnitalAlgHom.range (g.comp f) = NonUnitalSubalgebra.map g (NonUnitalAlgHom.range f)

theorem NonUnitalAlgHom.range_comp_le_range {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [NonUnitalNonAssocSemiring C] [Module R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) : NonUnitalAlgHom.range (g.comp f) ≤ NonUnitalAlgHom.range g

def NonUnitalAlgHom.codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : A →ₙₐ[R] ↥S

Restrict the codomain of a non-unital algebra homomorphism.

Equations

• NonUnitalAlgHom.codRestrict f S hf = { toFun := (NonUnitalRingHom.codRestrict (↑f) S.toNonUnitalSubsemiring hf).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.subtype_comp_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : (NonUnitalSubalgebraClass.subtype S).comp (codRestrict f S hf) = NonUnitalAlgHomClass.toNonUnitalAlgHom f

@[simp]

theorem NonUnitalAlgHom.coe_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A) : ↑((codRestrict f S hf) x) = f x

theorem NonUnitalAlgHom.injective_codRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) : Function.Injective ⇑(codRestrict f S hf) ↔ Function.Injective ⇑f

@[reducible, inline]

abbrev NonUnitalAlgHom.rangeRestrict {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : A →ₙₐ[R] ↥(NonUnitalAlgHom.range f)

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

This is the bundled version of Set.rangeFactorization.

Equations

• NonUnitalAlgHom.rangeRestrict f = NonUnitalAlgHom.codRestrict f (NonUnitalAlgHom.range f) ⋯

def NonUnitalAlgHom.equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (ϕ ψ : F) : NonUnitalSubalgebra R A

The equalizer of two non-unital R-algebra homomorphisms

Equations

• NonUnitalAlgHom.equalizer ϕ ψ = { carrier := {a : A | ϕ a = ψ a}, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem NonUnitalAlgHom.mem_equalizer {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ ψ : F) (x : A) : x ∈ equalizer φ ψ ↔ φ x = ψ x

instance NonUnitalAlgHom.fintypeRange {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [Fintype A] [DecidableEq B] (φ : F) : Fintype ↥(NonUnitalAlgHom.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

• NonUnitalAlgHom.fintypeRange φ = Set.fintypeRange ⇑φ

@[simp]

theorem NonUnitalAlgebra.span_eq_toSubmodule (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (s : NonUnitalSubalgebra R A) : Submodule.span R ↑s = s.toSubmodule

def NonUnitalAlgebra.adjoin (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : NonUnitalSubalgebra R A

The minimal non-unital subalgebra that includes s.

Equations

• NonUnitalAlgebra.adjoin R s = { toAddSubmonoid := (Submodule.span R ↑(NonUnitalSubsemiring.closure s)).toAddSubmonoid, mul_mem' := ⋯, smul_mem' := ⋯ }

theorem NonUnitalAlgebra.adjoin_toSubmodule (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : (adjoin R s).toSubmodule = Submodule.span R ↑(NonUnitalSubsemiring.closure s)

@[simp]

theorem NonUnitalAlgebra.subset_adjoin (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} : s ⊆ ↑(adjoin R s)

theorem NonUnitalAlgebra.mem_adjoin_of_mem (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {x : A} (hx : x ∈ s) : x ∈ adjoin R s

@[simp]

theorem NonUnitalAlgebra.self_mem_adjoin_singleton (R : Type u) {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : A) : x ∈ adjoin R {x}

theorem NonUnitalAlgebra.gc {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : GaloisConnection (adjoin R) SetLike.coe

def NonUnitalAlgebra.gi {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : GaloisInsertion (adjoin R) SetLike.coe

Galois insertion between adjoin and SetLike.coe.

Equations

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

instance NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : CompleteLattice (NonUnitalSubalgebra R A)

Equations

• NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra = NonUnitalAlgebra.gi.liftCompleteLattice

theorem NonUnitalAlgebra.adjoin_le {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {s : Set A} (hs : s ⊆ ↑S) : adjoin R s ≤ S

@[simp]

theorem NonUnitalAlgebra.adjoin_le_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} {s : Set A} : adjoin R s ≤ S ↔ s ⊆ ↑S

theorem NonUnitalAlgebra.adjoin_mono {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s t : Set A} (H : s ⊆ t) : adjoin R s ≤ adjoin R t

theorem NonUnitalAlgebra.adjoin_union {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s t : Set A) : adjoin R (s ∪ t) = adjoin R s ⊔ adjoin R t

@[simp]

theorem NonUnitalAlgebra.adjoin_eq {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : NonUnitalSubalgebra R A) : adjoin R ↑s = s

theorem NonUnitalAlgebra.adjoin_induction {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : (x : A) → x ∈ adjoin R s → Prop} (mem : ∀ (x : A) (hx : x ∈ s), p x ⋯) (add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯) {x : A} (hx : x ∈ adjoin R s) : p x hx

If some predicate holds for all x ∈ (s : Set A) and this predicate is closed under the algebraMap, addition, multiplication and star operations, then it holds for a ∈ adjoin R s.

theorem NonUnitalAlgebra.adjoin_induction₂ {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop} (mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) (zero_left : ∀ (x : A) (hx : x ∈ adjoin R s), p 0 x ⋯ hx) (zero_right : ∀ (x : A) (hx : x ∈ adjoin R s), p x 0 hx ⋯) (add_left : ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) (add_right : ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) (mul_left : ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (smul_left : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p (r • x) y ⋯ hy) (smul_right : ∀ (r : R) (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x y hx hy → p x (r • y) hx ⋯) {x y : A} (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) : p x y hx hy

theorem NonUnitalAlgebra.adjoin_eq_span {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : (adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure s)

@[simp]

theorem NonUnitalAlgebra.adjoin_empty (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : adjoin R ∅ = ⊥

@[simp]

theorem NonUnitalAlgebra.adjoin_univ (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : adjoin R Set.univ = ⊤

theorem NonUnitalAlgHom.map_adjoin {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (s : Set A) : NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (⇑f '' s)

@[simp]

theorem NonUnitalAlgHom.map_adjoin_singleton {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (x : A) : NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R {x}) = NonUnitalAlgebra.adjoin R {f x}

@[simp]

theorem NonUnitalAlgebra.coe_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑⊤ = Set.univ

@[simp]

theorem NonUnitalAlgebra.mem_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} : x ∈ ⊤

@[simp]

theorem NonUnitalAlgebra.top_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toSubmodule = ⊤

@[simp]

theorem NonUnitalAlgebra.top_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toNonUnitalSubsemiring = ⊤

@[simp]

theorem NonUnitalAlgebra.toNonUnitalSubring_top {R : Type u_2} {A : Type u_3} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toNonUnitalSubring = ⊤

@[deprecated NonUnitalAlgebra.toNonUnitalSubring_top (since := "2026-01-03")]

theorem NonUnitalAlgebra.top_toSubring {R : Type u_2} {A : Type u_3} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊤.toNonUnitalSubring = ⊤

Alias of NonUnitalAlgebra.toNonUnitalSubring_top.

@[simp]

theorem NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤

theorem NonUnitalAlgebra.toSubmodule_eq_top {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : S.toSubmodule = ⊤ ↔ S = ⊤

@[simp]

theorem NonUnitalAlgebra.toNonUnitalSubring_eq_top {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} : S.toNonUnitalSubring = ⊤ ↔ S = ⊤

@[deprecated NonUnitalAlgebra.toNonUnitalSubring_eq_top (since := "2026-01-01")]

theorem NonUnitalAlgebra.to_subring_eq_top {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] {S : NonUnitalSubalgebra R A} : S.toNonUnitalSubring = ⊤ ↔ S = ⊤

Alias of NonUnitalAlgebra.toNonUnitalSubring_eq_top.

theorem NonUnitalAlgebra.mem_sup_left {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A} : x ∈ S → x ∈ S ⊔ T

theorem NonUnitalAlgebra.mem_sup_right {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A} : x ∈ T → x ∈ S ⊔ T

theorem NonUnitalAlgebra.mul_mem_sup {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T) : x * y ∈ S ⊔ T

theorem NonUnitalAlgebra.map_sup {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (S T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊔ T) = NonUnitalSubalgebra.map f S ⊔ NonUnitalSubalgebra.map f T

theorem NonUnitalAlgebra.map_inf {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective ⇑f) (S T : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (S ⊓ T) = NonUnitalSubalgebra.map f S ⊓ NonUnitalSubalgebra.map f T

@[simp]

theorem NonUnitalAlgebra.coe_inf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S T : NonUnitalSubalgebra R A) : ↑(S ⊓ T) = ↑S ∩ ↑T

@[simp]

theorem NonUnitalAlgebra.mem_inf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} {x : A} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

@[simp]

theorem NonUnitalAlgebra.inf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S T : NonUnitalSubalgebra R A) : (S ⊓ T).toSubmodule = S.toSubmodule ⊓ T.toSubmodule

@[simp]

theorem NonUnitalAlgebra.inf_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S T : NonUnitalSubalgebra R A) : (S ⊓ T).toNonUnitalSubsemiring = S.toNonUnitalSubsemiring ⊓ T.toNonUnitalSubsemiring

@[simp]

theorem NonUnitalAlgebra.coe_sInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) : ↑(sInf S) = ⋂ s ∈ S, ↑s

@[simp]

theorem NonUnitalAlgebra.mem_sInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : Set (NonUnitalSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

@[simp]

theorem NonUnitalAlgebra.sInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) : (sInf S).toSubmodule = sInf (NonUnitalSubalgebra.toSubmodule '' S)

@[simp]

theorem NonUnitalAlgebra.sInf_toNonUnitalSubsemiring {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)) : (sInf S).toNonUnitalSubsemiring = sInf (NonUnitalSubalgebra.toNonUnitalSubsemiring '' S)

@[simp]

theorem NonUnitalAlgebra.coe_iInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} {S : ι → NonUnitalSubalgebra R A} : ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

@[simp]

theorem NonUnitalAlgebra.mem_iInf {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} {S : ι → NonUnitalSubalgebra R A} {x : A} : x ∈ ⨅ (i : ι), S i ↔ ∀ (i : ι), x ∈ S i

theorem NonUnitalAlgebra.map_iInf {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} [Nonempty ι] [IsScalarTower R B B] [SMulCommClass R B B] (f : F) (hf : Function.Injective ⇑f) (S : ι → NonUnitalSubalgebra R A) : NonUnitalSubalgebra.map f (⨅ (i : ι), S i) = ⨅ (i : ι), NonUnitalSubalgebra.map f (S i)

@[simp]

theorem NonUnitalAlgebra.iInf_toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_2} (S : ι → NonUnitalSubalgebra R A) : (⨅ (i : ι), S i).toSubmodule = ⨅ (i : ι), (S i).toSubmodule

instance NonUnitalAlgebra.instInhabitedNonUnitalSubalgebra {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Inhabited (NonUnitalSubalgebra R A)

Equations

• NonUnitalAlgebra.instInhabitedNonUnitalSubalgebra = { default := ⊥ }

theorem NonUnitalAlgebra.mem_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} : x ∈ ⊥ ↔ x = 0

theorem NonUnitalAlgebra.toSubmodule_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ⊥.toSubmodule = ⊥

@[simp]

theorem NonUnitalAlgebra.coe_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑⊥ = {0}

theorem NonUnitalAlgebra.eq_top_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : S = ⊤ ↔ ∀ (x : A), x ∈ S

@[simp]

theorem NonUnitalAlgebra.range_id {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalAlgHom.range (NonUnitalAlgHom.id R A) = ⊤

@[simp]

theorem NonUnitalAlgebra.map_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map f ⊤ = NonUnitalAlgHom.range f

@[simp]

theorem NonUnitalAlgebra.map_bot {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.map f ⊥ = ⊥

@[simp]

theorem NonUnitalAlgebra.comap_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalSubalgebra.comap f ⊤ = ⊤

def NonUnitalAlgebra.toTop {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : A →ₙₐ[R] ↥⊤

NonUnitalAlgHom to ⊤ : NonUnitalSubalgebra R A.

Equations

• NonUnitalAlgebra.toTop = NonUnitalAlgHom.codRestrict (NonUnitalAlgHom.id R A) ⊤ ⋯

theorem NonUnitalAlgebra.range_eq_top (R : Type u) {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : NonUnitalAlgHom.range f = ⊤ ↔ Function.Surjective ⇑f

theorem NonUnitalSubalgebra.range_val {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalAlgHom.range (NonUnitalSubalgebraClass.subtype S) = S

instance NonUnitalSubalgebra.subsingleton_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Subsingleton A] : Subsingleton (NonUnitalSubalgebra R A)

def NonUnitalSubalgebra.prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NonUnitalNonAssocSemiring B] [Module R B] (S₁ : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R (A × B)

The product of two non-unital subalgebras is a non-unital subalgebra.

Equations

• S.prod S₁ = { carrier := ↑S ×ˢ ↑S₁, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem NonUnitalSubalgebra.coe_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NonUnitalNonAssocSemiring B] [Module R B] (S₁ : NonUnitalSubalgebra R B) : ↑(S.prod S₁) = ↑S ×ˢ ↑S₁

theorem NonUnitalSubalgebra.prod_toSubmodule {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) [NonUnitalNonAssocSemiring B] [Module R B] (S₁ : NonUnitalSubalgebra R B) : (S.prod S₁).toSubmodule = S.toSubmodule.prod S₁.toSubmodule

@[simp]

theorem NonUnitalSubalgebra.mem_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] {S : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {x : A × B} : x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁

@[simp]

theorem NonUnitalSubalgebra.prod_top {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] : ⊤.prod ⊤ = ⊤

theorem NonUnitalSubalgebra.prod_mono {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} : S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁

@[simp]

theorem NonUnitalSubalgebra.prod_inf_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [IsScalarTower R B B] [SMulCommClass R B B] {S T : NonUnitalSubalgebra R A} {S₁ T₁ : NonUnitalSubalgebra R B} : S.prod S₁ ⊓ T.prod T₁ = (S ⊓ T).prod (S₁ ⊓ T₁)

instance NonUnitalAlgHom.subsingleton {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] [Subsingleton (NonUnitalSubalgebra R A)] : Subsingleton (A →ₙₐ[R] B)

def NonUnitalSubalgebra.inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) : ↥S →ₙₐ[R] ↥T

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

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

Equations

• NonUnitalSubalgebra.inclusion h = { toFun := Set.inclusion h, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

theorem NonUnitalSubalgebra.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) : Function.Injective ⇑(inclusion h)

@[simp]

theorem NonUnitalSubalgebra.inclusion_self {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S : NonUnitalSubalgebra R A} : inclusion ⋯ = NonUnitalAlgHom.id R ↥S

@[simp]

theorem NonUnitalSubalgebra.inclusion_mk {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) : (inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩

theorem NonUnitalSubalgebra.inclusion_right {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S) : (inclusion h) ⟨↑x, m⟩ = x

@[simp]

theorem NonUnitalSubalgebra.inclusion_inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T U : NonUnitalSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S) : (inclusion htu) ((inclusion hst) x) = (inclusion ⋯) x

@[simp]

theorem NonUnitalSubalgebra.coe_inclusion {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {S T : NonUnitalSubalgebra R A} (h : S ≤ T) (s : ↥S) : ↑((inclusion h) s) = ↑s

theorem NonUnitalSubalgebra.coe_iSup_of_directed {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {S : ι → NonUnitalSubalgebra R A} (dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) S) : ↑(iSup S) = ⋃ (i : ι), ↑(S i)

noncomputable def NonUnitalSubalgebra.iSupLift {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K) (f : (i : ι) → ↥(K i) →ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)) (T : NonUnitalSubalgebra R A) (hT : T = iSup K) : ↥T →ₙₐ[R] B

Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining it on each non-unital subalgebra, and proving that it agrees on the intersection of non-unital subalgebras.

Equations

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

@[simp]

theorem NonUnitalSubalgebra.iSupLift_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (h : K i ≤ T) : (iSupLift K dir f hf T hT) ((inclusion h) x) = (f i) x

@[simp]

theorem NonUnitalSubalgebra.iSupLift_comp_inclusion {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) : (iSupLift K dir f hf T hT).comp (inclusion h) = f i

@[simp]

theorem NonUnitalSubalgebra.iSupLift_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T) : (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

theorem NonUnitalSubalgebra.iSupLift_of_mem {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [NonUnitalNonAssocSemiring B] [Module R B] [IsScalarTower R A A] [SMulCommClass R A A] {ι : Sort u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : ↥T) (hx : ↑x ∈ K i) : (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

theorem Set.smul_mem_center {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (r : R) {a : A} (ha : a ∈ center A) : r • a ∈ center A

def NonUnitalSubalgebra.center (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalSubalgebra R A

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

Equations

• NonUnitalSubalgebra.center R A = { toNonUnitalSubsemiring := NonUnitalSubsemiring.center A, smul_mem' := ⋯ }

theorem NonUnitalSubalgebra.coe_center {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↑(center R A) = Set.center A

instance NonUnitalSubalgebra.center.instNonUnitalCommSemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommSemiring ↥(center R A)

The center of a non-unital algebra is commutative and associative

Equations

• NonUnitalSubalgebra.center.instNonUnitalCommSemiring = NonUnitalSubsemiring.center.instNonUnitalCommSemiring A

instance NonUnitalSubalgebra.center.instNonUnitalCommRing {R : Type u_1} [CommSemiring R] {A : Type u_3} [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : NonUnitalCommRing ↥(center R A)

Equations

• NonUnitalSubalgebra.center.instNonUnitalCommRing = NonUnitalSubring.center.instNonUnitalCommRing A

@[simp]

theorem NonUnitalSubalgebra.center_toNonUnitalSubsemiring {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A

@[simp]

theorem NonUnitalSubalgebra.center_toNonUnitalSubring (R : Type u_3) (A : Type u_4) [CommRing R] [NonUnitalNonAssocRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (center R A).toNonUnitalSubring = NonUnitalSubring.center A

@[simp]

theorem NonUnitalSubalgebra.center_eq_top (R : Type u_1) [CommSemiring R] (A : Type u_3) [NonUnitalCommSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : center R A = ⊤

theorem NonUnitalSubalgebra.mem_center_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a : A} : a ∈ center R A ↔ ∀ (b : A), b * a = a * b

@[simp]

theorem Set.smul_mem_centralizer {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (r : R) {a : A} (ha : a ∈ s.centralizer) : r • a ∈ s.centralizer

def NonUnitalSubalgebra.centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : NonUnitalSubalgebra R A

The centralizer of a set as a non-unital subalgebra.

Equations

• NonUnitalSubalgebra.centralizer R s = { toNonUnitalSubsemiring := NonUnitalSubsemiring.centralizer s, smul_mem' := ⋯ }

@[simp]

theorem NonUnitalSubalgebra.coe_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : ↑(centralizer R s) = s.centralizer

theorem NonUnitalSubalgebra.mem_centralizer_iff (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} {z : A} : z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g

theorem NonUnitalSubalgebra.centralizer_le (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s t : Set A) (h : s ⊆ t) : centralizer R t ≤ centralizer R s

@[simp]

theorem NonUnitalSubalgebra.centralizer_univ (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : centralizer R Set.univ = center R A

theorem NonUnitalAlgebra.adjoin_le_centralizer_centralizer (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (s : Set A) : adjoin R s ≤ NonUnitalSubalgebra.centralizer R ↑(NonUnitalSubalgebra.centralizer R s)

theorem NonUnitalAlgebra.commute_of_mem_adjoin_of_forall_mem_commute {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a b : A} {s : Set A} (hb : b ∈ adjoin R s) (h : ∀ b ∈ s, Commute a b) : Commute a b

theorem NonUnitalAlgebra.commute_of_mem_adjoin_singleton_of_commute {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a b c : A} (hc : c ∈ adjoin R {b}) (h : Commute a b) : Commute a c

theorem NonUnitalAlgebra.commute_of_mem_adjoin_self {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {a b : A} (hb : b ∈ adjoin R {a}) : Commute a b

@[reducible, inline]

abbrev NonUnitalAlgebra.adjoinNonUnitalCommSemiringOfComm (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : NonUnitalCommSemiring ↥(adjoin R s)

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

See note [reducible non-instances].

Equations

• NonUnitalAlgebra.adjoinNonUnitalCommSemiringOfComm R hcomm = { toNonUnitalSemiring := (NonUnitalAlgebra.adjoin R s).toNonUnitalSemiring, mul_comm := ⋯ }

@[reducible, inline]

abbrev NonUnitalAlgebra.adjoinNonUnitalCommRingOfComm (R : Type u_3) {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {s : Set A} (hcomm : ∀ a ∈ s, ∀ b ∈ s, a * b = b * a) : NonUnitalCommRing ↥(adjoin R s)

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

See note [reducible non-instances].

Equations

• NonUnitalAlgebra.adjoinNonUnitalCommRingOfComm R hcomm = { toNonUnitalRing := (NonUnitalAlgebra.adjoin R s).toNonUnitalRing, mul_comm := ⋯ }

def nonUnitalSubalgebraOfNonUnitalSubsemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] (S : NonUnitalSubsemiring R) : NonUnitalSubalgebra ℕ R

A non-unital subsemiring is a non-unital ℕ-subalgebra.

Equations

• nonUnitalSubalgebraOfNonUnitalSubsemiring S = { toNonUnitalSubsemiring := S, smul_mem' := ⋯ }

@[simp]

theorem mem_nonUnitalSubalgebraOfNonUnitalSubsemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] {x : R} {S : NonUnitalSubsemiring R} : x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S

def nonUnitalSubalgebraOfNonUnitalSubring {R : Type u_1} [NonUnitalNonAssocRing R] (S : NonUnitalSubring R) : NonUnitalSubalgebra ℤ R

A non-unital subring is a non-unital ℤ-subalgebra.

Equations

• nonUnitalSubalgebraOfNonUnitalSubring S = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, smul_mem' := ⋯ }

@[simp]

theorem mem_nonUnitalSubalgebraOfNonUnitalSubring {R : Type u_1} [NonUnitalNonAssocRing R] {x : R} {S : NonUnitalSubring R} : x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S