of_comp_surjective — Mathlib

English

If f: X → Y and g: Y → Z are schemes and the composition f ≫ g is universally closed, with f surjective, then g is universally closed.

Русский

Пусть f: X → Y и g: Y → Z — морфизмы, композиция f ≫ g universally_closed; если f сюръективен, то g тоже universally_closed.

LaTeX

$$$\\text{UniversallyClosed}(f \\circ g) \\land \\text{Surjective}(f) \\Rightarrow \\text{UniversallyClosed}(g)$$$

Lean4

theorem of_comp_surjective {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [UniversallyClosed (f ≫ g)] [Surjective f] :
    UniversallyClosed g := by
  constructor
  intro X' Y' i₁ i₂ f' H
  have := UniversallyClosed.out _ _ _ ((IsPullback.of_hasPullback i₁ f).paste_horiz H)
  exact
    IsClosedMap.of_comp_surjective (MorphismProperty.pullback_fst (P := @Surjective) _ _ ‹_›).1
      (Scheme.Hom.continuous _) this

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