Submonoid of pairs with quotient in a submonoid

This file defines the submonoid of pairs whose quotient lies in a submonoid of the localization.

def Submonoid.divPairs {M : Type u_1} {G : Type u_2} [CommMonoid M] [CommGroup G] (f : ⊤.LocalizationMap G) (s : Submonoid G) : Submonoid (M × M)

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.

Equations

• Submonoid.divPairs f s = Submonoid.comap (divMonoidHom.comp ((↑f).prodMap ↑f)) s

def AddSubmonoid.subPairs {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] (f : ⊤.LocalizationMap G) (s : AddSubmonoid G) : AddSubmonoid (M × M)

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.

Equations

• AddSubmonoid.subPairs f s = AddSubmonoid.comap (subAddMonoidHom.comp ((↑f).prodMap ↑f)) s

@[simp]

theorem Submonoid.mem_divPairs {M : Type u_1} {G : Type u_2} [CommMonoid M] [CommGroup G] {f : ⊤.LocalizationMap G} {s : Submonoid G} {x : M × M} : x ∈ divPairs f s ↔ f x.1 / f x.2 ∈ s

@[simp]

theorem AddSubmonoid.mem_subPairs {M : Type u_1} {G : Type u_2} [AddCommMonoid M] [AddCommGroup G] {f : ⊤.LocalizationMap G} {s : AddSubmonoid G} {x : M × M} : x ∈ subPairs f s ↔ f x.1 - f x.2 ∈ s

theorem Submonoid.divPairs_comap {M : Type u_1} {G : Type u_2} {H : Type u_3} [CommMonoid M] [CommGroup G] [CommGroup H] (f : ⊤.LocalizationMap G) (g : ⊤.LocalizationMap H) (s : Submonoid G) : divPairs g (comap (g.mulEquivOfLocalizations f).toMonoidHom s) = divPairs f s

theorem AddSubmonoid.subPairs_comap {M : Type u_1} {G : Type u_2} {H : Type u_3} [AddCommMonoid M] [AddCommGroup G] [AddCommGroup H] (f : ⊤.LocalizationMap G) (g : ⊤.LocalizationMap H) (s : AddSubmonoid G) : subPairs g (comap (g.addEquivOfLocalizations f).toAddMonoidHom s) = subPairs f s