Documentation

TauCeti.Algebra.Coalgebra.Subcomodule.Transport

Transport of subcomodules #

Mutually inverse comodule morphisms identify the corresponding subcomodule lattices by taking images. In particular, transporting a comodule structure along a linear equivalence preserves its subcomodules and their underlying submodules.

This is Layer 1 infrastructure for the reductive-groups roadmap: changing the carrier of a comodule must preserve its invariant subspaces.

Main declarations #

source
def TauCeti.Subcomodule.mapOrderIso {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Comodule.Hom R C M N) (g : Comodule.Hom R C N M) (hgf : g.comp f = Comodule.Hom.id R C M) (hfg : f.comp g = Comodule.Hom.id R C N) :
Subcomodule R C M ≃o Subcomodule R C N

Mutually inverse comodule morphisms identify the lattices of subcomodules by taking images.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Subcomodule.mapOrderIso_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Comodule.Hom R C M N) (g : Comodule.Hom R C N M) (hgf : g.comp f = Comodule.Hom.id R C M) (hfg : f.comp g = Comodule.Hom.id R C N) (A : Subcomodule R C M) :
    (mapOrderIso f g hgf hfg) A = A.map f

    The forward correspondence induced by mutually inverse comodule morphisms is image under the forward morphism.

    source
    @[simp]
    theorem TauCeti.Subcomodule.mapOrderIso_symm_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Comodule.Hom R C M N) (g : Comodule.Hom R C N M) (hgf : g.comp f = Comodule.Hom.id R C M) (hfg : f.comp g = Comodule.Hom.id R C N) (A : Subcomodule R C N) :
    (mapOrderIso f g hgf hfg).symm A = A.map g

    The inverse correspondence induced by mutually inverse comodule morphisms is image under the inverse morphism.

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

    Transporting a comodule along a linear equivalence identifies its subcomodule lattice with the original one.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Subcomodule.transportOrderIso_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (A : Subcomodule R C M) :
      (transportOrderIso e) A = A.map (Comodule.transportToHom e)

      The forward transport correspondence is image under the transport equivalence.

      source
      @[simp]
      theorem TauCeti.Subcomodule.transportOrderIso_symm_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (A : Subcomodule R C N) :
      (transportOrderIso e).symm A = A.map (Comodule.transportInvHom e)

      The inverse transport correspondence is image under the inverse transport equivalence.

      source
      theorem TauCeti.Subcomodule.transportOrderIso_apply_toSubmodule {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (A : Subcomodule R C M) :
      ((transportOrderIso e) A).toSubmodule = (Submodule.orderIsoMapComap e) A.toSubmodule

      The forward transport correspondence maps the underlying submodule along the linear equivalence.

      source
      theorem TauCeti.Subcomodule.transportOrderIso_symm_apply_toSubmodule {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] (e : M ≃ₗ[R] N) (A : Subcomodule R C N) :
      ((transportOrderIso e).symm A).toSubmodule = (Submodule.orderIsoMapComap e).symm A.toSubmodule

      The inverse transport correspondence maps the underlying submodule along the inverse linear equivalence.