isPullback_lift_id — Mathlib

English

Let f: X → Y and g: U → Y with [IsOpenImmersion g], and let H be the range inclusion condition. Then the square formed by IsOpenImmersion.lift g f H, the identity on Y, g and f is a pullback square.

Русский

Пусть f: X → Y и g: U → Y с условием открытого вложения, и H — включение образов. Тогда квадрат, образованный IsOpenImmersion.lift g f H, идентитетом на Y, g и f, является тождественным диаграммой-квадратом (pullback).

LaTeX

$$$IsPullback\\left(IsOpenImmersion.lift\\ g\\ f\\ H\\right)\\left(\\,Id\\,\\right)\\ g\\ f$$$

Lean4

theorem isPullback_lift_id {X U Y : Scheme.{u}} (f : X ⟶ Y) (g : U ⟶ Y) [IsOpenImmersion g]
    (H : Set.range f.base ⊆ Set.range g.base) : IsPullback (IsOpenImmersion.lift g f H) (𝟙 _) g f :=
  by
  convert IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)
  · exact (Category.comp_id _).symm
  · simp

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