Unitization of a non-unital algebra #
Given a non-unital R
-algebra A
(given via the type classes
[non_unital_ring A] [module R A] [smul_comm_class R A A] [is_scalar_tower R A A]
) we construct
the minimal unital R
-algebra containing A
as an ideal. This object algebra.unitization R A
is
a type synonym for R × A
on which we place a different multiplicative structure, namely,
(r₁, a₁) * (r₂, a₂) = (r₁ * r₂, r₁ • a₂ + r₂ • a₁ + a₁ * a₂)
where the multiplicative identity
is (1, 0)
.
Note, when A
is a unital R
-algebra, then unitization R A
constructs a new multiplicative
identity different from the old one, and so in general unitization R A
and A
will not be
isomorphic even in the unital case. This approach actually has nice functorial properties.
There is a natural coercion from A
to unitization R A
given by λ a, (0, a)
, the image
of which is a proper ideal (TODO), and when R
is a field this ideal is maximal. Moreover,
this ideal is always an essential ideal (it has nontrivial intersection with every other nontrivial
ideal).
Every non-unital algebra homomorphism from A
into a unital R
-algebra B
has a unique
extension to a (unital) algebra homomorphism from unitization R A
to B
.
Main definitions #
unitization R A
: the unitization of a non-unitalR
-algebraA
.unitization.algebra
: the unitization ofA
as a (unital)R
-algebra.unitization.coe_non_unital_alg_hom
: coercion as a non-unital algebra homomorphism.non_unital_alg_hom.to_alg_hom φ
: the extension of a non-unital algebra homomorphismφ : A → B
into a unitalR
-algebraB
to an algebra homomorphismunitization R A →ₐ[R] B
.
Main results #
non_unital_alg_hom.to_alg_hom_unique
: the extension is unique
TODO #
- prove the unitization operation is a functor between the appropriate categories
- prove the image of the coercion is an essential ideal, maximal if scalars are a field.
The minimal unitization of a non-unital R
-algebra A
. This is just a type synonym for
R × A
.
Equations
- unitization R A = (R × A)
Instances for unitization
- unitization.has_coe_t
- unitization.inhabited
- unitization.has_zero
- unitization.has_add
- unitization.has_neg
- unitization.add_semigroup
- unitization.add_zero_class
- unitization.add_monoid
- unitization.add_group
- unitization.add_comm_semigroup
- unitization.add_comm_monoid
- unitization.add_comm_group
- unitization.has_smul
- unitization.is_scalar_tower
- unitization.smul_comm_class
- unitization.is_central_scalar
- unitization.mul_action
- unitization.distrib_mul_action
- unitization.module
- unitization.has_one
- unitization.has_mul
- unitization.mul_one_class
- unitization.non_assoc_semiring
- unitization.monoid
- unitization.comm_monoid
- unitization.semiring
- unitization.comm_semiring
- unitization.has_star
- unitization.star_add_monoid
- unitization.star_module
- unitization.star_ring
- unitization.algebra
The canonical inclusion R → unitization R A
.
Equations
- unitization.inl r = (r, 0)
The canonical inclusion A → unitization R A
.
Equations
- unitization.has_coe_t = {coe := λ (a : A), (0, a)}
The canonical projection unitization R A → R
.
The canonical projection unitization R A → A
.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
To show a property hold on all unitization R A
it suffices to show it holds
on terms of the form inl r + a
.
This can be used as induction x using unitization.ind
.
This cannot be marked @[ext]
as it ends up being used instead of linear_map.prod_ext
when
working with R × A
.
The canonical R
-linear inclusion A → unitization R A
.
Equations
- unitization.coe_hom R A = {to_fun := coe coe_to_lift, map_add' := _, map_smul' := _}
The canonical R
-linear projection unitization R A → A
.
Equations
- unitization.snd_hom R A = {to_fun := unitization.snd A, map_add' := _, map_smul' := _}
Multiplicative structure #
Equations
- unitization.has_one = {one := (1, 0)}
Equations
- unitization.mul_one_class = {one := 1, mul := has_mul.mul unitization.has_mul, one_mul := _, mul_one := _}
Equations
- unitization.non_assoc_semiring = {add := add_comm_monoid.add unitization.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero unitization.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul unitization.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_one_class.mul unitization.mul_one_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one unitization.mul_one_class, one_mul := _, mul_one := _, nat_cast := add_comm_monoid_with_one.nat_cast._default mul_one_class.one add_comm_monoid.add unitization.non_assoc_semiring._proof_13 add_comm_monoid.zero unitization.non_assoc_semiring._proof_14 unitization.non_assoc_semiring._proof_15 add_comm_monoid.nsmul unitization.non_assoc_semiring._proof_16 unitization.non_assoc_semiring._proof_17, nat_cast_zero := _, nat_cast_succ := _}
Equations
- unitization.monoid = {mul := mul_one_class.mul unitization.mul_one_class, mul_assoc := _, one := mul_one_class.one unitization.mul_one_class, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (unitization R A)), npow_zero' := _, npow_succ' := _}
Equations
- unitization.comm_monoid = {mul := monoid.mul unitization.monoid, mul_assoc := _, one := monoid.one unitization.monoid, one_mul := _, mul_one := _, npow := monoid.npow unitization.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
Equations
- unitization.semiring = {add := non_assoc_semiring.add unitization.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero unitization.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul unitization.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul unitization.monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid.one unitization.monoid, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast unitization.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := monoid.npow unitization.monoid, npow_zero' := _, npow_succ' := _}
Equations
- unitization.comm_semiring = {add := non_assoc_semiring.add unitization.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero unitization.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul unitization.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_monoid.mul unitization.comm_monoid, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_monoid.one unitization.comm_monoid, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast unitization.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_monoid.npow unitization.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}
The canonical inclusion of rings R →+* unitization R A
.
Equations
- unitization.inl_ring_hom R A = {to_fun := unitization.inl (mul_zero_class.to_has_zero A), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Star structure #
Equations
- unitization.has_star = {star := λ (ra : unitization R A), (has_star.star ra.fst, has_star.star ra.snd)}
Equations
Equations
Algebra structure #
Equations
- unitization.algebra S R A = {to_has_smul := unitization.has_smul mul_action.to_has_smul, to_ring_hom := {to_fun := ((unitization.inl_ring_hom R A).comp (algebra_map S R)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
The canonical R
-algebra projection unitization R A → R
.
Equations
- unitization.fst_hom R A = {to_fun := unitization.fst A, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
The coercion from a non-unital R
-algebra A
to its unitization unitization R A
realized as a non-unital algebra homomorphism.
Equations
- unitization.coe_non_unital_alg_hom R A = {to_fun := coe coe_to_lift, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _}
Non-unital algebra homomorphisms from A
into a unital R
-algebra C
lift uniquely to
unitization R A →ₐ[R] C
. This is the universal property of the unitization.
Equations
- unitization.lift = {to_fun := λ (φ : A →ₙₐ[R] C), {to_fun := λ (x : unitization R A), ⇑(algebra_map R C) x.fst + ⇑φ x.snd, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv_fun := λ (φ : unitization R A →ₐ[R] C), φ.to_non_unital_alg_hom.comp (unitization.coe_non_unital_alg_hom R A), left_inv := _, right_inv := _}