English
A ring homomorphism between local rings is a local ring hom iff a number of equivalent conditions hold (TFAE).
Русский
Гомоморфизм колец, локальных по отношению к каждому другому, локален тогда и только тогда, когда выполняются ряд эквивалентных условий (TFAE).
LaTeX
$$$\text{List.TFAE}\ [\mathrm{IsLocalHom}(f),\; \cdots ]$$$
Lean4
/-- A ring homomorphism between local rings is a local ring hom iff it reflects units,
i.e. any preimage of a unit is still a unit. -/
@[stacks 07BJ]
theorem local_hom_TFAE (f : R →+* S) :
List.TFAE
[IsLocalHom f, f '' (maximalIdeal R).1 ⊆ maximalIdeal S, (maximalIdeal R).map f ≤ maximalIdeal S,
maximalIdeal R ≤ (maximalIdeal S).comap f, (maximalIdeal S).comap f = maximalIdeal R] :=
by
tfae_have 1 → 2
| _, _, ⟨a, ha, rfl⟩ => map_nonunit f a ha
tfae_have 2 → 4 := Set.image_subset_iff.1
tfae_have 3 ↔ 4 := Ideal.map_le_iff_le_comap
tfae_have 4 → 1 := fun h ↦ ⟨fun x => not_imp_not.1 (@h x)⟩
tfae_have 1 → 5
| _ => by ext; exact not_iff_not.2 (isUnit_map_iff f _)
tfae_have 5 → 4 := fun h ↦ le_of_eq h.symm
tfae_finish
