Subalgebras over Commutative Semiring #
In this file we define Subalgebra
s and the usual operations on them (map
, comap
).
More lemmas about adjoin
can be found in RingTheory.Adjoin
.
A subalgebra is a sub(semi)ring that includes the range of algebraMap
.
The image of
algebraMap
is contained in the underlying set of the subalgebra
Instances For
Equations
- Subalgebra.instSetLike = { coe := fun (s : Subalgebra R A) => s.carrier, coe_injective' := ⋯ }
Copy of a subalgebra with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
Instances For
Turn a Subalgebra
into a NonUnitalSubalgebra
by forgetting that it contains 1
.
Equations
- S.toNonUnitalSubalgebra = { carrier := S.carrier, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯ }
Instances For
The projection from a subalgebra of A
to an additive submonoid of A
.
Equations
Instances For
A subalgebra over a ring is also a Subring
.
Equations
- S.toSubring = { toSubsemiring := S.toSubsemiring, neg_mem' := ⋯ }
Instances For
Equations
- S.instInhabitedSubtypeMem = { default := 0 }
Subalgebra
s inherit structure from their Subsemiring
/ Semiring
coercions.
Equations
- S.toSemiring = S.toSemiring
Equations
Equations
The forgetful map from Subalgebra
to Submodule
as an OrderEmbedding
Equations
- Subalgebra.toSubmodule = { toFun := fun (S : Subalgebra R A) => { carrier := ↑S, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Subalgebra
s inherit structure from their Submodule
coercions.
Equations
Equations
Equations
- S.algebra' = Algebra.mk ((algebraMap R' A).codRestrict S ⋯) ⋯ ⋯
Embedding of a subalgebra into the algebra.
Equations
- S.val = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
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
Instances For
Transport a subalgebra via an algebra homomorphism.
Equations
- Subalgebra.map f S = { toSubsemiring := Subsemiring.map (↑f) S.toSubsemiring, algebraMap_mem' := ⋯ }
Instances For
Preimage of a subalgebra under an algebra homomorphism.
Equations
- Subalgebra.comap f S = { toSubsemiring := Subsemiring.comap (↑f) S.toSubsemiring, algebraMap_mem' := ⋯ }
Instances For
Equations
- SubalgebraClass.toAlgebra s = Algebra.mk { toFun := fun (r : R) => ⟨(algebraMap R A) r, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯
Embedding of a subalgebra into the algebra, as an algebra homomorphism.
Equations
- SubalgebraClass.val s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
A submodule containing 1
and closed under multiplication is a subalgebra.
Equations
- p.toSubalgebra h_one h_mul = { carrier := p.carrier, mul_mem' := ⋯, one_mem' := h_one, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }
Instances For
Restrict the codomain of an algebra homomorphism.
Equations
- f.codRestrict S hf = { toRingHom := (↑f).codRestrict S hf, commutes' := ⋯ }
Instances For
Restrict the codomain of an AlgHom
f
to f.range
.
This is the bundled version of Set.rangeFactorization
.
Equations
- f.rangeRestrict = f.codRestrict f.range ⋯
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
Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.
This is a computable alternative to AlgEquiv.ofInjective
.
Equations
- AlgEquiv.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := g ∘ ⇑f.range.val, left_inv := h, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Restrict an injective algebra homomorphism to an algebra isomorphism
Equations
Instances For
Restrict an algebra homomorphism between fields to an algebra isomorphism
Equations
Instances For
Given an equivalence e : A ≃ₐ[R] B
of R
-algebras and a subalgebra S
of A
,
subalgebraMap
is the induced equivalence between S
and S.map e
Equations
- e.subalgebraMap S = { toEquiv := (e.toRingEquiv.subsemiringMap S.toSubsemiring).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
The minimal subalgebra that includes s
.
Equations
- Algebra.adjoin R s = { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s), algebraMap_mem' := ⋯ }
Instances For
Galois insertion between adjoin
and coe
.
Equations
- Algebra.gi = { choice := fun (s : Set A) (hs : ↑(Algebra.adjoin R s) ≤ s) => (Algebra.adjoin R s).copy s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Equations
- Algebra.instCompleteLatticeSubalgebra = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A dependent version of Subalgebra.iSup_induction
.
Equations
- Algebra.instInhabitedSubalgebra = { default := ⊥ }
TODO: change proof to rfl
when fixing https://github.com/leanprover-community/mathlib4/issues/18110.
Alias of AlgHom.range_eq_top
.
The bottom subalgebra is isomorphic to the base ring.
Equations
Instances For
The bottom subalgebra is isomorphic to the field.
Equations
Instances For
The top subalgebra is isomorphic to the algebra.
This is the algebra version of Submodule.topEquiv
.
Equations
Instances For
Equations
- Subalgebra.instUnique = { toInhabited := inferInstanceAs (Inhabited (Subalgebra R R)), uniq := ⋯ }
The map S → T
when S
is a subalgebra contained in the subalgebra T
.
This is the subalgebra version of Submodule.inclusion
, or Subring.inclusion
Equations
- Subalgebra.inclusion h = { toFun := Set.inclusion h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Two subalgebras that are equal are also equivalent as algebras.
This is the Subalgebra
version of LinearEquiv.ofEq
and Equiv.Set.ofEq
.
Equations
Instances For
An AlgHom
between two rings restricts to an AlgHom
from any subalgebra of the
domain onto the image of that subalgebra.
Equations
- AlgHom.subalgebraMap S f = (f.comp S.val).codRestrict (Subalgebra.map f S) ⋯
Instances For
A subalgebra is isomorphic to its image under an injective AlgHom
Equations
- S.equivMapOfInjective f hf = (AlgEquiv.ofInjective (f.comp S.val) ⋯).trans ((f.comp S.val).range.equivOfEq (Subalgebra.map f S) ⋯)
Instances For
Actions by Subalgebra
s #
These are just copies of the definitions about Subsemiring
starting from
Subring.mulAction
.
The action by a subalgebra is the action by the underlying algebra.
Equations
- S.instSMulSubtypeMem = inferInstanceAs (SMul (↥S.toSubsemiring) α)
Note that this provides IsScalarTower S R R
which is needed by smul_mul_assoc
.
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
The action by a subalgebra is the action by the underlying algebra.
Equations
- S.moduleLeft = inferInstanceAs (Module (↥S.toSubsemiring) α)
The action by a subalgebra is the action by the underlying algebra.
Equations
The center of an algebra is the set of elements which commute with every element. They form a subalgebra.
Equations
- Subalgebra.center R A = { toSubsemiring := Subsemiring.center A, algebraMap_mem' := ⋯ }
Instances For
Equations
The centralizer of a set as a subalgebra.
Equations
- Subalgebra.centralizer R s = { toSubsemiring := Subsemiring.centralizer s, algebraMap_mem' := ⋯ }
Instances For
A subsemiring is an ℕ
-subalgebra.
Equations
- subalgebraOfSubsemiring S = { toSubsemiring := S, algebraMap_mem' := ⋯ }
Instances For
A subring is a ℤ
-subalgebra.
Equations
- subalgebraOfSubring S = { toSubsemiring := S.toSubsemiring, algebraMap_mem' := ⋯ }
Instances For
The equalizer of two R-algebra homomorphisms
Equations
Instances For
Turn a non-unital subalgebra containing 1
into a subalgebra.
Equations
- S.toSubalgebra h1 = { carrier := S.carrier, mul_mem' := ⋯, one_mem' := h1, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }