instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl

English

Various localization maps are compatible with scalar towers, giving preserved structures in the localization chain.

Русский

Различные локализационные отображения совместимы с каскадами скалярных торов, сохраняя структуры локализации.

LaTeX

$$$\text IsLocalization.map_compatibility$$$

Lean4

instance : IsScalarTower Rₚ Sₚ Tₚ := by
  refine ⟨fun a b c ↦ a.ind fun ⟨a₁, a₂⟩ ↦ ?_⟩
  have : a₂.val ≠ 0 := nonZeroDivisors.ne_zero <| Ideal.primeCompl_le_nonZeroDivisors P <| a₂.prop
  rw [← smul_right_inj this, ← _root_.smul_assoc (M := R) (N := Sₚ), ← _root_.smul_assoc (M := R) (α := Sₚ), ←
    _root_.smul_assoc (M := R) (α := Tₚ), Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
    IsLocalization.mk'_mul_cancel_left, algebraMap_smul, algebraMap_smul, _root_.smul_assoc]

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