pullback_to_base — Mathlib

English

If f: X → Z is open immersion, and g: Y → Z is open immersion as well, then the projection from the limit of the cospan f, g onto the first component is open immersion.

Русский

Если f: X → Z и g: Y → Z — открытые вложения, то проекция из предельного значения циркульной схемы на первый компонент открыто вложена.

LaTeX

$$$IsOpenImmersion(\limit.\pi(\cospan\ f\ g)\ WalkingCospan.one)$$$

Lean4

instance pullback_to_base [IsOpenImmersion g] : IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one) :=
  by
  rw [← limit.w (cospan f g) WalkingCospan.Hom.inl]
  change IsOpenImmersion (_ ≫ f)
  infer_instance

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