English
For a local commutative ring R, the following statements are equivalent: (i) R is a HenselianLocalRing; (ii) for every monic f ∈ R[X], every a0 in the residue field with f(a0)=0 and f'(a0)≠0, there exists a ∈ R with f(a)=0 and residue(a)=a0; (iii) for every surjective φ: R → K to a field K and every monic f ∈ R[X], if f evaluated at a0 equals 0 and derivative evaluated at a0 is nonzero, then there exists a ∈ R with f(a)=0 and φ(a)=a0.
Русский
Для локального коммутативного кольца R следующие условия эквивалентны: (i) R гензелевское; (ii) для любого монического многочлена f над R, для каждого a0 в остаточном полеме, если f(a0)=0 и f'(a0)≠0, существует a ∈ R с f(a)=0 и резидуa(a)=a0; (iii) аналогично в терминах отображений R → K, где φ простое и изоморф.
LaTeX
$$$\mathrm{TFAE}\left[ \mathrm{HenselianLocalRing}(R), \forall f \ f.Monic \to \forall a_0, f(a_0)=0 \land f'(a_0) \neq 0 \to \exists a \ (f(a)=0 \land \text{residue}(a)=a_0), \forall \{K\}[Field\ K], \forall \phi: R \to^+ K\ \mathrm{Surjective}(\phi) \to \forall f: R[X], f.Monic \to \forall a_0: K, f.eval_\phi(a_0)=0 \land f.derivative.eval_\phi(a_0) \neq 0 \to \exists a: R, f.IsRoot(a) \land \phi(a)=a_0]$$$
Lean4
theorem TFAE (R : Type u) [CommRing R] [IsLocalRing R] :
TFAE
[HenselianLocalRing R,
∀ f : R[X],
f.Monic →
∀ a₀ : ResidueField R,
aeval a₀ f = 0 → aeval a₀ (derivative f) ≠ 0 → ∃ a : R, f.IsRoot a ∧ residue R a = a₀,
∀ {K : Type u} [Field K],
∀ (φ : R →+* K),
Surjective φ →
∀ f : R[X],
f.Monic → ∀ a₀ : K, f.eval₂ φ a₀ = 0 → f.derivative.eval₂ φ a₀ ≠ 0 → ∃ a : R, f.IsRoot a ∧ φ a = a₀] :=
by
tfae_have 3 → 2
| H => H (residue R) Ideal.Quotient.mk_surjective
tfae_have 2 → 1
| H => by
constructor
intro f hf a₀ h₁ h₂
specialize H f hf (residue R a₀)
have aux := flip mem_nonunits_iff.mp h₂
simp only [aeval_def, ResidueField.algebraMap_eq, eval₂_at_apply, ← Ideal.Quotient.eq_zero_iff_mem,
← IsLocalRing.mem_maximalIdeal] at H h₁ aux
obtain ⟨a, ha₁, ha₂⟩ := H h₁ aux
refine ⟨a, ha₁, ?_⟩
rw [← Ideal.Quotient.eq_zero_iff_mem]
rwa [← sub_eq_zero, ← RingHom.map_sub] at ha₂
tfae_have 1 → 3
| hR, K, _K, φ, hφ, f, hf, a₀, h₁, h₂ => by
obtain ⟨a₀, rfl⟩ := hφ a₀
have H := HenselianLocalRing.is_henselian f hf a₀
simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
obtain ⟨a, ha₁, ha₂⟩ :=
H h₁
(by
contrapose! h₂
rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ, RingHom.mem_ker] at h₂)
refine ⟨a, ha₁, ?_⟩
rwa [φ.map_sub, sub_eq_zero] at ha₂
tfae_finish
