English
Let R be a commutative ring and I an ideal with I ≤ Jacobson(⊥). Then the canonical quotient map π: R → R/I is a local homomorphism.
Русский
Пусть R — коммутативное кольцо, I — идеал с условием I ⊆ Jacobson(⊥). Тогда каноническое отображение π: R → R/I является локальным гомоморфизмом.
LaTeX
$$$I \le \operatorname{Jac}(R, \bot) \;\Rightarrow\; \text{IsLocalHom}(\operatorname{Quotient.mk} I).$$$
Lean4
theorem isLocalHom_of_le_jacobson_bot {R : Type*} [CommRing R] (I : Ideal R) (h : I ≤ Ideal.jacobson ⊥) :
IsLocalHom (Ideal.Quotient.mk I) := by
constructor
intro a h
have : IsUnit (Ideal.Quotient.mk (Ideal.jacobson ⊥) a) :=
by
rw [isUnit_iff_exists_inv] at *
obtain ⟨b, hb⟩ := h
obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
use Ideal.Quotient.mk _ b
rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
exact h hb
obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
Ideal.mem_jacobson_bot] at h1 h2
specialize h1 1
have h1 : IsUnit a ∧ IsUnit y := by simpa using h1
exact h1.1
