instUniversallyClosedOfIsClosedImmersion

English

UniversallyClosed is stable under base change: if f is universally closed, then its pullback along any map is universally closed.

Русский

UniversallyClosed устойчиво к базовым изменениям: если f универсально замкнуто, то его базовое изменение по любому отображению тоже универсально замкнуто.

LaTeX

$$$\\text{IsStableUnderBaseChange} \\; (\\mathrm{UniversallyClosed})$$$

Lean4

instance (priority := 900) [IsClosedImmersion f] : UniversallyClosed f :=
  by
  rw [universallyClosed_eq]
  intro X' Y' i₁ i₂ f' hf
  have hf' : IsClosedImmersion f' := MorphismProperty.of_isPullback hf.flip inferInstance
  exact hf'.base_closed.isClosedMap

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