English
If for all y ∈ S, g(y) ∈ T and k:LocalizationMap T Q, then k(g x) = k(g y) when f x = f y.
Русский
Если для всех y ∈ S выполняется g(y) ∈ T и k: LocalizationMap T Q, то k(g x) = k(g y) при f x = f y.
LaTeX
$$$\forall x,y\; (f(x)=f(y) \rightarrow k(g(x))=k(g(y)))$ with $g(y)\in T$$$
Lean4
/-- Given `CommMonoid`s `M, P`, Localization maps `f : M →* N, k : P →* Q` for Submonoids
`S, T` respectively, and `g : M →* P` such that `g(S) ⊆ T`, `f x = f y` implies
`k (g x) = k (g y)`. -/
@[to_additive /-- Given `AddCommMonoid`s `M, P`, Localization maps `f : M →+ N, k : P →+ Q` for AddSubmonoids
`S, T` respectively, and `g : M →+ P` such that `g(S) ⊆ T`, `f x = f y`
implies `k (g x) = k (g y)`. -/
]
theorem comp_eq_of_eq {T : Submonoid P} {Q : Type*} [CommMonoid Q] (hg : ∀ y : S, g y ∈ T) (k : LocalizationMap T Q)
{x y} (h : f x = f y) : k (g x) = k (g y) :=
f.eq_of_eq (fun y : S ↦ show IsUnit (k.comp g y) from k.map_units ⟨g y, hg y⟩) h
