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) : { x : A // x ∈ 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.coeSubtype {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) : ⇑(NonUnitalSubalgebraClass.subtype s) = Subtype.val

structure NonUnitalSubalgebra (R : Type u) (A : Type v) [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] extends NonUnitalSubsemiring : 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

  The carrier set is closed under scalar multiplication.

@[reducible]

abbrev NonUnitalSubalgebra.toSubmodule {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (self : NonUnitalSubalgebra R A) : Submodule R A

Reinterpret a NonUnitalSubalgebra as a Submodule.

Equations

• self.toSubmodule = { toAddSubmonoid := self.toAddSubmonoid, smul_mem' := ⋯ }

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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_iff {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} : S = T ↔ ∀ (x : A), x ∈ S ↔ x ∈ T

theorem NonUnitalSubalgebra.ext {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : ∀ (x : A), x ∈ S ↔ x ∈ T) : S = 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.toNonUnitalSubsemiring_injective {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] : Function.Injective NonUnitalSubalgebra.toNonUnitalSubsemiring

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

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

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

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

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 { x : A // x ∈ 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

Equations

• ⋯ = ⋯

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

theorem NonUnitalSubalgebra.toNonUnitalSubring_inj {R : Type u} {A : Type v} [CommRing R] [NonUnitalNonAssocRing A] [Module R A] {S : NonUnitalSubalgebra R A} {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 { x : A // x ∈ 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 { x : A // x ∈ 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 { x : A // x ∈ 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 { x : A // x ∈ 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 { x : A // x ∈ 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 { x : A // x ∈ 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' { x : A // x ∈ 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 { x : A // x ∈ 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 { x : A // x ∈ S }

Equations

• ⋯ = ⋯

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 { x : A // x ∈ S } { x : A // x ∈ S }

Equations

• ⋯ = ⋯

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 { x : A // x ∈ S }

Equations

• ⋯ = ⋯

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 { x : A // x ∈ S } { x : A // x ∈ S }

Equations

• ⋯ = ⋯

instance NonUnitalSubalgebra.noZeroSMulDivisors_bot {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R { x : A // x ∈ S }

Equations

• ⋯ = ⋯

theorem NonUnitalSubalgebra.coe_add {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] {S : NonUnitalSubalgebra R A} (x : { x : A // x ∈ S }) (y : { x : A // x ∈ 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 : { x : A // x ∈ S }) (y : { x : A // x ∈ 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 : { x : 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 : { x : A // x ∈ S }) (y : { x : A // x ∈ 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} [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] (r : R') (x : { x : A // 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 : { x : 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) : { x : A // x ∈ S.toSubmodule } ≃ₗ[R] { x : A // x ∈ 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₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalSubalgebra R A} {f : F} : S₁ ≤ S₂ → NonUnitalSubalgebra.map f S₁ ≤ NonUnitalSubalgebra.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 (NonUnitalSubalgebra.map f)

@[simp]

theorem NonUnitalSubalgebra.map_id {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] (S : NonUnitalSubalgebra R A) : NonUnitalSubalgebra.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) : NonUnitalSubalgebra.map g (NonUnitalSubalgebra.map f S) = NonUnitalSubalgebra.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 ∈ NonUnitalSubalgebra.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} : (NonUnitalSubalgebra.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} : (NonUnitalSubalgebra.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) : ↑(NonUnitalSubalgebra.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} : NonUnitalSubalgebra.map f S ≤ U ↔ S ≤ NonUnitalSubalgebra.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 (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.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 ∈ NonUnitalSubalgebra.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) : ↑(NonUnitalSubalgebra.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 { x : A // x ∈ S }

Equations

• ⋯ = ⋯

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] { x : B // x ∈ 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 (NonUnitalAlgHom.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) : ↑((NonUnitalAlgHom.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 ⇑(NonUnitalAlgHom.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] { x : B // x ∈ 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) (ψ : 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) (ψ : F) (x : A) : x ∈ NonUnitalAlgHom.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 { x : B // x ∈ 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) : (NonUnitalAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(NonUnitalSubsemiring.closure s)

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 ⊆ ↑(NonUnitalAlgebra.adjoin R s)

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 ∈ NonUnitalAlgebra.adjoin R {x}

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 : A → Prop} {a : A} (h : a ∈ NonUnitalAlgebra.adjoin R s) (mem : ∀ x ∈ s, p x) (add : ∀ (x y : A), p x → p y → p (x + y)) (zero : p 0) (mul : ∀ (x y : A), p x → p y → p (x * y)) (smul : ∀ (r : R) (x : A), p x → p (r • x)) : p a

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 : A → A → Prop} {a : A} {b : A} (ha : a ∈ NonUnitalAlgebra.adjoin R s) (hb : b ∈ NonUnitalAlgebra.adjoin R s) (Hs : ∀ x ∈ s, ∀ y ∈ s, p x y) (H0_left : ∀ (y : A), p 0 y) (H0_right : ∀ (x : A), p x 0) (Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y) (Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)) (Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y) (Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)) (Hsmul_left : ∀ (r : R) (x y : A), p x y → p (r • x) y) (Hsmul_right : ∀ (r : R) (x y : A), p x y → p x (r • y)) : p a b

theorem NonUnitalAlgebra.adjoin_induction_subtype {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 ∈ NonUnitalAlgebra.adjoin R s } → Prop} (a : { x : A // x ∈ NonUnitalAlgebra.adjoin R s }) (mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) (add : ∀ (x y : { x : A // x ∈ NonUnitalAlgebra.adjoin R s }), p x → p y → p (x + y)) (zero : p 0) (mul : ∀ (x y : { x : A // x ∈ NonUnitalAlgebra.adjoin R s }), p x → p y → p (x * y)) (smul : ∀ (r : R) (x : { x : A // x ∈ NonUnitalAlgebra.adjoin R s }), p x → p (r • x)) : p a

The difference with NonUnitalAlgebra.adjoin_induction is that this acts on the subtype.

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 ∈ NonUnitalAlgebra.adjoin R s → Prop} (mem : ∀ (x : A) (h : x ∈ s), p x ⋯) (add : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (y : A) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) (zero : p 0 ⋯) (mul : ∀ (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s) (y : A) (hy : y ∈ NonUnitalAlgebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) (smul : ∀ (r : R) (x : A) (hx : x ∈ NonUnitalAlgebra.adjoin R s), p x hx → p (r • x) ⋯) {a : A} (ha : a ∈ NonUnitalAlgebra.adjoin R s) : p a ha

A dependent version of NonUnitalAlgebra.adjoin_induction.

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 (NonUnitalAlgebra.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 (NonUnitalAlgebra.adjoin R) SetLike.coe

Galois insertion between adjoin and Subtype.val.

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

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} : NonUnitalAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S

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 : Set A) (t : Set A) : NonUnitalAlgebra.adjoin R (s ∪ t) = NonUnitalAlgebra.adjoin R s ⊔ NonUnitalAlgebra.adjoin R t

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) : NonUnitalAlgebra.adjoin R ↑s = s

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) : (NonUnitalAlgebra.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] : NonUnitalAlgebra.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] : NonUnitalAlgebra.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.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 = ⊤

@[simp]

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

@[simp]

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

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 : NonUnitalSubalgebra R A} {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 : NonUnitalSubalgebra R A} {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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {x : A} {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 : NonUnitalSubalgebra R A) (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 : NonUnitalSubalgebra R A) (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 : NonUnitalSubalgebra R A} {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 : NonUnitalSubalgebra R A) (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 : NonUnitalSubalgebra R A) (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

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)

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

@[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] { x : A // x ∈ ⊤ }

NonUnitalAlgHom to ⊤ : NonUnitalSubalgebra R A.

Equations

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

theorem NonUnitalAlgebra.range_top_iff_surjective (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)

Equations

• ⋯ = ⋯

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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {S₁ : NonUnitalSubalgebra R B} {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)

Equations

• ⋯ = ⋯

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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) : { x : A // x ∈ S } →ₙₐ[R] { x : A // x ∈ 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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) : Function.Injective ⇑(NonUnitalSubalgebra.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} : NonUnitalSubalgebra.inclusion ⋯ = NonUnitalAlgHom.id R { x : A // x ∈ 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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : A) (hx : x ∈ S) : (NonUnitalSubalgebra.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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) (x : { x : A // x ∈ T }) (m : ↑x ∈ S) : (NonUnitalSubalgebra.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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} {U : NonUnitalSubalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : { x : A // x ∈ S }) : (NonUnitalSubalgebra.inclusion htu) ((NonUnitalSubalgebra.inclusion hst) x) = (NonUnitalSubalgebra.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 : NonUnitalSubalgebra R A} {T : NonUnitalSubalgebra R A} (h : S ≤ T) (s : { x : A // x ∈ S }) : ↑((NonUnitalSubalgebra.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] {ι : Type 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] {ι : Type u_1} [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K) (f : (i : ι) → { x : A // x ∈ K i } →ₙₐ[R] B) (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)) (T : NonUnitalSubalgebra R A) (hT : T = iSup K) : { x : A // x ∈ 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] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → { x : A // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : { x : A // x ∈ K i }) (h : K i ≤ T) : (NonUnitalSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalSubalgebra.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] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → { x : A // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (h : K i ≤ T) : (NonUnitalSubalgebra.iSupLift K dir f hf T hT).comp (NonUnitalSubalgebra.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] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → { x : A // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : { x : A // x ∈ K i }) (hx : ↑x ∈ T) : (NonUnitalSubalgebra.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] {ι : Type u_1} [Nonempty ι] {K : ι → NonUnitalSubalgebra R A} {dir : Directed (fun (x1 x2 : NonUnitalSubalgebra R A) => x1 ≤ x2) K} {f : (i : ι) → { x : A // x ∈ K i } →ₙₐ[R] B} {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A} {hT : T = iSup K} {i : ι} (x : { x : A // x ∈ T }) (hx : ↑x ∈ K i) : (NonUnitalSubalgebra.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 ∈ Set.center A) : r • a ∈ Set.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] : ↑(NonUnitalSubalgebra.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 { x : A // x ∈ NonUnitalSubalgebra.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 { x : A // x ∈ NonUnitalSubalgebra.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] : (NonUnitalSubalgebra.center R A).toNonUnitalSubsemiring = NonUnitalSubsemiring.center A

@[simp]

theorem NonUnitalSubalgebra.center_toNonUnitalSubring (R : Type u_3) (A : Type u_4) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (NonUnitalSubalgebra.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] : NonUnitalSubalgebra.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 ∈ NonUnitalSubalgebra.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) : ↑(NonUnitalSubalgebra.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 ∈ NonUnitalSubalgebra.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 : Set A) (t : Set A) (h : s ⊆ t) : NonUnitalSubalgebra.centralizer R t ≤ NonUnitalSubalgebra.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] : NonUnitalSubalgebra.centralizer R Set.univ = NonUnitalSubalgebra.center R A

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