Documentation

TauCeti.Algebra.Bialgebra.MonoidAlgebra.GroupLike

Group-like elements of monoid algebras #

The standard basis elements of a monoid algebra over a commutative semiring are group-like and span the whole algebra. Over a commutative ring with connected prime spectrum, these are exactly the group-like elements. The proof of the classification compares coefficients in the group-like comultiplication identity. Connectedness makes every idempotent coefficient zero or one, and the counit condition excludes the zero element.

Consequently, a bialgebra morphism between monoid algebras over such a base uniquely recovers the monoid homomorphism on their standard basis indices. This gives a two-sided inverse to MonoidAlgebra.mapDomainBialgHom on the corresponding hom-sets.

Main declarations #

source
theorem TauCeti.MonoidAlgebra.groupLikeSetSpan_eq_top (R : Type u) [CommSemiring R] (G : Type v) :
Subcoalgebra.groupLikeSetSpan Set.univ = ⊤

The group-like elements of a monoid algebra span the whole algebra: every standard basis element is group-like, and the standard basis spans.

source
theorem TauCeti.MonoidAlgebra.isGroupLikeElem_iff_eq_single (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {H : Type v} [Monoid H] (x : MonoidAlgebra R H) :
IsGroupLikeElem R x ↔ ∃! h : H, x = MonoidAlgebra.single h 1

Over a commutative ring with connected prime spectrum, the group-like elements of a monoid algebra are exactly its standard basis elements, with a unique basis index.

source
noncomputable def TauCeti.MonoidAlgebra.groupLikeEquiv (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {H : Type w} [Monoid H] :
GroupLike R (MonoidAlgebra R H) ≃* H

The group-like elements of a monoid algebra over a connected base are its standard basis elements, multiplicatively identified with the index monoid.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.MonoidAlgebra.groupLikeEquiv_apply_eq_iff (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {H : Type w} [Monoid H] (x : GroupLike R (MonoidAlgebra R H)) (h : H) :
    (groupLikeEquiv R) x = h ↔ ↑x = MonoidAlgebra.single h 1

    The standard basis index recovered from a group-like element is characterized by its underlying value.

    source
    @[simp]
    theorem TauCeti.MonoidAlgebra.val_groupLikeEquiv_symm (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {H : Type w} [Monoid H] (h : H) :
    ↑((groupLikeEquiv R).symm h) = MonoidAlgebra.single h 1

    The inverse image of an index under groupLikeEquiv is the corresponding standard basis element.

    source
    noncomputable def TauCeti.MonoidAlgebra.mapDomainBialgHomPreimage (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (F : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) :
    G →* H

    Recover the monoid homomorphism inducing a bialgebra morphism between monoid algebras over a base with connected prime spectrum.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem TauCeti.MonoidAlgebra.mapDomainBialgHomPreimage_apply_eq_iff (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (F : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) (g : G) (h : H) :
      (mapDomainBialgHomPreimage R F) g = h ↔ F (MonoidAlgebra.single g 1) = MonoidAlgebra.single h 1

      The recovered monoid homomorphism takes g to h exactly when the bialgebra morphism takes the corresponding standard basis element to the standard basis element indexed by h.

      source
      @[simp]
      theorem TauCeti.MonoidAlgebra.mapDomainBialgHomPreimage_single (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (F : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) (g : G) :
      F (MonoidAlgebra.single g 1) = MonoidAlgebra.single ((mapDomainBialgHomPreimage R F) g) 1

      The image of a standard basis element under a bialgebra morphism is indexed by the recovered monoid homomorphism.

      source
      @[simp]
      theorem TauCeti.MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHomPreimage (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (F : MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H) :
      MonoidAlgebra.mapDomainBialgHom R (mapDomainBialgHomPreimage R F) = F

      Mapping the domain by the recovered monoid homomorphism gives the original bialgebra morphism.

      source
      theorem TauCeti.MonoidAlgebra.mapDomainBialgHom_injective (R : Type u) [CommSemiring R] [Nontrivial R] {G : Type v} {H : Type w} [Monoid G] [Monoid H] :
      Function.Injective (MonoidAlgebra.mapDomainBialgHom R)

      Over a nontrivial base, distinct monoid homomorphisms induce distinct bialgebra morphisms between monoid algebras.

      source
      @[simp]
      theorem TauCeti.MonoidAlgebra.mapDomainBialgHomPreimage_mapDomainBialgHom (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G : Type v} {H : Type w} [Monoid G] [Monoid H] (φ : G →* H) :
      mapDomainBialgHomPreimage R (MonoidAlgebra.mapDomainBialgHom R φ) = φ

      Recovering from the bialgebra morphism induced by a monoid homomorphism returns that monoid homomorphism.

      source
      theorem TauCeti.MonoidAlgebra.mapDomainBialgHom_surjective (R : Type u) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] {G : Type v} {H : Type w} [Monoid G] [Monoid H] :
      Function.Surjective (MonoidAlgebra.mapDomainBialgHom R)

      Every bialgebra morphism between monoid algebras over a base with connected prime spectrum is induced by a monoid homomorphism.