English
Let R be a commutative ring with A → B and I an ideal of B. If the I-adic infimum ⨅ i, I^i equals ⊥, and g1,g2: A → B satisfy that for all x, the images g1(x) and g2(x) are congruent modulo I, then g1 = g2.
Русский
Пусть R — коммутативное кольцо, A → B гомоморфизм, I — идеал B. Если пересечение I^i по i равно ⊥, и для всех x ∈ A выполняется равенство образов g1(x) и g2(x) в факторе B/I, то g1 = g2.
LaTeX
$$$\forall I:\,\text{Ideal}(B),\ g_1,g_2:\, A \to_R B,\ (\forall x, \mkern1mu \operatorname{Quotient.mk} I (g_1 x) = \operatorname{Quotient.mk} I (g_2 x)) \Rightarrow g_1 = g_2$ при условии $\bigl( \bigwedge_i I^i \bigr) = \{0\}$$$
Lean4
theorem ext_of_iInf [FormallyUnramified R A] (hI : ⨅ i, I ^ i = ⊥) {g₁ g₂ : A →ₐ[R] B}
(H : ∀ x, Ideal.Quotient.mk I (g₁ x) = Ideal.Quotient.mk I (g₂ x)) : g₁ = g₂ :=
by
have (i : ℕ) : (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂ :=
by
by_cases hi : i = 0
· ext x
have : Subsingleton (B ⧸ I ^ i) := by
rw [hi, pow_zero, Ideal.one_eq_top]
infer_instance
exact Subsingleton.elim _ _
apply ext (I.map (algebraMap _ _)) ⟨i, by simp [← Ideal.map_pow]⟩
intro x
dsimp
rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective', sup_eq_left.mpr, ←
Ideal.Quotient.eq]
· exact H _
· simpa using Ideal.pow_le_self hi
· exact Ideal.Quotient.mk_surjective
ext x
rw [← sub_eq_zero, ← Ideal.mem_bot, ← hI, Ideal.mem_iInf]
intro i
rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero]
exact DFunLike.congr_fun (this i) x
