Documentation

TauCeti.Algebra.Coalgebra.Subcomodule.Comap

Inverse images of subcomodules #

This file adds inverse images of subcomodules under comodule morphisms. If f : M → N is a morphism of right comodules and B ≤ N is a subcomodule, then B.comap f has underlying submodule B.toSubmodule.comap f. Stability under the coaction follows by applying tensor-product right exactness to the quotient map N → N / B.

This is Layer 1 infrastructure for the reductive-groups roadmap target on comodules: subobjects of representations need both images and inverse images before kernels, finite-subcomodule constructions, and the representation/comodule dictionary can be used comfortably.

Main declarations #

References #

The construction is the standard inverse image of a subcomodule; see Sweedler, Hopf Algebras, Chapter 2. The exactness step reuses Mathlib's TensorProduct.rTensor_exact and LinearMap.exact_subtype_ker_map.

source
def TauCeti.Subcomodule.comap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (B : Subcomodule R C N) (f : Comodule.Hom R C M N) :
Subcomodule R C M

The inverse image of a subcomodule under a comodule morphism.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Subcomodule.comap_toSubmodule {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (B : Subcomodule R C N) (f : Comodule.Hom R C M N) :
    (B.comap f).toSubmodule = Submodule.comap f.toLinearMap B.toSubmodule

    The underlying submodule of an inverse-image subcomodule is the inverse image of the underlying submodule.

    source
    theorem TauCeti.Subcomodule.comap_finite {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (B : Subcomodule R C N) (f : Comodule.Hom R C M N) [IsNoetherian R M] :
    Module.Finite R ↥(B.comap f).toSubmodule

    The inverse image of a subcomodule into a noetherian module is finitely generated as an R-module.

    source
    @[simp]
    theorem TauCeti.Subcomodule.mem_comap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {B : Subcomodule R C N} {f : Comodule.Hom R C M N} {m : M} :
    m ∈ B.comap f ↔ f m ∈ B

    Membership in an inverse-image subcomodule.

    source
    theorem TauCeti.Subcomodule.comap_mono {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [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) {B D : Subcomodule R C N} (hBD : B ≤ D) :
    B.comap f ≤ D.comap f

    The inverse-image construction is monotone in the target subcomodule.

    source
    @[simp]
    theorem TauCeti.Subcomodule.comap_top {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [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) :
    ⊤.comap f = ⊤

    The inverse image of the top subcomodule is top.

    source
    @[simp]
    theorem TauCeti.Subcomodule.comap_bot_toSubmodule {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [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) :
    (⊥.comap f).toSubmodule = f.ker

    The underlying submodule of the inverse image of the bottom subcomodule is the kernel.

    source
    theorem TauCeti.Subcomodule.map_le_iff_le_comap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {A : Subcomodule R C M} {B : Subcomodule R C N} {f : Comodule.Hom R C M N} :
    A.map f ≤ B ↔ A ≤ B.comap f

    Images are left adjoint to inverse images for subcomodules.

    source
    theorem TauCeti.Subcomodule.gc_map_comap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [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) :
    GaloisConnection (fun (A : Subcomodule R C M) => A.map f) fun (B : Subcomodule R C N) => B.comap f

    The image construction is left adjoint to inverse image for subcomodules.

    source
    theorem TauCeti.Subcomodule.le_comap_map {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (A : Subcomodule R C M) (f : Comodule.Hom R C M N) :
    A ≤ (A.map f).comap f

    A subcomodule is contained in the inverse image of its image.

    source
    theorem TauCeti.Subcomodule.le_comap_map_of_le {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {A D : Subcomodule R C M} (hAD : A ≤ D) (f : Comodule.Hom R C M N) :
    A ≤ (D.map f).comap f

    A subcomodule is contained in the inverse image of the image of a larger subcomodule.

    source
    theorem TauCeti.Subcomodule.map_comap_le {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (B : Subcomodule R C N) (f : Comodule.Hom R C M N) :
    (B.comap f).map f ≤ B

    The image of the inverse image of a subcomodule is contained in the subcomodule.

    source
    @[simp]
    theorem TauCeti.Subcomodule.comap_comap {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type y} [AddCommMonoid P] [Module R P] [Comodule R C P] (B : Subcomodule R C P) (f : Comodule.Hom R C M N) (g : Comodule.Hom R C N P) :
    (B.comap g).comap f = B.comap (g.comp f)

    Inverse images compose contravariantly with comodule morphisms.

    source
    @[simp]
    theorem TauCeti.Subcomodule.comap_id {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (B : Subcomodule R C M) :
    B.comap (Comodule.Hom.id R C M) = B

    The inverse image along the identity comodule morphism is the original subcomodule.

    source
    def TauCeti.Comodule.Hom.ker {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) :
    Subcomodule R C M

    The kernel of a comodule morphism as a subcomodule of the domain.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Comodule.Hom.ker_toSubmodule {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) :
      f.ker.toSubmodule = f.ker

      The underlying submodule of the kernel subcomodule is the linear-map kernel.

      source
      theorem TauCeti.Comodule.Hom.ker_finite {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) [IsNoetherian R M] :
      Module.Finite R ↥f.ker.toSubmodule

      The kernel of a comodule morphism out of a noetherian module is finitely generated as an R-module.

      source
      @[simp]
      theorem TauCeti.Comodule.Hom.mem_ker {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {f : Hom R C M N} {m : M} :
      m ∈ f.ker ↔ f m = 0

      Membership in the kernel subcomodule is vanishing under the morphism.

      source
      theorem TauCeti.Comodule.Hom.zero_mem_ker {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (f : Hom R C M N) :
      0 ∈ f.ker

      The kernel subcomodule contains zero.

      source
      theorem TauCeti.Comodule.Hom.le_ker_iff {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {f : Hom R C M N} {A : Subcomodule R C M} :
      A ≤ f.ker ↔ ∀ ⦃m : M⦄, m ∈ A → f m = 0

      A subcomodule is contained in the kernel exactly when the morphism vanishes on it.

      source
      theorem TauCeti.Comodule.Hom.mem_ker_of_apply_eq_zero {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {f : Hom R C M N} {m : M} (hm : f m = 0) :
      m ∈ f.ker

      An element whose image under a comodule morphism is zero belongs to its kernel.