iso_symm_apply_aux — Mathlib

English

The inverse image under the iso is a suitable mk representation given by the surjectivity witness.

Русский

Обратное изображение по изоморфизму задаётся представлением mk, полученным из свидетельства сюръекции.

LaTeX

$$$$ (\mathrm{iso}~S~f)^{-1}(m) = \mathrm{LocalizedModule.mk}(a,b) \text{ with } m = (\mathrm{iso}~S~f)(\mathrm{LocalizedModule.mk}(a,b)). $$$$

Lean4

theorem iso_symm_apply_aux (m : M') :
    (iso S f).symm m =
      LocalizedModule.mk (IsLocalizedModule.surj S f m).choose.1 (IsLocalizedModule.surj S f m).choose.2 :=
  by
  apply_fun iso S f using LinearEquiv.injective (iso S f)
  rw [LinearEquiv.apply_symm_apply]
  simp [iso, fromLocalizedModule, Module.End.algebraMap_isUnit_inv_apply_eq_iff', ← Submonoid.smul_def,
    (surj _ _ _).choose_spec]

Похожие утверждения