surjective_isZariskiLocalAtTarget

English

Surjectivity is a property that is local on the target in the Zariski topology: f is surjective if all restrictions of f to a Zariski open cover of the target are surjective.

Русский

Сюръективность является локальной по Зарисковской топологии на мишени: отображение сюръективно тогда и только тогда, когда его ограничения на открытых Зарисковских подмножествах мишени сюръективны.

LaTeX

$$$IsZariskiLocalAtTarget(\mathrm{Surjective})$$$

Lean4

instance surjective_isZariskiLocalAtTarget : IsZariskiLocalAtTarget @Surjective :=
  by
  have : MorphismProperty.RespectsIso @Surjective := inferInstance
  rw [surjective_eq_topologically] at this ⊢
  refine topologically_isZariskiLocalAtTarget _ (fun _ s _ _ h ↦ h.restrictPreimage s) ?_
  intro α β _ _ f ι U H _ hf x
  obtain ⟨i, hxi⟩ : ∃ i, x ∈ U i := by simpa using congr(x ∈ $H)
  obtain ⟨⟨y, _⟩, hy⟩ := hf i ⟨x, hxi⟩
  exact ⟨y, congr(($hy).1)⟩

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