English
Two ideals are equal if and only if every element is either in both or in neither.
Русский
Идеалы равны тогда и только тогда, когда для каждого элемента выполняется: он принадлежит обоим или ни одному.
LaTeX
$$Ideal.ext (I J) (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J$$
Lean4
theorem map_eq_top_iff [IsNoetherianRing R] {M : Submodule R (maximalIdeal R)} :
M.map (maximalIdeal R).toCotangent = ⊤ ↔ M = ⊤ :=
by
refine ⟨fun H ↦ eq_top_iff.mpr ?_, by rintro rfl; simp [Ideal.toCotangent_range]⟩
refine (Submodule.map_le_map_iff_of_injective (Submodule.injective_subtype _) _ _).mp ?_
rw [Submodule.map_top, Submodule.range_subtype]
apply
Submodule.le_of_le_smul_of_le_jacobson_bot (IsNoetherian.noetherian _)
(IsLocalRing.jacobson_eq_maximalIdeal _ bot_ne_top).ge
rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup, ← Submodule.comap_map_eq, H,
Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
