Documentation

TauCeti.Algebra.Coalgebra.GroupLike.Map

Transport of group-like elements along coalgebra equivalences #

A coalgebra equivalence preserves the group-like equations in both directions and therefore induces an equivalence of group-like elements.

Main declarations #

source
def TauCeti.GroupLike.equivOfCoalgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (e : A ≃ₗc[R] B) :
GroupLike R A ≃ GroupLike R B

A coalgebra equivalence induces an equivalence of group-like elements.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GroupLike.val_equivOfCoalgEquiv {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (e : A ≃ₗc[R] B) (x : GroupLike R A) :
    ↑((equivOfCoalgEquiv e) x) = e ↑x

    The value of the transported group-like element is the image under the coalgebra equivalence.

    source
    @[simp]
    theorem TauCeti.GroupLike.equivOfCoalgEquiv_refl {R : Type u} {A : Type v} [CommSemiring R] [AddCommMonoid A] [Module R A] [Coalgebra R A] :
    equivOfCoalgEquiv (CoalgEquiv.refl R A) = Equiv.refl (GroupLike R A)

    Transport along the identity coalgebra equivalence is the identity equivalence.

    source
    @[simp]
    theorem TauCeti.GroupLike.equivOfCoalgEquiv_trans {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] {C : Type u_1} [AddCommMonoid C] [Module R C] [Coalgebra R C] (e : A ≃ₗc[R] B) (f : B ≃ₗc[R] C) :
    equivOfCoalgEquiv (e.trans f) = (equivOfCoalgEquiv e).trans (equivOfCoalgEquiv f)

    Transport along a composite coalgebra equivalence is the composite transport.

    source
    @[simp]
    theorem TauCeti.GroupLike.equivOfCoalgEquiv_symm {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module R B] [Coalgebra R A] [Coalgebra R B] (e : A ≃ₗc[R] B) :
    (equivOfCoalgEquiv e).symm = equivOfCoalgEquiv e.symm

    Inverting transport is transport along the inverse coalgebra equivalence.