respectsIso — Mathlib

English

If a property P holds for localization away and f is bijective, then P holds for f.

Русский

Если свойство P сохраняется для локализации away и отображение f биективно, то P выполняется для f.

LaTeX

$$$\\text{HoldsForLocalizationAway }P \\to \\text{Bijective }f \\Rightarrow P(f)$$$

Lean4

theorem respectsIso (hP : LocalizationAwayPreserves P) : RespectsIso P
    where
  left {R S T} _ _ _ f e
    hf := by
    letI := e.toRingHom.toAlgebra
    have : IsLocalization.Away (1 : R) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one (Equiv.refl _).bijective
    have : IsLocalization.Away (f 1) T := IsLocalization.away_of_isUnit_of_bijective _ (by simp) e.bijective
    convert hP f 1 R T hf
    trans (IsLocalization.Away.map R T f 1).comp (algebraMap R R)
    · rw [IsLocalization.Away.map, IsLocalization.map_comp]; rfl
    · rfl
  right {R S T} _ _ _ f e
    hf := by
    letI := e.symm.toRingHom.toAlgebra
    have : IsLocalization.Away (1 : S) R := IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.symm.bijective
    have : IsLocalization.Away (f 1) T :=
      IsLocalization.away_of_isUnit_of_bijective _ (by simp) (Equiv.refl _).bijective
    convert hP f 1 R T hf
    have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f := IsLocalization.map_comp ..
    conv_lhs => rw [← this, RingHom.comp_assoc]
    simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, RingHomCompTriple.comp_eq]

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