iff_map_piEvalRingHom — Mathlib

English

Equivalence between IsLocalization for M in S' and the pi-map of localized M.

Русский

Эквивалентность между локализацией для M в S' и локализованной проекции M через pi-map.

LaTeX

$$$\\text{IsLocalization } M S' \\iff \\text{IsLocalization}(\\pi\\text{univ}_M M) S'$$$

Lean4

theorem iff_map_piEvalRingHom [Finite ι] :
    IsLocalization M S' ↔ IsLocalization (.pi .univ fun i ↦ M.map (Pi.evalRingHom R i)) S' :=
  iff_of_le_of_exists_dvd M _ (fun m hm i _ ↦ ⟨m, hm, rfl⟩) fun n hn ↦
    by
    choose m mem eq using hn
    have := Fintype.ofFinite ι
    refine ⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩
    rw [Fintype.prod_apply]
    exact (eq i ⟨⟩).symm.dvd.trans (Finset.dvd_prod_of_mem _ <| Finset.mem_univ _)

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