locally_isStableUnderBaseChange — Mathlib

English

If P is stable under base change, then Locally P is stable under base change as well.

Русский

Если P устойчива к изменению основания, то Locally P устойчива к изменению основания тоже.

LaTeX

$$$\operatorname{IsStableUnderBaseChange}(P) \Rightarrow \operatorname{IsStableUnderBaseChange}(\Locally P).$$$

Lean4

/-- If `P` is stable under base change, then so is `Locally P`. -/
theorem locally_isStableUnderBaseChange (hPi : RespectsIso P) (hPb : IsStableUnderBaseChange P) :
    IsStableUnderBaseChange (Locally P) :=
  by
  apply IsStableUnderBaseChange.mk (locally_respectsIso hPi)
  introv hf
  obtain ⟨s, hsone, hs⟩ := hf
  rw [locally_iff_exists hPi]
  letI (a : s) : Algebra (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) :=
    (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toRingHom.toAlgebra
  letI (a : s) : Algebra T (S ⊗[R] Localization.Away a.val) :=
    ((algebraMap _ (S ⊗[R] Localization.Away a.val)).comp (algebraMap T (S ⊗[R] T))).toAlgebra
  haveI (a : s) : IsScalarTower T (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) := IsScalarTower.of_algebraMap_eq' rfl
  haveI (a : s) : IsScalarTower T (Localization.Away a.val) (S ⊗[R] Localization.Away a.val) :=
    IsScalarTower.of_algebraMap_eq' rfl
  haveI (a : s) : IsScalarTower S (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) :=
    IsScalarTower.of_algebraMap_eq <| by
      intro x
      simp [RingHom.algebraMap_toAlgebra]
  haveI (a : s) : Algebra.IsPushout T (Localization.Away a.val) (S ⊗[R] T) (S ⊗[R] Localization.Away a.val) :=
    by
    rw [← Algebra.IsPushout.comp_iff R _ S]
    infer_instance
  refine
    ⟨s, fun a ↦ Algebra.TensorProduct.includeRight a.val, ?_, fun a ↦ (S ⊗[R] Localization.Away a.val), inferInstance,
      inferInstance, ?_, ?_⟩
  · rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
  · intro a
    convert_to
      IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] T) (Submonoid.powers a.val)) (S ⊗[R] Localization.Away a.val)
    · simp only [Algebra.TensorProduct.includeRight_apply, Algebra.algebraMapSubmonoid, Submonoid.map_powers]
      rfl
    · rw [← isLocalizedModule_iff_isLocalization,
        isLocalizedModule_iff_isBaseChange (S := Submonoid.powers a.val) (A := Localization.Away a.val)]
      exact Algebra.IsPushout.out
  · intro a
    rw [← IsScalarTower.algebraMap_eq]
    apply hPb R (Localization.Away a.val)
    rw [IsScalarTower.algebraMap_eq R T]
    exact hs a a.property

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