English
The map mapPiEvalRingHom is a bijection between the corresponding localizations.
Русский
Отображение mapPiEvalRingHom является биекцией между соответствующими локализациями.
LaTeX
$$$\\mathrm{mapPiEvalRingHom}\\;\\text{is bijective}$$$
Lean4
theorem mapPiEvalRingHom_bijective : Bijective (mapPiEvalRingHom S) :=
by
let T := S.comap (Pi.evalRingHom R i)
classical
refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
· obtain ⟨r₁, s₁, rfl⟩ := mk'_surjective T x₁
obtain ⟨r₂, s₂, rfl⟩ := mk'_surjective T x₂
simp_rw [map_mk'] at eq
rw [IsLocalization.eq] at eq ⊢
obtain ⟨s, hs⟩ := eq
refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
obtain rfl | ne := eq_or_ne j i
· simpa using hs
· simp [update_of_ne ne]
· obtain ⟨r, s, rfl⟩ := mk'_surjective S x
exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, by simp [map_mk']⟩
