Documentation

TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Adjoin

Subobjects generated by matrix coefficients #

This file packages the linear span and algebra generated by the matrix coefficients of a right comodule, together with their basic functoriality under comodule morphisms. These are bookkeeping objects for the faithful-representation criterion in the reductive-groups roadmap. For a finite projective comodule over a commutative Hopf algebra, the closed-immersion criterion uses the original coefficients together with their antipode images, equivalently the coefficients of the comodule together with its dual; see TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Dual.

Main definitions #

References #

This is standard coalgebra/comodule terminology; see Sweedler, Hopf Algebras, Chapter 2. It supplies a prerequisite for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1, "Faithfulness done right". The necessary antipode closure of the original coefficients is developed in TauCeti.Algebra.Coalgebra.Comodule.MatrixCoefficient.Dual.

source
def TauCeti.Comodule.matrixCoefficientSet {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] :
Set C

The set of all matrix coefficients of a right comodule.

Equations
Instances For
    source
    theorem TauCeti.Comodule.matrixCoefficientSet_def {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] :
    matrixCoefficientSet = Set.range (Function.uncurry matrixCoefficient)

    The matrix coefficient set is the range of the uncurried matrix coefficient map.

    source
    @[simp]
    theorem TauCeti.Comodule.matrixCoefficient_mem_set {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] (φ : M →ₗ[R] R) (m : M) :
    matrixCoefficient φ m ∈ matrixCoefficientSet

    A matrix coefficient belongs to the set of all matrix coefficients.

    source
    theorem TauCeti.Comodule.mem_matrixCoefficientSet_iff {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] (c : C) :
    c ∈ matrixCoefficientSet ↔ ∃ (φ : M →ₗ[R] R) (m : M), matrixCoefficient φ m = c

    Membership in the set of matrix coefficients is the existence of a functional and a vector giving the element.

    source
    def TauCeti.Comodule.matrixCoefficientSubmodule {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] :
    Submodule R C

    The R-submodule spanned by all matrix coefficients of a right comodule.

    Equations
    Instances For
      source
      theorem TauCeti.Comodule.matrixCoefficientSubmodule_def {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] :
      matrixCoefficientSubmodule = Submodule.span R matrixCoefficientSet

      The matrix coefficient submodule is the span of the matrix coefficient set.

      source
      @[simp]
      theorem TauCeti.Comodule.matrixCoefficient_mem_submodule {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] (φ : M →ₗ[R] R) (m : M) :
      matrixCoefficient φ m ∈ matrixCoefficientSubmodule

      A matrix coefficient belongs to the submodule spanned by all matrix coefficients.

      source
      theorem TauCeti.Comodule.matrixCoefficientSubmodule_le {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] {P : Submodule R C} (hP : ∀ (φ : M →ₗ[R] R) (m : M), matrixCoefficient φ m ∈ P) :
      matrixCoefficientSubmodule ≤ P

      The coefficient submodule is the smallest submodule containing all matrix coefficients.

      source
      theorem TauCeti.Comodule.matrixCoefficientSubmodule_le_iff {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] {P : Submodule R C} :
      matrixCoefficientSubmodule ≤ P ↔ ∀ (φ : M →ₗ[R] R) (m : M), matrixCoefficient φ m ∈ P

      The coefficient submodule is contained in a submodule iff that submodule contains each matrix coefficient.

      source
      theorem TauCeti.Comodule.range_matrixCoefficientTensor {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] :
      matrixCoefficientTensor.range = matrixCoefficientSubmodule

      The range of the tensor-linearized matrix-coefficient map is exactly the submodule spanned by all matrix coefficients.

      source
      theorem TauCeti.Comodule.matrixCoefficient_mem_set_of_map {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] [Comodule R C N] (f : Hom R C M N) (φ : N →ₗ[R] R) (m : M) :
      matrixCoefficient φ (f m) ∈ matrixCoefficientSet

      The matrix coefficient of the image of a vector under a comodule morphism is a matrix coefficient of the source comodule.

      source
      theorem TauCeti.Comodule.matrixCoefficientSet_subset_of_surjective {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] [Comodule R C N] (f : Hom R C M N) (hf : Function.Surjective ⇑f) :
      matrixCoefficientSet ⊆ matrixCoefficientSet

      If f : M → N is a surjective comodule morphism, every matrix coefficient of N is a matrix coefficient of M.

      source
      theorem TauCeti.Comodule.matrixCoefficientSubmodule_le_of_surjective {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] [Comodule R C N] (f : Hom R C M N) (hf : Function.Surjective ⇑f) :
      matrixCoefficientSubmodule ≤ matrixCoefficientSubmodule

      A surjective comodule morphism makes the coefficient submodule of the target contained in the coefficient submodule of the source.

      source
      theorem TauCeti.Comodule.matrixCoefficientSet_eq_of_inverse_hom {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] [Comodule R C N] (f : Hom R C M N) (g : Hom R C N M) (hfg : ∀ (n : N), f (g n) = n) (hgf : ∀ (m : M), g (f m) = m) :
      matrixCoefficientSet = matrixCoefficientSet

      Inverse comodule morphisms identify the coefficient sets.

      source
      theorem TauCeti.Comodule.matrixCoefficientSubmodule_eq_of_inverse_hom {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] [Comodule R C N] (f : Hom R C M N) (g : Hom R C N M) (hfg : ∀ (n : N), f (g n) = n) (hgf : ∀ (m : M), g (f m) = m) :
      matrixCoefficientSubmodule = matrixCoefficientSubmodule

      Inverse comodule morphisms identify the coefficient submodules.

      source
      def TauCeti.Comodule.matrixCoefficientSubalgebra {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] :
      Subalgebra R C

      The R-subalgebra generated by all matrix coefficients of a right comodule.

      For a finite projective comodule over a commutative Hopf algebra, a closed-immersion criterion uses this subalgebra together with its antipode image, equivalently the coefficient subalgebra of the product with the dual comodule.

      Equations
      Instances For
        source
        theorem TauCeti.Comodule.matrixCoefficientSubalgebra_def {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] :
        matrixCoefficientSubalgebra = Algebra.adjoin R matrixCoefficientSet

        The matrix coefficient subalgebra is the algebra generated by the matrix coefficient set.

        source
        @[simp]
        theorem TauCeti.Comodule.matrixCoefficient_mem_subalgebra {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (φ : M →ₗ[R] R) (m : M) :
        matrixCoefficient φ m ∈ matrixCoefficientSubalgebra

        A matrix coefficient belongs to the algebra generated by all matrix coefficients.

        source
        theorem TauCeti.Comodule.matrixCoefficientSubalgebra_le {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {S : Subalgebra R C} (hS : ∀ (φ : M →ₗ[R] R) (m : M), matrixCoefficient φ m ∈ S) :
        matrixCoefficientSubalgebra ≤ S

        The coefficient algebra is the smallest subalgebra containing all matrix coefficients.

        source
        theorem TauCeti.Comodule.matrixCoefficientSubalgebra_le_iff {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] {S : Subalgebra R C} :
        matrixCoefficientSubalgebra ≤ S ↔ ∀ (φ : M →ₗ[R] R) (m : M), matrixCoefficient φ m ∈ S

        The coefficient algebra is contained in a subalgebra iff that subalgebra contains each matrix coefficient.

        source
        theorem TauCeti.Comodule.matrixCoefficientSubalgebra_eq_top_of_submodule_eq_top {R : Type u} {C : Type v} {M : Type w} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra R C] [AddCommMonoid M] [Module R M] [Comodule R C M] (h : matrixCoefficientSubmodule = ⊤) :
        matrixCoefficientSubalgebra = ⊤

        If the matrix coefficients linearly span the coalgebra, then they generate the ambient algebra.

        source
        theorem TauCeti.Comodule.matrixCoefficientSubalgebra_le_of_surjective {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra 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) (hf : Function.Surjective ⇑f) :
        matrixCoefficientSubalgebra ≤ matrixCoefficientSubalgebra

        A surjective comodule morphism makes the coefficient algebra of the target contained in the coefficient algebra of the source.

        source
        theorem TauCeti.Comodule.matrixCoefficientSubalgebra_eq_of_inverse_hom {R : Type u} {C : Type v} {M : Type w} {N : Type x} [CommSemiring R] [Semiring C] [Algebra R C] [Coalgebra 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) (g : Hom R C N M) (hfg : ∀ (n : N), f (g n) = n) (hgf : ∀ (m : M), g (f m) = m) :
        matrixCoefficientSubalgebra = matrixCoefficientSubalgebra

        Inverse comodule morphisms identify the coefficient algebras.