locally_ofLocalizationSpanTarget — Mathlib

English

Locally P is local on the target; i.e., the property Locally P satisfies the localization-span target condition.

Русский

Locally P локально по целевому модулю; свойство Locally P удовлетворяет условию локализации на целевом модуле.

LaTeX

$$$\OfLocalizationSpanTarget(\Locally P).$$$

Lean4

/-- `Locally P` is local on the target. -/
theorem locally_ofLocalizationSpanTarget (hP : RespectsIso P) : OfLocalizationSpanTarget (Locally P) :=
  by
  intro R S _ _ f s hsone hs
  choose t htone ht using hs
  rw [locally_iff_exists hP]
  refine
    ⟨(a : s) × t a, IsLocalization.Away.mulNumerator s t,
      IsLocalization.Away.span_range_mulNumerator_eq_top hsone htone, fun ⟨a, b⟩ ↦ Localization.Away b.val,
      inferInstance, inferInstance, fun ⟨a, b⟩ ↦ ?_, ?_⟩
  · haveI :
      IsLocalization.Away ((algebraMap S (Localization.Away a.val)) (IsLocalization.Away.sec a.val b.val).1)
        (Localization.Away b.val) :=
      by
      apply IsLocalization.Away.of_associated (r := b.val)
      rw [← IsLocalization.Away.sec_spec]
      apply associated_mul_unit_right
      rw [map_pow _ _]
      exact IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)
    apply IsLocalization.Away.mul' (Localization.Away a.val) (Localization.Away b.val)
  · intro ⟨a, b⟩
    rw [IsScalarTower.algebraMap_eq S (Localization.Away a.val) (Localization.Away b.val)]
    apply ht _ _ b.property

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