pullbackConeOfLeft — Mathlib

English

A variant capturing left pullback conditions in a presheafed space setting for open immersions.

Русский

Вариант условий левого предела в контексте прешефед пространства и открытых вложений.

LaTeX

$$pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict _ ≫ g$$

Lean4

/-- We construct the pullback along an open immersion via restricting along the pullback of the
maps of underlying spaces (which is also an open embedding).
-/
def pullbackConeOfLeft : PullbackCone f g :=
  PullbackCone.mk (pullbackConeOfLeftFst f g) (Y.ofRestrict _) (pullback_cone_of_left_condition f g)

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