English
Symmetric application recovers the original map.
Русский
Симметрическое применение восстанавливает исходное отображение.
LaTeX
$$$ k.symm (f.ofMulEquivOfLocalizations k x) = f x $$$
Lean4
/-- Given an injective `CommMonoid` homomorphism `g : M →* P`, and a submonoid `S ⊆ M`,
the induced monoid homomorphism from the localization of `M` at `S` to the
localization of `P` at `g S`, is injective.
-/
@[to_additive /-- Given an injective `AddCommMonoid` homomorphism `g : M →+ P`, and a
submonoid `S ⊆ M`, the induced monoid homomorphism from the localization of `M` at `S`
to the localization of `P` at `g S`, is injective. -/
]
theorem map_injective_of_injective (hg : Injective g) (k : LocalizationMap (S.map g) Q) :
Injective (map f (apply_coe_mem_map g S) k) := fun z w hizw ↦
by
set i := map f (apply_coe_mem_map g S) k
have ifkg (a : M) : i (f a) = k (g a) := map_eq f (apply_coe_mem_map g S) a
let ⟨z', w', x, hxz, hxw⟩ := surj₂ f z w
have : k (g z') = k (g w') := by rw [← ifkg, ← ifkg, ← hxz, ← hxw, map_mul, map_mul, hizw]
obtain ⟨⟨_, c, hc, rfl⟩, eq⟩ := k.exists_of_eq _ _ this
simp_rw [← map_mul, hg.eq_iff] at eq
rw [← (f.map_units x).mul_left_inj, hxz, hxw, f.eq_iff_exists]
exact ⟨⟨c, hc⟩, eq⟩
