English
The lift composed with the inclusion recovers the original j: the map f.lift hg composed with f is j.
Русский
Составление подъема с включением восстанавливает исходное j: (f.lift hg) ∘ f = j.
LaTeX
$$$ (f.lift hg) \circ f = j $$$
Lean4
/-- Given a Localization map `f : M →* N` for a Submonoid `S ⊆ M`, if a `CommMonoid` map
`g : M →* P` induces a map `f.lift hg : N →* P` then for all `z : N, v w : P`, we have
`f.lift hg z * w = v ↔ g x * w = g y * v`, where `x : M, y ∈ S` are such that
`z * f y = f x`. -/
@[to_additive /-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M`, if an `AddCommMonoid` map
`g : M →+ P` induces a map `f.lift hg : N →+ P` then for all
`z : N, v w : P`, we have `f.lift hg z + w = v ↔ g x + w = g y + v`, where `x : M, y ∈ S` are such
that `z + f y = f x`. -/
]
theorem lift_spec_mul (z w v) : f.lift hg z * w = v ↔ g (f.sec z).1 * w = g (f.sec z).2 * v := by
rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]
