Finite monoid algebras as Hahn series

7 fully proved

Finite

DefinitionEmbedding of a finite additive monoid algebra into Hahn series#✓fully proved

Embed a finite additive monoid algebra into Hahn series.

noncomputable def ofAddMonoidAlgebra :
    AddMonoidAlgebra R Γ →+* HahnSeries Γ R := by
  let F : Multiplicative Γ →* HahnSeries Γ R :=
    { toFun := fun g => single g.toAdd 1
      map_one' := rfl
      map_mul' := fun g h => by
        change single (g.toAdd + h.toAdd) 1 = single g.toAdd 1 * single h.toAdd 1
        rw [single_mul_single, one_mul] }
  exact (AddMonoidAlgebra.lift R (HahnSeries Γ R) Γ F).toRingHom

Used by 5

Used byCoefficients of the bivariate monoid algebra embedding · Monoid algebra embedding into Hahn series preserves coefficients · Monoid algebra embedding into Hahn series as a ring map · Injectivity of the monoid algebra embedding into Hahn series · Embedding of a bivariate monoid algebra into Hahn series

TheoremMonoid algebra embedding into Hahn series preserves coefficients#✓fully proved

The finite Hahn embedding preserves every coefficient.

@[simp] theorem coeff_ofAddMonoidAlgebra (f : AddMonoidAlgebra R Γ) (g : Γ) :
    (ofAddMonoidAlgebra f).coeff g = f.coeff g

Uses 1 · Used by 3

Statement usesEmbedding of a finite additive monoid algebra into Hahn series

Used byCoefficients of the bivariate monoid algebra embedding · Monoid algebra embedding into Hahn series as a ring map · Injectivity of the monoid algebra embedding into Hahn series

TheoremMonoid algebra embedding into Hahn series as a ring map#✓fully proved

The finite Hahn embedding is Mathlib's ofFinsupp, bundled as a ring homomorphism.

theorem ofAddMonoidAlgebra_apply (f : AddMonoidAlgebra R Γ) :
    ofAddMonoidAlgebra f = ofFinsupp f.coeff

Uses 2

Statement usesEmbedding of a finite additive monoid algebra into Hahn series

Proof usesMonoid algebra embedding into Hahn series preserves coefficients

TheoremInjectivity of the monoid algebra embedding into Hahn series#✓fully proved

The finite Hahn embedding is injective.

theorem ofAddMonoidAlgebra_injective :
    Function.Injective (ofAddMonoidAlgebra : AddMonoidAlgebra R Γ → HahnSeries Γ R)

Uses 2

Statement usesEmbedding of a finite additive monoid algebra into Hahn series

Proof usesMonoid algebra embedding into Hahn series preserves coefficients

Bivariate

DefinitionEmbedding of a bivariate monoid algebra into Hahn series#✓fully proved

Embed a bivariate finite monoid algebra into Hahn series, with the second coordinate outer.

noncomputable def ofBivariateAddMonoidAlgebra :
    AddMonoidAlgebra R (G × H) →+* HahnSeries H (AddMonoidAlgebra R G) :=
  (ofAddMonoidAlgebra (Γ := H) (R := AddMonoidAlgebra R G)).comp
    ((AddMonoidAlgebra.curryRingEquiv (R := R) (M := H) (N := G)).toRingHom.comp
      (AddMonoidAlgebra.mapDomainRingEquiv R
        (AddEquiv.prodComm (M := G) (N := H))).toRingHom)

Uses 1 · Used by 2

Statement usesEmbedding of a finite additive monoid algebra into Hahn series

Used byCoefficients of the bivariate monoid algebra embedding · Injectivity of the bivariate monoid algebra embedding

TheoremCoefficients of the bivariate monoid algebra embedding#✓fully proved

The two coefficient projections of the bivariate embedding recover the original coefficient.

@[simp] theorem coeff_coeff_ofBivariateAddMonoidAlgebra
    (f : AddMonoidAlgebra R (G × H)) (g : G) (h : H) :
    ((ofBivariateAddMonoidAlgebra f).coeff h).coeff g = f.coeff (g, h)

Uses 3 · Used by 1

Statement usesEmbedding of a bivariate monoid algebra into Hahn series

Proof usesMonoid algebra embedding into Hahn series preserves coefficients · Embedding of a finite additive monoid algebra into Hahn series

Used byInjectivity of the bivariate monoid algebra embedding

TheoremInjectivity of the bivariate monoid algebra embedding#✓fully proved

The bivariate finite Hahn embedding is injective.

theorem ofBivariateAddMonoidAlgebra_injective :
    Function.Injective
      (ofBivariateAddMonoidAlgebra :
        AddMonoidAlgebra R (G × H) → HahnSeries H (AddMonoidAlgebra R G))

Uses 2

Statement usesEmbedding of a bivariate monoid algebra into Hahn series

Proof usesCoefficients of the bivariate monoid algebra embedding

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.