Functoriality of group-like elements

A bialgebra morphism sends group-like elements to group-like elements and respects their multiplication. This file bundles that operation as a monoid homomorphism and records that a bialgebra equivalence induces a multiplicative equivalence of group-like elements.

Main declarations

• TauCeti.GroupLike.map: the homomorphism on group-like elements induced by a bialgebra map.
• TauCeti.GroupLike.groupLikeSetSpan_eq_top_of_surjective: a surjective bialgebra map preserves spanning by group-like elements.
• TauCeti.GroupLike.mapEquiv: the equivalence induced by a bialgebra equivalence.

def TauCeti.GroupLike.map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A →ₐc[R] B) : GroupLike R A →* GroupLike R B

A bialgebra morphism induces a monoid homomorphism on group-like elements.

Equations

• TauCeti.GroupLike.map f = { toFun := fun (x : GroupLike R A) => { val := f ↑x, isGroupLikeElem_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GroupLike.val_map {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A →ₐc[R] B) (x : GroupLike R A) : ↑((map f) x) = f ↑x

The underlying value of the image of a group-like element is its image under the bialgebra morphism.

@[simp]

theorem TauCeti.GroupLike.map_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] : map (BialgHom.id R A) = MonoidHom.id (GroupLike R A)

Mapping group-like elements respects identity bialgebra morphisms.

@[simp]

theorem TauCeti.GroupLike.map_comp {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] {C : Type u_1} [Semiring C] [Bialgebra R C] (g : B →ₐc[R] C) (f : A →ₐc[R] B) : map (g.comp f) = (map g).comp (map f)

Mapping group-like elements respects composition of bialgebra morphisms.

theorem TauCeti.GroupLike.groupLikeSetSpan_eq_top_of_surjective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (f : A →ₐc[R] B) (hf : Function.Surjective ⇑f) (hA : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤) : Subcoalgebra.groupLikeSetSpan Set.univ = ⊤

A surjective bialgebra morphism preserves spanning by group-like elements.

def TauCeti.GroupLike.mapEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (e : A ≃ₐc[R] B) : GroupLike R A ≃* GroupLike R B

A bialgebra equivalence induces a multiplicative equivalence of group-like elements.

Equations

• TauCeti.GroupLike.mapEquiv e = { toEquiv := TauCeti.GroupLike.equivOfCoalgEquiv e.toCoalgEquiv, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GroupLike.val_mapEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (e : A ≃ₐc[R] B) (x : GroupLike R A) : ↑((mapEquiv e) x) = e ↑x

The underlying value of mapEquiv is the original bialgebra equivalence.

@[simp]

theorem TauCeti.GroupLike.mapEquiv_refl {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Bialgebra R A] : mapEquiv (BialgEquiv.refl R A) = MulEquiv.refl (GroupLike R A)

Mapping group-like elements along the identity equivalence is the identity equivalence.

@[simp]

theorem TauCeti.GroupLike.mapEquiv_trans {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] {C : Type u_1} [Semiring C] [Bialgebra R C] (e : A ≃ₐc[R] B) (f : B ≃ₐc[R] C) : mapEquiv (e.trans f) = (mapEquiv e).trans (mapEquiv f)

Mapping group-like elements along a composite equivalence is the composite of the maps.

@[simp]

theorem TauCeti.GroupLike.mapEquiv_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Bialgebra R A] [Bialgebra R B] (e : A ≃ₐc[R] B) : (mapEquiv e).symm = mapEquiv e.symm

The inverse of the induced equivalence is induced by the inverse equivalence.