comp_lift — Mathlib

English

A reassociated form of lift respects composition: (g' ≫ lift f g H') ≈ lift f (g' ≫ g) with a subsidiary equality, capturing functorial behavior of lifts.

Русский

Формулировка с повторной ассоциацией: композиция g' с лифтом сохраняет структуру: g' ≫ lift f g H' ≈ lift f (g' ≫ g).

LaTeX

$$$ g' \gg \text{lift } f g H' = \text{lift } f (g' \gg g) \;\; (\text{with } \text{range subset adjustment}) $$$

Lean4

@[reassoc]
theorem comp_lift {Y' : Scheme} (g' : Y' ⟶ Y) (H : Set.range g.base ⊆ Set.range f.base) :
    g' ≫ lift f g H = lift f (g' ≫ g) (.trans (by simp [Set.range_comp_subset_range]) H) := by simp [← cancel_mono f]

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