lift_fac — Mathlib

English

If a map l: Y → X satisfies l ≫ f = g under the same data, then l is exactly the lift: l = lift f g H'.

Русский

Если отображение l: Y → X удовлетворяет l ≫ f = g при тех же данных, то l совпадает с лифтом: l = lift f g H'.

LaTeX

$$$ l = \text{lift } f g H' \quad\text{whenever } l \;\text{ satisfies }\; l \gg f = g $$$

Lean4

@[reassoc (attr := simp)]
theorem lift_fac (H' : Set.range g.base ⊆ Set.range f.base) : lift f g H' ≫ f = g :=
  Scheme.Hom.ext' <| LocallyRingedSpace.IsOpenImmersion.lift_fac f.toLRSHom g.toLRSHom H'

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