surjectiveOnStalks_iff_of_isLocalHom

English

If f is surjective as a map of rings, then f is surjective on stalks.

Русский

Если отображение колец f сюръективно как функция, то оно сюръективно на стэках.

LaTeX

$$$\\text{surjective on stalks} \\Rightarrow f.SurjectiveOnStalks$$$

Lean4

theorem surjectiveOnStalks_iff_of_isLocalHom [IsLocalRing S] [IsLocalHom f] :
    f.SurjectiveOnStalks ↔ Function.Surjective f :=
  by
  refine ⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩
  obtain ⟨y, r, c, hc, hr, e⟩ := (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x
  simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr
  refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩
  apply hr.mul_right_injective
  apply hc.mul_right_injective
  simp only [← map_mul, ← mul_assoc, IsUnit.mul_val_inv, one_mul, e]

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