Toric.Mathlib.RingTheory.Bialgebra.MonoidAlgebra

source

theorem MonoidAlgebra.bialgHom_ext {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] ⦃φ₁ φ₂ : MonoidAlgebra R M →ₐc[R] A⦄ (h : ∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) :

φ₁ = φ₂

A R-algebra homomorphism from MonoidAlgebra R M is uniquely defined by its values on the functions single a 1.

source

theorem MonoidAlgebra.bialgHom_ext' {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] ⦃φ₁ φ₂ : MonoidAlgebra R M →ₐc[R] A⦄ (h : (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)) :

φ₁ = φ₂

See note [partially-applied ext lemmas].

source

theorem MonoidAlgebra.bialgHom_ext'_iff {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] {φ₁ φ₂ : MonoidAlgebra R M →ₐc[R] A} :

φ₁ = φ₂ ↔ (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)

source

@[simp]

theorem MonoidAlgebra.counit_domCongr {R : Type u_1} {A : Type u_3} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (x : MonoidAlgebra A M) :

CoalgebraStruct.counit ((domCongr R A e) x) = CoalgebraStruct.counit x

source

def MonoidAlgebra.domCongrBialgHom (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] (e : M ≃* N) :

MonoidAlgebra A M ≃ₐc[R] MonoidAlgebra A N

Isomorphic monoids have isomorphic monoid algebras.

Equations

MonoidAlgebra.domCongrBialgHom R A e = BialgEquiv.ofAlgEquiv (MonoidAlgebra.domCongr R A e) ⋯ ⋯

Instances For

source

@[simp]

theorem MonoidAlgebra.domCongrBialgHom_symm_apply_toFun (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (a✝ : MonoidAlgebra A N) (a : M) :

((domCongrBialgHom R A e).symm a✝) a = a✝ (e a)

source

@[simp]

theorem MonoidAlgebra.domCongrBialgHom_apply_toFun (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (a✝ : MonoidAlgebra A M) (a : N) :

((domCongrBialgHom R A e) a✝) a = a✝ (e.symm a)

source

@[simp]

theorem MonoidAlgebra.domCongrBialgHom_symm_apply_support_val (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (a✝ : MonoidAlgebra A N) :

((domCongrBialgHom R A e).symm a✝).support.val = Multiset.map (⇑e.symm) a✝.support.val

source

@[simp]

theorem MonoidAlgebra.domCongrBialgHom_apply_support_val (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (a✝ : MonoidAlgebra A M) :

((domCongrBialgHom R A e) a✝).support.val = Multiset.map (⇑e) a✝.support.val

source

noncomputable def MonoidAlgebra.bialgEquivOfSubsingleton {R : Type u_1} (M : Type u_7) [CommSemiring R] [Monoid M] [Subsingleton M] :

MonoidAlgebra R M ≃ₐc[R] R

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

source

theorem MonoidAlgebra.isGroupLikeElem_of {R : Type u_1} {A : Type u_3} {G : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [Group G] (g : G) :

IsGroupLikeElem R ((of A G) g)

source

@[simp]

theorem MonoidAlgebra.isGroupLikeElem_single_one {R : Type u_1} {A : Type u_3} {G : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [Group G] (g : G) :

IsGroupLikeElem R (single g 1)

source

@[simp]

theorem MonoidAlgebra.span_isGroupLikeElem {R : Type u_1} {A : Type u_3} {G : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [Group G] :

Submodule.span A {a : MonoidAlgebra A G | IsGroupLikeElem R a} = ⊤

A group algebra is spanned by its group-like elements.

source

def MonoidAlgebra.liftMulEquiv (R : Type u_1) (A : Type u_3) (M : Type u_7) [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid M] :

(M →* A) ≃* (MonoidAlgebra R M →ₐ[R] A)

MonoidAlgebra.lift as a MulEquiv.

Equations

MonoidAlgebra.liftMulEquiv R A M = { toEquiv := MonoidAlgebra.lift R M A, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem MonoidAlgebra.convMul_algHom_single {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [CommSemiring A] [Algebra R A] [Monoid M] (f g : MonoidAlgebra R M →ₐ[R] A) (x : M) :

(f * g) (single x 1) = f (single x 1) * g (single x 1)

source

@[simp]

theorem MonoidAlgebra.convMul_bialgHom_single {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [CommMonoid M] (f g : MonoidAlgebra R M →ₐc[R] A) (x : M) :

(f * g) (single x 1) = f (single x 1) * g (single x 1)

source

@[simp]

theorem MonoidAlgebra.mapDomainBialgHom_mul {R : Type u_1} {M : Type u_7} {N : Type u_8} [CommSemiring R] [CommMonoid M] [CommMonoid N] (f g : M →* N) :

mapDomainBialgHom R (f * g) = mapDomainBialgHom R f * mapDomainBialgHom R g

source

theorem MonoidAlgebra.comulAlgHom_comp_mapRangeRingHom {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommSemiring R] [CommSemiring S] [CommMonoid M] (f : R →+* S) :

(Bialgebra.comulAlgHom S (MonoidAlgebra S M)).comp (mapRangeRingHom M f) = (Algebra.TensorProduct.mapRingHom f (mapRangeRingHom M f) (mapRangeRingHom M f) ⋯ ⋯).comp (Bialgebra.comulAlgHom R (MonoidAlgebra R M)).toRingHom

source

theorem MonoidAlgebra.counitAlgHom_comp_mapRangeRingHom {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommSemiring R] [CommSemiring S] [CommMonoid M] (f : R →+* S) :

(Bialgebra.counitAlgHom S (MonoidAlgebra S M)).comp (mapRangeRingHom M f) = f.comp (Bialgebra.counitAlgHom R (MonoidAlgebra R M)).toRingHom

source

@[simp]

theorem MonoidAlgebra.isGroupLikeElem_iff_mem_range_of {R : Type u_1} {G : Type u_4} [CommRing R] [IsDomain R] [Group G] {x : MonoidAlgebra R G} :

IsGroupLikeElem R x ↔ x ∈ Set.range ⇑(of R G)

source

noncomputable def MonoidAlgebra.mapDomainOfBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) :

G →* 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

source

theorem MonoidAlgebra.single_mapDomainOfBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) (g : G) (r : R) :

single ((mapDomainOfBialgHom f) g) r = f (single g r)

source

@[simp]

theorem MonoidAlgebra.mapDomainBialgHom_mapDomainOfBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) :

mapDomainBialgHom R (mapDomainOfBialgHom f) = f

source

@[simp]

theorem MonoidAlgebra.mapDomainOfBialgHom_mapDomainBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] (f : G →* H) :

mapDomainOfBialgHom (mapDomainBialgHom R f) = f

source

noncomputable def MonoidAlgebra.mapDomainBialgHomEquiv {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] :

(G →* H) ≃ (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R 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

source

@[simp]

theorem MonoidAlgebra.mapDomainBialgHomEquiv_apply {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] (f : G →* H) :

mapDomainBialgHomEquiv f = mapDomainBialgHom R f

source

@[simp]

theorem MonoidAlgebra.mapDomainBialgHomEquiv_symm_apply {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [Group G] [Group H] (f : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) :

mapDomainBialgHomEquiv.symm f = mapDomainOfBialgHom f

source

noncomputable def MonoidAlgebra.mapDomainBialgHomMulEquiv {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [CommGroup G] [CommGroup H] :

(G →* H) ≃* (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R 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, map_mul' := ⋯ }

Instances For

source

theorem AddMonoidAlgebra.bialgHom_ext {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] ⦃φ₁ φ₂ : AddMonoidAlgebra R M →ₐc[R] A⦄ (h : ∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) :

φ₁ = φ₂

A R-algebra homomorphism from R[M] is uniquely defined by its values on the functions single a 1.

source

theorem AddMonoidAlgebra.bialgHom_ext' {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] ⦃φ₁ φ₂ : AddMonoidAlgebra R M →ₐc[R] A⦄ (h : (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)) :

φ₁ = φ₂

See note [partially-applied ext lemmas].

source

theorem AddMonoidAlgebra.bialgHom_ext'_iff {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] {φ₁ φ₂ : AddMonoidAlgebra R M →ₐc[R] A} :

φ₁ = φ₂ ↔ (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)

source

@[simp]

theorem AddMonoidAlgebra.counit_domCongr {R : Type u_1} {A : Type u_3} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (x : AddMonoidAlgebra A M) :

CoalgebraStruct.counit ((domCongr R A e) x) = CoalgebraStruct.counit x

source

def AddMonoidAlgebra.domCongrBialgHom (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) :

AddMonoidAlgebra A M ≃ₐc[R] AddMonoidAlgebra A N

Isomorphic monoids have isomorphic monoid algebras.

Equations

AddMonoidAlgebra.domCongrBialgHom R A e = BialgEquiv.ofAlgEquiv (AddMonoidAlgebra.domCongr R A e) ⋯ ⋯

Instances For

source

@[simp]

theorem AddMonoidAlgebra.domCongrBialgHom_apply_toFun (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (a✝ : AddMonoidAlgebra A M) (a : N) :

((domCongrBialgHom R A e) a✝) a = a✝ (e.symm a)

source

@[simp]

theorem AddMonoidAlgebra.domCongrBialgHom_symm_apply_toFun (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (a✝ : AddMonoidAlgebra A N) (a : M) :

((domCongrBialgHom R A e).symm a✝) a = a✝ (e a)

source

@[simp]

theorem AddMonoidAlgebra.domCongrBialgHom_symm_apply_support_val (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (a✝ : AddMonoidAlgebra A N) :

((domCongrBialgHom R A e).symm a✝).support.val = Multiset.map (⇑e.symm) a✝.support.val

source

@[simp]

theorem AddMonoidAlgebra.domCongrBialgHom_apply_support_val (R : Type u_1) (A : Type u_3) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (a✝ : AddMonoidAlgebra A M) :

((domCongrBialgHom R A e) a✝).support.val = Multiset.map (⇑e) a✝.support.val

source

noncomputable def AddMonoidAlgebra.bialgEquivOfSubsingleton {R : Type u_1} (M : Type u_7) [CommSemiring R] [AddMonoid M] [Subsingleton M] :

AddMonoidAlgebra R M ≃ₐc[R] R

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

source

theorem AddMonoidAlgebra.isGroupLikeElem_of {R : Type u_1} {A : Type u_3} {G : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddGroup G] (g : G) :

IsGroupLikeElem R ((of A G) g)

source

@[simp]

theorem AddMonoidAlgebra.isGroupLikeElem_single {R : Type u_1} {A : Type u_3} {G : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddGroup G] (g : G) :

IsGroupLikeElem R (single g 1)

source

@[simp]

theorem AddMonoidAlgebra.span_isGroupLikeElem {R : Type u_1} {A : Type u_3} {G : Type u_4} [CommSemiring R] [Semiring A] [Bialgebra R A] [AddGroup G] :

Submodule.span A {a : AddMonoidAlgebra A G | IsGroupLikeElem R a} = ⊤

A group algebra is spanned by its group-like elements.

source

@[simp]

theorem AddMonoidAlgebra.convMul_algHom_single {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddMonoid M] (f g : AddMonoidAlgebra R M →ₐ[R] A) (x : M) :

(f * g) (single x 1) = f (single x 1) * g (single x 1)

source

@[simp]

theorem AddMonoidAlgebra.convMul_bialgHom_single {R : Type u_1} {A : Type u_3} {M : Type u_7} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [AddCommMonoid M] (f g : AddMonoidAlgebra R M →ₐc[R] A) (x : M) :

(f * g) (single x 1) = f (single x 1) * g (single x 1)

source

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHom_add {R : Type u_1} {M : Type u_7} {N : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] (f g : M →+ N) :

mapDomainBialgHom R (f + g) = mapDomainBialgHom R f * mapDomainBialgHom R g

source

theorem AddMonoidAlgebra.comulAlgHom_comp_mapRangeRingHom {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] (f : R →+* S) :

(Bialgebra.comulAlgHom S (AddMonoidAlgebra S M)).comp (mapRangeRingHom M f) = (Algebra.TensorProduct.mapRingHom f (mapRangeRingHom M f) (mapRangeRingHom M f) ⋯ ⋯).comp (Bialgebra.comulAlgHom R (AddMonoidAlgebra R M)).toRingHom

source

theorem AddMonoidAlgebra.counitAlgHom_comp_mapRangeRingHom {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommSemiring R] [CommSemiring S] [AddCommMonoid M] (f : R →+* S) :

(Bialgebra.counitAlgHom S (AddMonoidAlgebra S M)).comp (mapRangeRingHom M f) = f.comp (Bialgebra.counitAlgHom R (AddMonoidAlgebra R M)).toRingHom

source

@[simp]

theorem AddMonoidAlgebra.isGroupLikeElem_iff_mem_range_of {R : Type u_1} {G : Type u_4} [CommRing R] [IsDomain R] [AddGroup G] {x : AddMonoidAlgebra R G} :

IsGroupLikeElem R x ↔ x ∈ Set.range ⇑(of R G)

source

noncomputable def AddMonoidAlgebra.mapDomainOfBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) :

G →+ H

A bialgebra homomorphism R[G] → R[H] between group algebras over a domain R comes from a group hom G → H.

See AddMonoidAlgebra.mapDomainBialgHom for the forward map.

Equations

AddMonoidAlgebra.mapDomainOfBialgHom f = { toFun := AddMonoidAlgebra.mapDomainOfBialgHomFun✝ f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

theorem AddMonoidAlgebra.single_mapDomainOfBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) (g : G) (r : R) :

single ((mapDomainOfBialgHom f) g) r = f (single g r)

source

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHom_mapDomainOfBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) :

mapDomainBialgHom R (mapDomainOfBialgHom f) = f

source

@[simp]

theorem AddMonoidAlgebra.mapDomainOfBialgHom_mapDomainBialgHom {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] (f : G →+ H) :

mapDomainOfBialgHom (mapDomainBialgHom R f) = f

source

@[simp]

theorem AddMonoidAlgebra.mapDomainOfBialgHom_id {R : Type u_1} {G : Type u_4} [CommRing R] [IsDomain R] [AddGroup G] :

mapDomainOfBialgHom (BialgHom.id R (AddMonoidAlgebra R G)) = AddMonoidHom.id G

source

@[simp]

theorem AddMonoidAlgebra.mapDomainOfBialgHom_comp {R : Type u_1} {G : Type u_4} {H : Type u_5} {I : Type u_6} [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) :

mapDomainOfBialgHom (f.comp g) = (mapDomainOfBialgHom f).comp (mapDomainOfBialgHom g)

source

noncomputable def AddMonoidAlgebra.mapDomainBialgHomEquiv {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] :

(G →+ H) ≃ (AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R 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

source

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHomEquiv_symm_apply {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] (f : AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H) :

mapDomainBialgHomEquiv.symm f = mapDomainOfBialgHom f

source

@[simp]

theorem AddMonoidAlgebra.mapDomainBialgHomEquiv_apply {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddGroup G] [AddGroup H] (f : G →+ H) :

mapDomainBialgHomEquiv f = mapDomainBialgHom R f

source

noncomputable def AddMonoidAlgebra.mapDomainBialgHomAddEquiv {R : Type u_1} {G : Type u_4} {H : Type u_5} [CommRing R] [IsDomain R] [AddCommGroup G] [AddCommGroup H] :

(G →+ H) ≃+ Additive (AddMonoidAlgebra R G →ₐc[R] AddMonoidAlgebra R H)

The group isomorphism between group homs G → H and bialgebra homs R[G] → R[H] of group algebras over a domain.

Equations

AddMonoidAlgebra.mapDomainBialgHomAddEquiv = { toEquiv := AddMonoidAlgebra.mapDomainBialgHomEquiv.trans Additive.ofMul, map_add' := ⋯ }

Instances For

source

noncomputable def MonoidAlgebra.liftGroupLikeAlgHom (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Bialgebra R A] :

MonoidAlgebra R (GroupLike R A) →ₐ[R] A

The R-algebra map from the group algebra on the group-like elements of A to A.

Equations

MonoidAlgebra.liftGroupLikeAlgHom R A = (MonoidAlgebra.lift R (GroupLike R A) A) { toFun := fun (g : GroupLike R A) => ↑g, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem MonoidAlgebra.liftGroupLikeAlgHom_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Bialgebra R A] (a✝ : MonoidAlgebra R (GroupLike R A)) :

(liftGroupLikeAlgHom R A) a✝ = (liftNC ↑(algebraMap R A) fun (g : GroupLike R A) => ↑g) a✝

source

noncomputable def MonoidAlgebra.liftGroupLikeBialgHom (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Bialgebra R A] :

MonoidAlgebra R (GroupLike R A) →ₐc[R] A

The R-bialgebra map from the group algebra on the group-like elements of A to A.

Equations

MonoidAlgebra.liftGroupLikeBialgHom R A = BialgHom.ofAlgHom (MonoidAlgebra.liftGroupLikeAlgHom R A) ⋯ ⋯

Instances For

source

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

(liftGroupLikeBialgHom R A) a✝ = (liftNC ↑(algebraMap R A) fun (g : GroupLike R A) => ↑g) a✝