lift_uniq — Mathlib

English

For any g' : Y' → Y, the lift is compatible with composition: g' ≫ lift f g H' = lift f (g' ≫ g) with a correct adjusted hypothesis.

Русский

Для любого g' : Y' → Y лифт совместим с композиция: g' ≫ lift f g H' = lift f (g' ≫ g) с корректной поправкой гипотезы.

LaTeX

$$$ g' \;\gg\; \text{lift } f g H' = \text{lift } f (g' \gg g) (\text{trans } (\text{by } \text{simp } [\operatorname{Set.range_comp_subset_range]) } H') $$$

Lean4

theorem lift_uniq (H' : Set.range g.base ⊆ Set.range f.base) (l : Y ⟶ X) (hl : l ≫ f = g) : l = lift f g H' :=
  Scheme.Hom.ext' <|
    LocallyRingedSpace.IsOpenImmersion.lift_uniq f.toLRSHom g.toLRSHom H' l.toLRSHom congr(($hl).toLRSHom)

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