ext' — Mathlib

English

Ext' provides the extensional equality criterion for extensions in FormallyUnramified, equating two AlgHoms when their images under a fixed f agree on all x.

Русский

Ext' задаёт критерий равенства расширений через алгебро-гомоморфизмы: g1=g2 если их образы совпадают на всех x.

LaTeX

$$$[FormallyUnramified R A] \\Rightarrow \\text{ext'}\\ (f)\\ (hf)\\ (g_1,g_2) \\Rightarrow g_1=g_2.$$$

Lean4

theorem ext' [FormallyUnramified R A] {C : Type*} [Ring C] (f : B →+* C) (hf : IsNilpotent <| RingHom.ker f)
    (g₁ g₂ : A →ₐ[R] B) (h : ∀ x, f (g₁ x) = f (g₂ x)) : g₁ = g₂ :=
  FormallyUnramified.lift_unique_of_ringHom f hf g₁ g₂ (RingHom.ext h)

Похожие утверждения