Documentation

TauCeti.Algebra.Bialgebra.GroupLike.Evaluation

Evaluation of the group-like monoid algebra #

Every bialgebra H over a commutative semiring R receives a canonical bialgebra morphism from the monoid algebra on its group-like elements. It sends each standard basis element to its underlying group-like element. Its linear range is exactly the span of the group-like elements, and its subcoalgebra image is the subcoalgebra spanned by all group-like elements. The morphism is injective exactly when the underlying group-like elements are linearly independent, and it is a bialgebra equivalence when they are also spanning. Over a commutative domain, linear independence is automatic when the carrier of H is torsion-free.

Main declarations #

References #

The automatic linear independence used in the domain and torsion-free specialization is the domain-valued form of Milne, Algebraic Groups, Proposition 4.23. The reconstruction in the spanning case is the bialgebra form underlying Definition 12.7 and Theorem 12.8 of the same reference.

source
noncomputable def TauCeti.GroupLike.evaluationBialgHom (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
MonoidAlgebra R (GroupLike R H) →ₐc[R] H

The canonical bialgebra morphism from the monoid algebra on the group-like elements of H to H, sending each standard basis element to its underlying group-like element.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GroupLike.evaluationBialgHom_single (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] (g : GroupLike R H) (r : R) :
    (evaluationBialgHom R H) (MonoidAlgebra.single g r) = r • ↑g

    Evaluation on a scalar multiple of a standard basis element.

    source
    theorem TauCeti.GroupLike.evaluationBialgHom_apply (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] (x : MonoidAlgebra R (GroupLike R H)) :
    (evaluationBialgHom R H) x = x.coeff.sum fun (g : GroupLike R H) (r : R) => r • ↑g

    Evaluation of a monoid-algebra element is the finite linear combination of its group-like indices with its coefficients.

    source
    theorem TauCeti.GroupLike.evaluationBialgHom_toLinearMap (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    ↑(evaluationBialgHom R H) = Finsupp.linearCombination R GroupLike.val ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv R)

    Evaluation is finite linear combination of the underlying group-like elements after passing to the coefficient representation of the monoid algebra.

    source
    theorem TauCeti.GroupLike.range_evaluationBialgHom (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    (↑(evaluationBialgHom R H)).range = Submodule.span R (Set.range GroupLike.val)

    The linear range of evaluation is the span of the underlying group-like elements.

    source
    theorem TauCeti.GroupLike.range_evaluationBialgHom_eq_groupLikeSetSpan_toSubmodule (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    (↑(evaluationBialgHom R H)).range = (Subcoalgebra.groupLikeSetSpan Set.univ).toSubmodule

    The linear range of evaluation is the underlying submodule of the subcoalgebra spanned by all group-like elements.

    source
    theorem TauCeti.GroupLike.map_top_evaluationBialgHom (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    Subcoalgebra.map ↑(evaluationBialgHom R H) ⊤ = Subcoalgebra.groupLikeSetSpan Set.univ

    The image of the full source subcoalgebra under evaluation is the subcoalgebra spanned by all group-like elements.

    source
    theorem TauCeti.GroupLike.evaluationBialgHom_surjective_iff_span_eq_top (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    Function.Surjective ⇑(evaluationBialgHom R H) ↔ Submodule.span R (Set.range GroupLike.val) = ⊤

    Evaluation is surjective exactly when the group-like elements span the whole bialgebra.

    source
    theorem TauCeti.GroupLike.evaluationBialgHom_surjective_iff_groupLikeSetSpan_eq_top (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    Function.Surjective ⇑(evaluationBialgHom R H) ↔ Subcoalgebra.groupLikeSetSpan Set.univ = ⊤

    Evaluation is surjective exactly when the subcoalgebra spanned by all group-like elements is the full subcoalgebra.

    source
    theorem TauCeti.GroupLike.evaluationBialgHom_injective_iff_linearIndependent (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] :
    Function.Injective ⇑(evaluationBialgHom R H) ↔ LinearIndependent R GroupLike.val

    Evaluation is injective exactly when the underlying group-like elements are linearly independent.

    source
    noncomputable def TauCeti.GroupLike.evaluationBialgEquivOfLinearIndependentOfSpanEqTop (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] (hlinear : LinearIndependent R GroupLike.val) (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) :
    MonoidAlgebra R (GroupLike R H) ≃ₐc[R] H

    If the underlying group-like elements are linearly independent and span the bialgebra, evaluation is a bialgebra equivalence.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GroupLike.evaluationBialgEquivOfLinearIndependentOfSpanEqTop_apply (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] (hlinear : LinearIndependent R GroupLike.val) (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) (x : MonoidAlgebra R (GroupLike R H)) :
      (evaluationBialgEquivOfLinearIndependentOfSpanEqTop R H hlinear hspan) x = (evaluationBialgHom R H) x

      The general bialgebra equivalence obtained from linear independence and spanning applies as evaluation.

      source
      @[simp]
      theorem TauCeti.GroupLike.evaluationBialgEquivOfLinearIndependentOfSpanEqTop_toBialgHom (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Bialgebra R H] (hlinear : LinearIndependent R GroupLike.val) (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) :
      ↑(evaluationBialgEquivOfLinearIndependentOfSpanEqTop R H hlinear hspan) = evaluationBialgHom R H

      The bialgebra morphism underlying the general equivalence from linear independence and spanning is evaluation.

      source
      theorem TauCeti.GroupLike.evaluationBialgHom_injective (R : Type u) (H : Type v) [CommRing R] [IsDomain R] [Ring H] [Bialgebra R H] [Module.IsTorsionFree R H] :
      Function.Injective ⇑(evaluationBialgHom R H)

      Over a commutative domain, evaluation is injective when the carrier is torsion-free.

      source
      noncomputable def TauCeti.GroupLike.evaluationBialgEquiv (R : Type u) (H : Type v) [CommRing R] [IsDomain R] [Ring H] [Bialgebra R H] [Module.IsTorsionFree R H] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) :
      MonoidAlgebra R (GroupLike R H) ≃ₐc[R] H

      If the group-like elements span a torsion-free bialgebra over a commutative domain, evaluation is a bialgebra equivalence.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.GroupLike.evaluationBialgEquiv_apply (R : Type u) (H : Type v) [CommRing R] [IsDomain R] [Ring H] [Bialgebra R H] [Module.IsTorsionFree R H] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) (x : MonoidAlgebra R (GroupLike R H)) :
        (evaluationBialgEquiv R H hspan) x = (evaluationBialgHom R H) x

        The bialgebra equivalence obtained from spanning applies as evaluation.

        source
        @[simp]
        theorem TauCeti.GroupLike.evaluationBialgEquiv_toBialgHom (R : Type u) (H : Type v) [CommRing R] [IsDomain R] [Ring H] [Bialgebra R H] [Module.IsTorsionFree R H] (hspan : Submodule.span R (Set.range GroupLike.val) = ⊤) :
        ↑(evaluationBialgEquiv R H hspan) = evaluationBialgHom R H

        The bialgebra morphism underlying the spanning equivalence is evaluation.