Documentation

TauCeti.Algebra.Group.FreeCommMonoidCharacter

Characters of a free commutative monoid #

The free commutative monoid on an index type σ is modelled as Multiplicative (σ →₀ ℕ): its underlying additive monoid σ →₀ ℕ is the free ℕ-module on σ. This file records its universal property in the form most useful for the functor of points of an affine semigroup: a homomorphism Multiplicative (σ →₀ ℕ) →* M to a commutative monoid M is the same data as a family σ → M.

The equivalence sends a homomorphism χ to its values i ↦ χ (ofAdd (single i 1)) on the standard generators, and a family c : σ → M to the unique homomorphism extending it. This is the many-generator version of Mathlib's powersHom : M ≃ (Multiplicative ℕ →* M) (the case of one generator), and the monoid counterpart of TauCeti.freeAbelianCharEquiv in TauCeti.Algebra.Group.FreeAbelianCharacter: no invertibility is imposed on the values. The two appear together whenever a semigroup splits as a product of a free commutative monoid and a free abelian group, as the dual semigroup of a smooth cone does; the values of a character on the free monoid factor may vanish, while those on the free abelian factor are units.

Main definitions #

References #

The construction reuses Mathlib's group-algebra-free toolkit: the Finsupp.liftAddHom universal property of σ →₀ ℕ, the ℕ-power homomorphism multiplesHom, and the type-tag adjunction AddMonoidHom.toMultiplicativeLeft from Mathlib.Algebra.Group.TypeTags.Hom.

source
noncomputable def TauCeti.freeCommMonoidCharEquiv {σ : Type u_1} {M : Type u_2} [CommMonoid M] :
(Multiplicative (σ →₀ ℕ) →* M) ≃* (σ → M)

The universal property of the free commutative monoid Multiplicative (σ →₀ ℕ): a homomorphism to a commutative monoid M is the same data as a family σ → M. The forward map reads off the values on the standard generators ofAdd (single i 1); the inverse extends a family to the unique homomorphism through Finsupp.liftAddHom and the ℕ-power homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.freeCommMonoidCharEquiv_apply {σ : Type u_1} {M : Type u_2} [CommMonoid M] (χ : Multiplicative (σ →₀ ℕ) →* M) (i : σ) :
    freeCommMonoidCharEquiv χ i = χ (Multiplicative.ofAdd (Finsupp.single i 1))

    The forward direction of freeCommMonoidCharEquiv evaluates a character on the standard generator indexed by i.

    source
    @[simp]
    theorem TauCeti.freeCommMonoidCharEquiv_symm_apply_ofAdd {σ : Type u_1} {M : Type u_2} [CommMonoid M] (c : σ → M) (m : σ →₀ ℕ) :
    (freeCommMonoidCharEquiv.symm c) (Multiplicative.ofAdd m) = m.prod fun (i : σ) (n : ℕ) => c i ^ n

    The inverse of freeCommMonoidCharEquiv evaluates a finitely supported family of natural exponents as the corresponding product of powers of the chosen coordinates.

    source
    theorem TauCeti.freeCommMonoidCharEquiv_comp {σ : Type u_1} {M : Type u_2} [CommMonoid M] {N : Type u_3} [CommMonoid N] (ψ : M →* N) (χ : Multiplicative (σ →₀ ℕ) →* M) (i : σ) :
    freeCommMonoidCharEquiv (ψ.comp χ) i = ψ (freeCommMonoidCharEquiv χ i)

    Reading off generator values is natural in the target monoid: post-composing with a homomorphism ψ : M →* N commutes with freeCommMonoidCharEquiv.