English
For a commutative monoid M, a localization map f to its Grothendieck group G and a submonoid s of G, define the submonoid divPairs f s of pairs (a,b) ∈ M×M by requiring that f(a)/f(b) ∈ s.
Русский
Для коммутативного моноида M, локализационной карты f в группу Грота и подмножества s в G задаём подмножество пар divPairs f s ⊆ M×M, состоящее из пар (a,b), таких что f(a)/f(b) ∈ s.
LaTeX
$$$\\text{divPairs}(f,s) = \\{(a,b)\\in M\\times M : f(a)/f(b) \\in s\\}$$$
Lean4
/-- Given a commutative monoid `M`, a localization map `f` to its Grothendieck group `G` and
a submonoid `s` of `G`, `s.divPairs f` is the submonoid of pairs `(a, b)`
such that `f a / f b ∈ s`. -/
@[to_additive /-- Given an additive commutative monoid `M`, a localization map `f` to its Grothendieck group `G`
and a submonoid `s` of `G`, `s.subPairs f` is the submonoid of pairs `(a, b)`
such that `f a - f b ∈ s`. -/
]
def divPairs : Submonoid (M × M) :=
s.comap <| divMonoidHom.comp <| .prodMap f f
