English
The exactness property of δ with respect to the map from Extension.H1Cotangent to H1Cotangent via base change holds.
Русский
Точность δ сохраняется под отображением базового переноса, в точном соотношении между H1Cotangent и базовым изменением.
LaTeX
$$$\text{Exact}( (\mathrm{Extension.H1Cotangent.map} (Q.ofComp P).toExtensionHom) , \; δ Q P)$$$
Lean4
theorem eventually_mem_nhds {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) {U : Set K⸨X⸩} (hU : U ∈ 𝓝 (Cauchy.limit hℱ)) :
∀ᶠ f in ℱ, f ∈ U := by
obtain ⟨γ, hU₁⟩ := Valued.mem_nhds.mp hU
suffices ∀ᶠ f in ℱ, f ∈ {y : K⸨X⸩ | Valued.v (y - limit hℱ) < ↑γ} by apply this.mono fun _ hf ↦ hU₁ hf
set D := -(WithZero.log γ - 1) with hD₀
have hD : WithZero.exp (-D) < γ :=
by
rw [← WithZero.lt_log_iff_exp_lt (by simp), hD₀]
simp
apply coeff_eventually_equal (D := D) hℱ |>.mono
intro _ hf
apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD
intro n hn
rw [HahnSeries.coeff_sub, sub_eq_zero, eq_comm]
exact hf _ hn
