locally_StableUnderCompositionWithLocalizationAwayTarget

English

More generally, Locally P is stable under composition with localization-away maps on the target side if P is.

Русский

Более общо, Locally P устойчива к композиции сAway локализацией на целевом конце, если P такова.

LaTeX

$$$\operatorname{StableUnderCompositionWithLocalizationAwayTarget}(\Locally P) \Leftarrow \operatorname{StableUnderCompositionWithLocalizationAwayTarget}(P).$$$

Lean4

/-- If `P` is stable under composition with localization away maps on the right,
then so is `Locally P`. -/
theorem locally_StableUnderCompositionWithLocalizationAwayTarget (hP0 : RespectsIso P)
    (hPa : StableUnderCompositionWithLocalizationAwayTarget P) :
    StableUnderCompositionWithLocalizationAwayTarget (Locally P) :=
  by
  intro R S T _ _ _ _ t _ f hf
  simp only [locally_iff_isLocalization hP0 f] at hf
  obtain ⟨s, hsone, hs⟩ := hf
  refine ⟨algebraMap S T '' s, ?_, ?_⟩
  · rw [← Ideal.map_span, hsone, Ideal.map_top]
  · rintro - ⟨a, ha, rfl⟩
    letI : Algebra (Localization.Away a) (Localization.Away (algebraMap S T a)) :=
      (IsLocalization.Away.map _ _ (algebraMap S T) a).toAlgebra
    have :
      (algebraMap (Localization.Away a) (Localization.Away (algebraMap S T a))).comp
          (algebraMap S (Localization.Away a)) =
        (algebraMap T (Localization.Away (algebraMap S T a))).comp (algebraMap S T) :=
      by simp [algebraMap_toAlgebra, IsLocalization.Away.map]
    rw [← comp_assoc, ← this, comp_assoc]
    haveI : IsScalarTower S (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
      by
      apply IsScalarTower.of_algebraMap_eq
      intro x
      simp [algebraMap_toAlgebra, IsLocalization.Away.map, ← IsScalarTower.algebraMap_apply]
    haveI : IsLocalization.Away (algebraMap S (Localization.Away a) t) (Localization.Away (algebraMap S T a)) :=
      IsLocalization.Away.commutes _ T ((Localization.Away (algebraMap S T a))) a t
    apply hPa _ (algebraMap S (Localization.Away a) t)
    apply hs a ha

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