Localizations of commutative monoids #

Localizing a commutative ring at one of its submonoids does not rely on the ring's addition, so we can generalize localizations to commutative monoids.

We characterize the localization of a commutative monoid M at a submonoid S up to isomorphism; that is, a commutative monoid N is the localization of M at S iff we can find a monoid homomorphism f : M →* N→* N satisfying 3 properties:

For all y ∈ S∈ S, f y is a unit;
For all z : N, there exists (x, y) : M × S× S such that z * f y = f x;
For all x, y : M, f x = f y iff there exists c ∈ S∈ S such that x * c = y * c.

Given such a localization map f : M →* N→* N, we can define the surjection LocalizationMap.mk' sending (x, y) : M × S× S to f x * (f y)⁻¹⁻¹, and LocalizationMap.lift, the homomorphism from N induced by a homomorphism from M which maps elements of S to invertible elements of the codomain. Similarly, given commutative monoids P, Q, a submonoid T of P and a localization map for T from P to Q, then a homomorphism g : M →* P→* P such that g(S) ⊆ T⊆ T induces a homomorphism of localizations, LocalizationMap.map, from N to Q. We treat the special case of localizing away from an element in the sections AwayMap and Away.

We also define the quotient of M × S× S by the unique congruence relation (equivalence relation preserving a binary operation) r such that for any other congruence relation s on M × S× S satisfying '∀ y ∈ S∀ y ∈ S∈ S, (1, 1) ∼ (y, y)∼ (y, y) under s', we have that (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by s whenever (x₁, y₁) ∼ (x₂, y₂)∼ (x₂, y₂) by r. We show this relation is equivalent to the standard localization relation. This defines the localization as a quotient type, Localization, but the majority of subsequent lemmas in the file are given in terms of localizations up to isomorphism, using maps which satisfy the characteristic predicate.

Implementation notes #

In maths it is natural to reason up to isomorphism, but in Lean we cannot naturally rewrite one structure with an isomorphic one; one way around this is to isolate a predicate characterizing a structure up to isomorphism, and reason about things that satisfy the predicate.

The infimum form of the localization congruence relation is chosen as 'canonical' here, since it shortens some proofs.

To apply a localization map f as a function, we use f.toMap, as coercions don't work well for this structure.

To reason about the localization as a quotient type, use mk_eq_monoidOf_mk' and associated lemmas. These show the quotient map mk : M → S → Localization S→ S → Localization S→ Localization S equals the surjection LocalizationMap.mk' induced by the map monoid_of : localization_map S (localization S) (where of establishes the localization as a quotient type satisfies the characteristic predicate). The lemma mk_eq_monoidOf_mk' hence gives you access to the results in the rest of the file, which are about the LocalizationMap.mk' induced by any localization map.

Tags #

localization, monoid localization, quotient monoid, congruence relation, characteristic predicate, commutative monoid