The bialgebra structure on monoid algebras #
Given a monoid M, a commutative semiring R and an R-bialgebra A, this file collects results
about the R-bialgebra instance on A[M] inherited from the corresponding structure on its
coefficients, building upon results in Mathlib/RingTheory/Coalgebra/MonoidAlgebra.lean about the
coalgebra structure.
Main definitions #
(Add)MonoidAlgebra.instBialgebra: theR-bialgebra structure onA[M]whenMis an (add) monoid andAis anR-bialgebra.LaurentPolynomial.instBialgebra: theR-bialgebra structure on the Laurent polynomialsA[T;T⁻¹]whenAis anR-bialgebra.(Add)MonoidAlgebra.mapDomainBialgHomEquiv: isomorphism betweenR-bialgebra homsA[G] → A[H]and groups homsG → HwhenGandHare an (add) group andAis anR-bialgebra.
@[simp]
theorem
MonoidAlgebra.isGroupLikeElem_single_one
{R : Type u_1}
{A : Type u_3}
{G : Type u_5}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
(g : G)
:
IsGroupLikeElem R (single g 1)
@[simp]
theorem
AddMonoidAlgebra.isGroupLikeElem_single_one
{R : Type u_1}
{A : Type u_3}
{G : Type u_5}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
(g : G)
:
IsGroupLikeElem R (single g 1)
@[simp]
theorem
MonoidAlgebra.span_isGroupLikeElem
{R : Type u_1}
{A : Type u_3}
{G : Type u_5}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
:
A group algebra is spanned by its group-like elements.
@[simp]
theorem
AddMonoidAlgebra.span_isGroupLikeElem
{R : Type u_1}
{A : Type u_3}
{G : Type u_5}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
:
@[instance_reducible]
noncomputable instance
MonoidAlgebra.instBialgebra
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
:
Bialgebra R (MonoidAlgebra A M)
Equations
- One or more equations did not get rendered due to their size.
@[instance_reducible]
noncomputable instance
AddMonoidAlgebra.instBialgebra
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
:
Bialgebra R (AddMonoidAlgebra A M)
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
MonoidAlgebra.mapDomainBialgHom
(R : Type u_1)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Monoid M]
[Monoid N]
(f : M →* N)
:
If f : M → N is a monoid hom, then MonoidAlgebra.mapDomain f is a bialgebra hom between
their monoid algebras.
Equations
Instances For
noncomputable def
AddMonoidAlgebra.mapDomainBialgHom
(R : Type u_1)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[AddMonoid M]
[AddMonoid N]
(f : M →+ N)
:
If f : M → N is an additive monoid hom, then MonoidAlgebra.mapDomain f is a bialgebra hom
between their additive monoid algebras.
Equations
Instances For
@[simp]
theorem
AddMonoidAlgebra.coeff_mapDomainBialgHom_apply
(R : Type u_1)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[AddMonoid M]
[AddMonoid N]
(f : M →+ N)
(a✝ : AddMonoidAlgebra R M)
:
@[simp]
theorem
MonoidAlgebra.coeff_mapDomainBialgHom_apply
(R : Type u_1)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Monoid M]
[Monoid N]
(f : M →* N)
(a✝ : MonoidAlgebra R M)
:
@[simp]
theorem
MonoidAlgebra.mapDomainBialgHom_id
{R : Type u_1}
{M : Type u_8}
[CommSemiring R]
[Monoid M]
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainBialgHom_id
{R : Type u_1}
{M : Type u_8}
[CommSemiring R]
[AddMonoid M]
:
theorem
MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom
{R : Type u_1}
{M : Type u_8}
{N : Type u_9}
{O : Type u_10}
[CommSemiring R]
[Monoid M]
[Monoid N]
[Monoid O]
(f : N →* O)
(g : M →* N)
(x : MonoidAlgebra R M)
:
theorem
AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom
{R : Type u_1}
{M : Type u_8}
{N : Type u_9}
{O : Type u_10}
[CommSemiring R]
[AddMonoid M]
[AddMonoid N]
[AddMonoid O]
(f : N →+ O)
(g : M →+ N)
(x : AddMonoidAlgebra R M)
:
@[simp]
theorem
MonoidAlgebra.mapDomainBialgHom_single
{R : Type u_1}
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Monoid M]
[Monoid N]
(f : M →* N)
(m : M)
(r : R)
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainBialgHom_single
{R : Type u_1}
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[AddMonoid M]
[AddMonoid N]
(f : M →+ N)
(m : M)
(r : R)
:
theorem
MonoidAlgebra.bialgHom_ext
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Bialgebra R A]
[Bialgebra R B]
[Monoid M]
⦃φ₁ φ₂ : MonoidAlgebra A M →ₐc[R] B⦄
(single_one_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1))
(single_one_left : (↑φ₁).comp singleOneAlgHom = (↑φ₂).comp singleOneAlgHom)
:
A R-bialgebra homomorphism from A[M] is uniquely defined by its
values on the functions single m 1 and single 1 a.
See note [partially-applied ext lemmas]. Note that the first assumption isn't written as an
equality of MonoidHoms because of doesn't additivise.
theorem
AddMonoidAlgebra.bialgHom_ext
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Bialgebra R A]
[Bialgebra R B]
[AddMonoid M]
⦃φ₁ φ₂ : AddMonoidAlgebra A M →ₐc[R] B⦄
(single_zero_right : ∀ (m : M), φ₁ (single m 1) = φ₂ (single m 1))
(single_zero_left : (↑φ₁).comp singleZeroAlgHom = (↑φ₂).comp singleZeroAlgHom)
:
A R-bialgebra homomorphism from A[M] is uniquely defined by its
values on the functions single m 1 and single 1 a.
See note [partially-applied ext lemmas]. Note that the first assumption isn't written as an
equality of AddMonoidHoms because of doesn't multiplicativise.
theorem
MonoidAlgebra.bialgHom_ext_iff
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Bialgebra R A]
[Bialgebra R B]
[Monoid M]
{φ₁ φ₂ : MonoidAlgebra A M →ₐc[R] B}
:
theorem
AddMonoidAlgebra.bialgHom_ext_iff
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Bialgebra R A]
[Bialgebra R B]
[AddMonoid M]
{φ₁ φ₂ : AddMonoidAlgebra A M →ₐc[R] B}
:
theorem
MonoidAlgebra.bialgHom_ext'
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Bialgebra R A]
[Bialgebra R B]
[Monoid M]
⦃φ₁ φ₂ : MonoidAlgebra A M →ₐc[R] B⦄
(single_one_right : (↑φ₁).comp (of A M) = (↑φ₂).comp (of A M))
(single_one_left : (↑φ₁).comp singleOneAlgHom = (↑φ₂).comp singleOneAlgHom)
:
Version of bialgHom_ext where both assumptions are written as equalities of bundled homs.
@[simp]
theorem
MonoidAlgebra.counit_domCongr
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
[Monoid N]
(e : M ≃* N)
(x : MonoidAlgebra A M)
:
@[simp]
theorem
AddMonoidAlgebra.counit_domCongr
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
[AddMonoid N]
(e : M ≃+ N)
(x : AddMonoidAlgebra A M)
:
noncomputable def
MonoidAlgebra.domCongrBialgEquiv
(R : Type u_1)
(A : Type u_3)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
[Monoid N]
(e : M ≃* N)
:
Isomorphic monoids have isomorphic monoid algebras.
Equations
- MonoidAlgebra.domCongrBialgEquiv R A e = BialgEquiv.ofAlgEquiv (MonoidAlgebra.domCongr R A e) ⋯ ⋯
Instances For
noncomputable def
AddMonoidAlgebra.domCongrBialgEquiv
(R : Type u_1)
(A : Type u_3)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
[AddMonoid N]
(e : M ≃+ N)
:
Isomorphic monoids have isomorphic monoid algebras.
Equations
- AddMonoidAlgebra.domCongrBialgEquiv R A e = BialgEquiv.ofAlgEquiv (AddMonoidAlgebra.domCongr R A e) ⋯ ⋯
Instances For
theorem
MonoidAlgebra.coeff_domCongrBialgEquiv_symm_apply
(R : Type u_1)
(A : Type u_3)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
[Monoid N]
(e : M ≃* N)
(a✝ : MonoidAlgebra A N)
:
theorem
AddMonoidAlgebra.coeff_domCongrBialgEquiv_apply
(R : Type u_1)
(A : Type u_3)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
[AddMonoid N]
(e : M ≃+ N)
(a✝ : AddMonoidAlgebra A M)
:
theorem
AddMonoidAlgebra.coeff_domCongrBialgEquiv_symm_apply
(R : Type u_1)
(A : Type u_3)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
[AddMonoid N]
(e : M ≃+ N)
(a✝ : AddMonoidAlgebra A N)
:
theorem
MonoidAlgebra.coeff_domCongrBialgEquiv_apply
(R : Type u_1)
(A : Type u_3)
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
[Monoid N]
(e : M ≃* N)
(a✝ : MonoidAlgebra A M)
:
noncomputable def
MonoidAlgebra.bialgEquivOfSubsingleton
{R : Type u_1}
(M : Type u_8)
[CommSemiring R]
[Monoid M]
[Subsingleton M]
:
The trivial monoid algebra is isomorphic to the base ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AddMonoidAlgebra.bialgEquivOfSubsingleton
{R : Type u_1}
(M : Type u_8)
[CommSemiring R]
[AddMonoid M]
[Subsingleton M]
:
The trivial monoid algebra is isomorphic to the base ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MonoidAlgebra.isGroupLikeElem_of
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
(m : M)
:
IsGroupLikeElem R ((of A M) m)
noncomputable def
MonoidAlgebra.liftGroupLikeBialgHom
{R : Type u_1}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
:
The R-bialgebra map from the group algebra on the group-like elements of A to A.
Equations
- MonoidAlgebra.liftGroupLikeBialgHom = BialgHom.ofAlgHom ((MonoidAlgebra.lift R A (GroupLike R A)) { toFun := fun (g : GroupLike R A) => ↑g, map_one' := ⋯, map_mul' := ⋯ }) ⋯ ⋯
Instances For
@[simp]
theorem
MonoidAlgebra.liftGroupLikeBialgHom_apply
{R : Type u_1}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
(a✝ : MonoidAlgebra R (GroupLike R A))
:
noncomputable def
MonoidAlgebra.toAdditiveBialgEquiv
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
:
The bialgebra equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of
Additive.
Equations
Instances For
theorem
MonoidAlgebra.coeff_toAdditiveBialgEquiv_symm_apply
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
(a✝ : AddMonoidAlgebra A (Additive M))
:
theorem
MonoidAlgebra.coeff_toAdditiveBialgEquiv_apply
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
(a✝ : MonoidAlgebra A M)
:
@[simp]
theorem
MonoidAlgebra.toAdditiveBialgEquiv_single
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[Monoid M]
(m : M)
(a : A)
:
noncomputable def
MonoidAlgebra.liftMulEquiv
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
[Monoid M]
:
MonoidAlgebra.lift as a MulEquiv.
Equations
- MonoidAlgebra.liftMulEquiv R A M = { toEquiv := (MonoidAlgebra.lift R A M).trans (WithConv.equiv (MonoidAlgebra R M →ₐ[R] A)).symm, map_mul' := ⋯ }
Instances For
@[simp]
@[simp]
theorem
MonoidAlgebra.convMul_bialgHom_single_one
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
[CommSemiring R]
[CommSemiring A]
[Bialgebra R A]
[CommMonoid M]
(f g : WithConv (MonoidAlgebra R M →ₐc[R] A))
(x : M)
:
@[simp]
theorem
AddMonoidAlgebra.convMul_bialgHom_single_one
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
[CommSemiring R]
[CommSemiring A]
[Bialgebra R A]
[AddCommMonoid M]
(f g : WithConv (AddMonoidAlgebra R M →ₐc[R] A))
(x : M)
:
@[simp]
theorem
MonoidAlgebra.mapDomainBialgHom_mul
{R : Type u_1}
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[CommMonoid M]
[CommMonoid N]
(f g : M →* N)
:
mapDomainBialgHom R (f * g) = (WithConv.toConv (mapDomainBialgHom R f) * WithConv.toConv (mapDomainBialgHom R g)).ofConv
@[simp]
theorem
AddMonoidAlgebra.mapDomainBialgHom_add
{R : Type u_1}
{M : Type u_8}
{N : Type u_9}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
(f g : M →+ N)
:
mapDomainBialgHom R (f + g) = (WithConv.toConv (mapDomainBialgHom R f) * WithConv.toConv (mapDomainBialgHom R g)).ofConv
theorem
MonoidAlgebra.comulAlgHom_comp_mapRingHom
{R : Type u_1}
{S : Type u_2}
{M : Type u_8}
[CommSemiring R]
[CommSemiring S]
[CommMonoid M]
(f : R →+* S)
:
(Bialgebra.comulAlgHom S (MonoidAlgebra S M)).comp (mapRingHom M f) = (Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp
(Bialgebra.comulAlgHom R (MonoidAlgebra R M)).toRingHom
theorem
MonoidAlgebra.counitAlgHom_comp_mapRingHom
{R : Type u_1}
{S : Type u_2}
{M : Type u_8}
[CommSemiring R]
[CommSemiring S]
[CommMonoid M]
(f : R →+* S)
:
(Bialgebra.counitAlgHom S (MonoidAlgebra S M)).comp (mapRingHom M f) = f.comp (Bialgebra.counitAlgHom R (MonoidAlgebra R M)).toRingHom
theorem
MonoidAlgebra.isGroupLikeElem_iff_mem_range_single_one
{R : Type u_1}
{M : Type u_8}
[CommRing R]
[IsDomain R]
{x : MonoidAlgebra R M}
:
theorem
AddMonoidAlgebra.isGroupLikeElem_iff_mem_range_single_one
{R : Type u_1}
{M : Type u_8}
[CommRing R]
[IsDomain R]
{x : AddMonoidAlgebra R M}
:
theorem
MonoidAlgebra.isGroupLikeElem_iff_mem_range_of
{R : Type u_1}
{M : Type u_8}
[CommRing R]
[IsDomain R]
[MulOneClass M]
{x : MonoidAlgebra R M}
:
noncomputable def
MonoidAlgebra.mapDomainOfBialgHom
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[Group G]
[Group H]
(f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
:
A bialgebra homomorphism R[G] → R[H] between group algebras over a domain R comes from a
group hom G → H.
See MonoidAlgebra.mapDomainBialgHom for the forward map.
Equations
- MonoidAlgebra.mapDomainOfBialgHom f = { toFun := MonoidAlgebra.mapDomainOfBialgHomFun✝ f, map_one' := ⋯, map_mul' := ⋯ }
Instances For
noncomputable def
AddMonoidAlgebra.mapDomainOfBialgHom
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[AddGroup G]
[AddGroup H]
(f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)
:
A bialgebra homomorphism R[G] → R[H] between group algebras over a domain R comes from a
group hom G → H.
See MonoidAlgebra.mapDomainBialgHom for the forward map.
Equations
- AddMonoidAlgebra.mapDomainOfBialgHom f = { toFun := AddMonoidAlgebra.mapDomainOfBialgHomFun✝ f, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.single_mapDomainOfBialgHom
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[Group G]
[Group H]
(f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
(g : G)
(r : R)
:
@[simp]
theorem
AddMonoidAlgebra.single_mapDomainOfBialgHom
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[AddGroup G]
[AddGroup H]
(f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)
(g : G)
(r : R)
:
@[simp]
theorem
MonoidAlgebra.mapDomainBialgHom_mapDomainOfBialgHom
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[Group G]
[Group H]
(f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainBialgHom_mapDomainOfBialgHom
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[AddGroup G]
[AddGroup H]
(f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)
:
@[simp]
theorem
MonoidAlgebra.mapDomainOfBialgHom_comp
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
{I : Type u_7}
[CommRing R]
[IsDomain R]
[Group G]
[Group H]
[Group I]
(f : MonoidAlgebra R H →ₐc[R] MonoidAlgebra R I)
(g : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
:
@[simp]
theorem
AddMonoidAlgebra.mapDomainOfBialgHom_comp
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
{I : Type u_7}
[CommRing R]
[IsDomain R]
[AddGroup G]
[AddGroup H]
[AddGroup I]
(f : AddMonoidAlgebra R H →ₐc[R] AddMonoidAlgebra R I)
(g : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)
:
noncomputable def
MonoidAlgebra.mapDomainBialgHomEquiv
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[Group G]
[Group H]
:
The equivalence between group homs G → H and bialgebra homs R[G] → R[H] of group algebras
over a domain.
Equations
- MonoidAlgebra.mapDomainBialgHomEquiv = { toFun := MonoidAlgebra.mapDomainBialgHom R, invFun := MonoidAlgebra.mapDomainOfBialgHom, left_inv := ⋯, right_inv := ⋯ }
Instances For
noncomputable def
AddMonoidAlgebra.mapDomainBialgHomEquiv
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[AddGroup G]
[AddGroup H]
:
The equivalence between group homs G → H and bialgebra homs R[G] → R[H] of group algebras
over a domain.
Equations
- AddMonoidAlgebra.mapDomainBialgHomEquiv = { toFun := AddMonoidAlgebra.mapDomainBialgHom R, invFun := AddMonoidAlgebra.mapDomainOfBialgHom, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[simp]
theorem
AddMonoidAlgebra.mapDomainBialgHomEquiv_symm_apply
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[AddGroup G]
[AddGroup H]
(f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)
:
@[simp]
theorem
MonoidAlgebra.mapDomainBialgHomEquiv_symm_apply
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[Group G]
[Group H]
(f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)
:
noncomputable def
MonoidAlgebra.mapDomainBialgHomMulEquiv
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[CommGroup G]
[CommGroup H]
:
The group isomorphism between group homs G → H and bialgebra homs R[G] → R[H] of group
algebras over a domain.
Equations
- MonoidAlgebra.mapDomainBialgHomMulEquiv = { toEquiv := MonoidAlgebra.mapDomainBialgHomEquiv.trans (WithConv.equiv (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)).symm, map_mul' := ⋯ }
Instances For
@[simp]
theorem
MonoidAlgebra.mapDomainBialgHomMulEquiv_symm_apply
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[CommGroup G]
[CommGroup H]
(a✝ : WithConv (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H))
:
@[simp]
theorem
MonoidAlgebra.coeff_mapDomainBialgHomMulEquiv_apply_ofConv_apply
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[CommGroup G]
[CommGroup H]
(a✝ : G →* H)
(a✝¹ : MonoidAlgebra R G)
:
theorem
AddMonoidAlgebra.bialgHom_ext'
{R : Type u_1}
{A : Type u_3}
{B : Type u_4}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Semiring B]
[Bialgebra R A]
[Bialgebra R B]
[AddMonoid M]
⦃φ₁ φ₂ : AddMonoidAlgebra A M →ₐc[R] B⦄
(single_one_right : (↑φ₁).comp (of A M) = (↑φ₂).comp (of A M))
(single_one_left : (↑φ₁).comp singleZeroAlgHom = (↑φ₂).comp singleZeroAlgHom)
:
See note [partially-applied ext lemmas].
theorem
AddMonoidAlgebra.isGroupLikeElem_of
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
(m : M)
:
IsGroupLikeElem R ((of A M) m)
noncomputable def
AddMonoidAlgebra.toMultiplicativeBialgEquiv
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
:
The bialgebra equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of
Multiplicative.
Equations
Instances For
theorem
AddMonoidAlgebra.coeff_toMultiplicativeBialgEquiv_symm_apply
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
(a✝ : MonoidAlgebra A (Multiplicative M))
:
((toMultiplicativeBialgEquiv R A M).symm a✝).coeff = Finsupp.mapDomain (⇑Multiplicative.toAdd) a✝.coeff
theorem
AddMonoidAlgebra.coeff_toMultiplicativeBialgEquiv_apply
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
(a✝ : AddMonoidAlgebra A M)
:
@[simp]
theorem
AddMonoidAlgebra.toMultiplicativeBialgEquiv_single
{R : Type u_1}
{A : Type u_3}
{M : Type u_8}
[CommSemiring R]
[Semiring A]
[Bialgebra R A]
[AddMonoid M]
(m : M)
(a : A)
:
noncomputable def
AddMonoidAlgebra.liftMulEquiv
(R : Type u_1)
(A : Type u_3)
(M : Type u_8)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
[AddMonoid M]
:
AddMonoidAlgebra.lift as a MulEquiv.
Equations
- AddMonoidAlgebra.liftMulEquiv R A M = { toEquiv := (AddMonoidAlgebra.lift R A M).trans (WithConv.equiv (AddMonoidAlgebra R M →ₐ[R] A)).symm, map_mul' := ⋯ }
Instances For
theorem
AddMonoidAlgebra.comulAlgHom_comp_mapRingHom
{R : Type u_1}
{S : Type u_2}
{M : Type u_8}
[CommSemiring R]
[CommSemiring S]
[AddCommMonoid M]
(f : R →+* S)
:
(Bialgebra.comulAlgHom S (AddMonoidAlgebra S M)).comp (mapRingHom M f) = (Algebra.TensorProduct.mapRingHom f (mapRingHom M f) (mapRingHom M f) ⋯ ⋯).comp
(Bialgebra.comulAlgHom R (AddMonoidAlgebra R M)).toRingHom
theorem
AddMonoidAlgebra.counitAlgHom_comp_mapRingHom
{R : Type u_1}
{S : Type u_2}
{M : Type u_8}
[CommSemiring R]
[CommSemiring S]
[AddCommMonoid M]
(f : R →+* S)
:
(Bialgebra.counitAlgHom S (AddMonoidAlgebra S M)).comp (mapRingHom M f) = f.comp (Bialgebra.counitAlgHom R (AddMonoidAlgebra R M)).toRingHom
theorem
AddMonoidAlgebra.isGroupLikeElem_iff_mem_range_of
{R : Type u_1}
{M : Type u_8}
[CommRing R]
[IsDomain R]
[AddZeroClass M]
{x : AddMonoidAlgebra R M}
:
noncomputable def
AddMonoidAlgebra.mapDomainBialgHomAddEquiv
{R : Type u_1}
{G : Type u_5}
{H : Type u_6}
[CommRing R]
[IsDomain R]
[AddCommGroup G]
[AddCommGroup H]
:
The group isomorphism between group homs G → H and bialgebra homs R[G] → R[H] of group
algebras over a domain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[instance_reducible]
noncomputable instance
LaurentPolynomial.instBialgebra
{R : Type u_11}
[CommSemiring R]
{A : Type u_12}
[Semiring A]
[Bialgebra R A]
:
Bialgebra R (LaurentPolynomial A)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LaurentPolynomial.comul_T
{R : Type u_11}
[CommSemiring R]
{A : Type u_12}
[Semiring A]
[Bialgebra R A]
(n : ℤ)
:
@[simp]
theorem
LaurentPolynomial.counit_T
{R : Type u_11}
[CommSemiring R]
{A : Type u_12}
[Semiring A]
[Bialgebra R A]
(n : ℤ)
: