English
Under suitable hypotheses, the map induced by composing a local hom and a range restriction is bijective.
Русский
При заданных условиях отображение, полученное из композиции локального гомоморфизма и ограничений диапазона, является биекцией.
LaTeX
$$$\\text{Bijective}(g.rangeRestrict \\circ f)$ under appropriate assumptions, e.g., $(g\\circ f) = \\mathrm{algebraMap}_{R,K}$ and IsLocalHom f.$$
Lean4
theorem bijective_rangeRestrict_comp_of_valuationRing [IsDomain R] [ValuationRing R] [IsLocalRing S] [Algebra R K]
[IsFractionRing R K] (f : R →+* S) (g : S →+* K) (h : g.comp f = algebraMap R K) [IsLocalHom f] :
Function.Bijective (g.rangeRestrict.comp f) := by
refine ⟨?_, ?_⟩
· exact .of_comp (f := Subtype.val) (by convert (IsFractionRing.injective R K); rw [← h]; rfl)
· let V : ValuationSubring K := ⟨(algebraMap R K).range, ValuationRing.isInteger_or_isInteger R⟩
suffices LocalSubring.range g ≤ V.toLocalSubring
by
rintro ⟨_, x, rfl⟩
obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩
apply V.isMax_toLocalSubring
have H : (algebraMap R K).range ≤ g.range := fun x ⟨a, ha⟩ ↦ ⟨f a, by simp [← ha, ← h]⟩
refine ⟨H, ⟨?_⟩⟩
rintro ⟨_, a, rfl⟩ (ha : IsUnit (M := g.range) ⟨algebraMap R K a, _⟩)
suffices IsUnit a from this.map (algebraMap R K).rangeRestrict
apply IsUnit.of_map f
apply (IsLocalHom.of_surjective g.rangeRestrict g.rangeRestrict_surjective).1
convert ha
simp [← h]
