Non-unital Subalgebras over Commutative Semirings #
In this file we define NonUnitalSubalgebra
s 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.
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
A non-unital subalgebra is a sub(semi)ring that is also a submodule.
Instances For
Reinterpret a NonUnitalSubalgebra
as a Submodule
.
Equations
- self.toSubmodule = { toAddSubmonoid := self.toAddSubmonoid, smul_mem' := ⋯ }
Instances For
Equations
- NonUnitalSubalgebra.instSetLike = { coe := fun (s : NonUnitalSubalgebra R A) => s.carrier, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
Equations
- S.instInhabitedSubtypeMem = { default := 0 }
Equations
- ⋯ = ⋯
A non-unital subalgebra over a ring is also a Subring
.
Equations
- S.toNonUnitalSubring = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, neg_mem' := ⋯ }
Instances For
NonUnitalSubalgebra
s inherit structure from their NonUnitalSubsemiring
/ Semiring
coercions.
Equations
- S.toNonUnitalNonAssocSemiring = inferInstance
Equations
- S.toNonUnitalSemiring = inferInstance
Equations
- S.toNonUnitalCommSemiring = inferInstance
Equations
- S.toNonUnitalNonAssocRing = inferInstance
Equations
- S.toNonUnitalRing = inferInstance
Equations
- S.toNonUnitalCommRing = inferInstance
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
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
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. #
Equations
- NonUnitalSubalgebra.instModule' = SMulMemClass.toModule' (NonUnitalSubalgebra R A) R' R A S
Equations
- NonUnitalSubalgebra.instModule = NonUnitalSubalgebra.instModule'
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
Transport a non-unital subalgebra via an algebra homomorphism.
Equations
- NonUnitalSubalgebra.map f S = { toNonUnitalSubsemiring := NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring, smul_mem' := ⋯ }
Instances For
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
Equations
- ⋯ = ⋯
A submodule closed under multiplication is a non-unital subalgebra.
Equations
- p.toNonUnitalSubalgebra h_mul = { toAddSubmonoid := p.toAddSubmonoid, mul_mem' := ⋯, smul_mem' := ⋯ }
Instances For
Range of an NonUnitalAlgHom
as a non-unital subalgebra.
Equations
- NonUnitalAlgHom.range φ = { toNonUnitalSubsemiring := NonUnitalRingHom.srange ↑φ, smul_mem' := ⋯ }
Instances For
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
Restrict the codomain of an NonUnitalAlgHom
f
to f.range
.
This is the bundled version of Set.rangeFactorization
.
Equations
Instances For
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
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
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
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
.
The difference with NonUnitalAlgebra.adjoin_induction
is that this acts on the subtype.
A dependent version of NonUnitalAlgebra.adjoin_induction
.
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
Equations
- NonUnitalAlgebra.instCompleteLatticeNonUnitalSubalgebra = NonUnitalAlgebra.gi.liftCompleteLattice
NonUnitalAlgHom
to ⊤ : NonUnitalSubalgebra R A
.
Equations
- NonUnitalAlgebra.toTop = NonUnitalAlgHom.codRestrict (NonUnitalAlgHom.id R A) ⊤ ⋯
Instances For
Equations
- ⋯ = ⋯
The product of two non-unital subalgebras is a non-unital subalgebra.
Equations
Instances For
Equations
- ⋯ = ⋯
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
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
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
The center of a non-unital algebra is commutative and associative
Equations
- NonUnitalSubalgebra.center.instNonUnitalCommSemiring = NonUnitalSubsemiring.center.instNonUnitalCommSemiring A
Equations
- NonUnitalSubalgebra.center.instNonUnitalCommRing = NonUnitalSubring.center.instNonUnitalCommRing A
The centralizer of a set as a non-unital subalgebra.
Equations
- NonUnitalSubalgebra.centralizer R s = { toNonUnitalSubsemiring := NonUnitalSubsemiring.centralizer s, smul_mem' := ⋯ }
Instances For
A non-unital subsemiring is a non-unital ℕ
-subalgebra.
Equations
- nonUnitalSubalgebraOfNonUnitalSubsemiring S = { toNonUnitalSubsemiring := S, smul_mem' := ⋯ }
Instances For
A non-unital subring is a non-unital ℤ
-subalgebra.
Equations
- nonUnitalSubalgebraOfNonUnitalSubring S = { toNonUnitalSubsemiring := S.toNonUnitalSubsemiring, smul_mem' := ⋯ }