lift_uniq — Mathlib

English

Given two open immersions f and g with a common pullback along a third morphism, the lift is unique: any map l with l ≫ f = g and the same pullback is equal to lift f g H.

Русский

Для двух открытых внедрений f и g с общим пределом по отношению к третьему морфизму существует единственный лифт.

LaTeX

$$$l = lift\ f\ g\ H$ given $l\gg f = g$$$

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 := by
  rw [← cancel_mono f, hl, lift_fac]

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