Localizations of monoid algebras away from a monomial

Let f : M →* N be an injective homomorphism of commutative monoids and let x : M be an element whose image is a unit of N. When every element of N becomes an element of the image of f after multiplying by a sufficiently large power of f x, the induced map of monoid algebras R[M] → R[N] is the localization away from the monomial of x.

This is the algebraic form of an open immersion of affine monoid schemes: in toric geometry, the coordinate ring of the affine chart of a face σ ∩ m^⊥ of a cone σ is obtained from the coordinate ring of σ by inverting the monomial of m.

Main declarations

• TauCeti.MonoidAlgebra.isLocalization_away_mapDomainRingHom: the induced map of monoid algebras is a localization away from the monomial of x.

References

• W. Fulton, Introduction to Toric Varieties, §§1.2–1.3.
• D. Cox, J. Little and H. Schenck, Toric Varieties, §1.3.

theorem TauCeti.MonoidAlgebra.isLocalization_away_mapDomainRingHom (R : Type u_1) [CommSemiring R] {M : Type u_2} {N : Type u_3} [CommMonoid M] [CommMonoid N] (f : M →* N) (hf : Function.Injective ⇑f) (x : M) (hx : IsUnit (f x)) (hsurj : ∀ (y : N), ∃ (n : ℕ), y * f x ^ n ∈ Set.range ⇑f) : IsLocalization.Away (MonoidAlgebra.single x 1) (MonoidAlgebra R N)

Let f : M →* N be an injective homomorphism of commutative monoids, and let x : M map to a unit of N such that every element of N lands in the image of f after multiplication by a power of f x. Then the induced map of monoid algebras R[M] → R[N] is the localization away from the monomial of x.