of_comp_of_isSeparated — Mathlib

English

If a composition is universally closed and the second morphism is separated, then the first morphism is universally closed.

Русский

Если композиция универсально замкнута и второй морфизм отделим, то первый тоже универсально замкнут.

LaTeX

$$[UniversallyClosed(f ≫ g)] ∧ [IsSeparated g] ⇒ UniversallyClosed f$$

Lean4

@[stacks 01W6 "(1)"]
theorem of_comp_of_isSeparated [UniversallyClosed (f ≫ g)] [IsSeparated g] : UniversallyClosed f :=
  by
  rw [← Limits.pullback.lift_snd (𝟙 _) f (Category.id_comp (f ≫ g))]
  infer_instance

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