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

Instances For

source

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

⇑(subtype s) = Subtype.val

source

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

Instances For

source

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

source

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

NonUnitalSubsemiringClass (NonUnitalSubalgebra R A) A

source

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

SMulMemClass (NonUnitalSubalgebra R A) R A

source

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

source

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

source

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

source

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

source

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

Function.Injective toNonUnitalSubsemiring

source

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

S.toNonUnitalSubsemiring = U.toNonUnitalSubsemiring ↔ S = U

source

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

source

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

source

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

Function.Injective toSubmodule

source

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

S.toSubmodule = U.toSubmodule ↔ S = U

source

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

Instances For

source

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

source

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

source

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 }

source

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

NonUnitalSubringClass (NonUnitalSubalgebra R A) A

source

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

Instances For

source

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

source

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

source

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

Function.Injective toNonUnitalSubring

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

Instances For

`NonUnitalSubalgebra`s inherit structure from their `Submodule` coercions. #

source

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

source

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'

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

↑0 = 0

source

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

source

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

source

@[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 : ↥S) :

↑(r • x) = r • ↑x

source

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

source

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

source

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

source

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 ⋯

Instances For

source

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

Instances For

source

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₂

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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)

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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 φ

source

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

source

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)

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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)

source

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)

source

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}

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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.

source

@[deprecated NonUnitalAlgebra.adjoin_induction (since := "2024-10-10")]

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

Alias of NonUnitalAlgebra.adjoin_induction.

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.

source

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

source

@[deprecated NonUnitalAlgebra.adjoin_induction (since := "2024-10-11")]

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

p a

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

source

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)

source

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

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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 := ⊥ }

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

@[deprecated NonUnitalAlgebra.range_eq_top (since := "2024-11-11")]

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

Alias of NonUnitalAlgebra.range_eq_top.

source

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

source

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

Subsingleton (NonUnitalSubalgebra R A)

source

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

Instances For

source

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

source

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

source

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

source

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

source

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₁

source

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

source

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)

source

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

Instances For

source

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)

source

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

source

@[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, ⋯⟩

source

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

source

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

source

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

source

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)

source

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 : ι) → ↥(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.

Instances For

source

@[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 : ι) → ↥(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

source

@[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 : ι) → ↥(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

source

@[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 : ι) → ↥(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

source

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 : ι) → ↥(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⟩

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

(center R A).toNonUnitalSubring = NonUnitalSubring.center A

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

@[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 = NonUnitalCommSemiring.mk ⋯

Instances For

source

@[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 = NonUnitalCommRing.mk ⋯

Instances For

source

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

Instances For

source

@[simp]

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

x ∈ nonUnitalSubalgebraOfNonUnitalSubsemiring S ↔ x ∈ S

source

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

Instances For

source

@[simp]

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

x ∈ nonUnitalSubalgebraOfNonUnitalSubring S ↔ x ∈ S

Documentation

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Non-unital Subalgebras over Commutative Semirings #

TODO #

`NonUnitalSubalgebra`s inherit structure from their `Submodule` coercions. #

Non-unital Subalgebras over Commutative Semirings #

TODO #

NonUnitalSubalgebras inherit structure from their Submodule coercions. #

`NonUnitalSubalgebra`s inherit structure from their `Submodule` coercions. #