Documentation

TauCeti.Algebra.Coalgebra.Comodule.Transport

Transporting comodules across linear equivalences #

This file records that a right comodule structure can be transported along an R-linear equivalence. This is a small but useful structural prerequisite for the reductive-groups roadmap's Layer 1 representation-category work: tensor products, unitors, associators, and duals of comodules all require moving coactions across canonical linear equivalences without unfolding the definition of a comodule.

Main declarations #

TauCeti.Comodule.Transport: the transported right-comodule structure on the target of a linear equivalence.
TauCeti.Comodule.transportHom: transport a comodule morphism across linear equivalences on source and target.
TauCeti.ComoduleCat.transport: the bundled comodule obtained by transport.
TauCeti.ComoduleCat.transportIso: the bundled isomorphism from the original comodule to its transport.

References #

This supplies infrastructure for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1 target "Comodules over a coalgebra/Hopf algebra", specifically the categorical API needed before tensor products and duals of comodules.

def TauCeti.Comodule.transportCoact {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

N →ₗ[R] TensorProduct R N C

The coaction obtained by transporting a right-comodule structure across a linear equivalence e : M ≃ₗ[R] N.

It sends n to (e ⊗ id) (ρ (e.symm n)).

Equations

TauCeti.Comodule.transportCoact e = TensorProduct.map (↑e) LinearMap.id ∘ₗ TauCeti.Comodule.coact ∘ₗ ↑e.symm

Instances For

@[simp]

theorem TauCeti.Comodule.transportCoact_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (n : N) :

(transportCoact e) n = (TensorProduct.map (↑e) LinearMap.id) (coact (e.symm n))

The transported coaction evaluates as (e ⊗ id) (ρ (e.symm n)).

@[simp]

theorem TauCeti.Comodule.transportCoact_refl {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] :

transportCoact (LinearEquiv.refl R M) = coact

Transporting along the identity linear equivalence leaves the coaction unchanged.

@[implicit_reducible]

def TauCeti.Comodule.Transport {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

Transport a right-comodule structure across a linear equivalence.

If M is a right C-comodule and e : M ≃ₗ[R] N, then N becomes a right C-comodule by the coaction (e ⊗ id) ∘ ρ ∘ e.symm. This definition is intentionally not a global instance: the target module may carry several different coactions.

Equations

TauCeti.Comodule.Transport e = { coact := TauCeti.Comodule.transportCoact e, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

Instances For

@[simp]

theorem TauCeti.Comodule.transport_coact {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

coact = transportCoact e

The transported coaction is (e ⊗ id) ∘ ρ ∘ e.symm.

@[simp]

theorem TauCeti.Comodule.transport_coact_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (n : N) :

coact n = (TensorProduct.map (↑e) LinearMap.id) (coact (e.symm n))

Pointwise form of transport_coact.

@[simp]

theorem TauCeti.Comodule.transportCoact_trans {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] {P : Type y} [AddCommMonoid P] [Module R P] (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] P) :

transportCoact (e ≪≫ₗ f) = transportCoact f

Transported coactions compose in the linear equivalence.

def TauCeti.Comodule.transportHom {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] (eM : M ≃ₗ[R] N) (eN : M' ≃ₗ[R] N') (f : Hom R C M M') :

Hom R C N N'

Transport a comodule morphism across linear equivalences on source and target.

Equations

TauCeti.Comodule.transportHom eM eN f = { toLinearMap := ↑eN ∘ₗ f.toLinearMap ∘ₗ ↑eM.symm, map_coact := ⋯ }

Instances For

@[simp]

theorem TauCeti.Comodule.transportHom_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] (eM : M ≃ₗ[R] N) (eN : M' ≃ₗ[R] N') (f : Hom R C M M') :

(transportHom eM eN f).toLinearMap = ↑eN ∘ₗ f.toLinearMap ∘ₗ ↑eM.symm

Transporting a morphism has the conjugated underlying linear map.

@[simp]

theorem TauCeti.Comodule.transportHom_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] (eM : M ≃ₗ[R] N) (eN : M' ≃ₗ[R] N') (f : Hom R C M M') (n : N) :

(transportHom eM eN f) n = eN (f (eM.symm n))

Pointwise form of transportHom_toLinearMap.

@[simp]

theorem TauCeti.Comodule.transportHom_id {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

transportHom e e (Hom.id R C M) = Hom.id R C N

Transporting the identity morphism gives the identity morphism.

@[simp]

theorem TauCeti.Comodule.transportHom_comp {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] {M' : Type y} {N' : Type z} [AddCommMonoid M'] [Module R M'] [Comodule R C M'] [AddCommMonoid N'] [Module R N'] {P : Type u_1} {P' : Type u_2} [AddCommMonoid P] [Module R P] [Comodule R C P] [AddCommMonoid P'] [Module R P'] (eM : M ≃ₗ[R] N) (eM' : M' ≃ₗ[R] N') (eP : P ≃ₗ[R] P') (f : Hom R C M M') (g : Hom R C M' P) :

transportHom eM eP (g.comp f) = (transportHom eM' eP g).comp (transportHom eM eM' f)

Transporting morphisms preserves composition.

def TauCeti.Comodule.transportToHom {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

Hom R C M N

The forward morphism from a comodule to its transport along a linear equivalence.

Equations

TauCeti.Comodule.transportToHom e = { toLinearMap := ↑e, map_coact := ⋯ }

Instances For

def TauCeti.Comodule.transportInvHom {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

Hom R C N M

The inverse morphism from a transported comodule back to the original comodule.

Equations

TauCeti.Comodule.transportInvHom e = { toLinearMap := ↑e.symm, map_coact := ⋯ }

Instances For

@[simp]

theorem TauCeti.Comodule.transportToHom_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

(transportToHom e).toLinearMap = ↑e

The forward transport morphism has the original linear equivalence underneath.

@[simp]

theorem TauCeti.Comodule.transportInvHom_toLinearMap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

(transportInvHom e).toLinearMap = ↑e.symm

The inverse transport morphism has the inverse linear equivalence underneath.

@[simp]

theorem TauCeti.Comodule.transportToHom_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (m : M) :

(transportToHom e) m = e m

Pointwise form of transportToHom_toLinearMap.

@[simp]

theorem TauCeti.Comodule.transportInvHom_apply {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (n : N) :

(transportInvHom e) n = e.symm n

Pointwise form of transportInvHom_toLinearMap.

def TauCeti.ComoduleCat.transport (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type x} [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

ComoduleCat R C

Bundle the transport of a comodule structure across a linear equivalence.

Equations

TauCeti.ComoduleCat.transport R C e = { carrier := N, isAddCommMonoid := inst✝¹, isModule := inst✝, instComodule := TauCeti.Comodule.Transport e }

Instances For

@[simp]

theorem TauCeti.ComoduleCat.transport_coact (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N : Type x} [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) :

Comodule.coact = Comodule.transportCoact e

The coaction on ComoduleCat.transport is the transported coaction.

def TauCeti.ComoduleCat.transportIso (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N₀ : Type w} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) :

of R C M ≅ transport R C e

The categorical isomorphism from a comodule to its transport along a linear equivalence.

Equations

TauCeti.ComoduleCat.transportIso R C e = { hom := TauCeti.Comodule.transportToHom e, inv := TauCeti.Comodule.transportInvHom e, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem TauCeti.ComoduleCat.transportIso_hom_toLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N₀ : Type w} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) :

(transportIso R C e).hom.toLinearMap = ↑e

The transport isomorphism has the original linear equivalence as its forward map.

@[simp]

theorem TauCeti.ComoduleCat.transportIso_inv_toLinearMap (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N₀ : Type w} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) :

(transportIso R C e).inv.toLinearMap = ↑e.symm

The transport isomorphism has the inverse linear equivalence as its inverse map.

@[simp]

theorem TauCeti.ComoduleCat.transportIso_hom_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N₀ : Type w} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) (m : M) :

(CategoryTheory.ConcreteCategory.hom (transportIso R C e).hom) m = e m

The forward map of the transport isomorphism applies as the original linear equivalence.

@[simp]

theorem TauCeti.ComoduleCat.transportIso_inv_apply (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} [AddCommMonoid M] [Module R M] [Comodule R C M] {N₀ : Type w} [AddCommMonoid N₀] [Module R N₀] (e : M ≃ₗ[R] N₀) (n : N₀) :

(CategoryTheory.ConcreteCategory.hom (transportIso R C e).inv) n = e.symm n

The inverse map of the transport isomorphism applies as the inverse linear equivalence.