w' — Mathlib · SciLib

English

If F is faithful, two morphisms a,b : c ⟶ hf.pullback g are equal whenever F.map a ≫ hf.fst g = F.map b ≫ hf.fst g and a ≫ hf.snd g = b ≫ hf.snd g.

Русский

Если F верно сохраняет различия, то два морфизма a,b : c ⟶ hf.pullback g равны, когда выполняются условия на их композиции с hf.fst g и hf.snd g.

LaTeX

$$$\\text{HomExt: } (F.map a \\gg hf.fst g = F.map b \\gg hf.fst g) \\land (a \\gg hf.snd g = b \\gg hf.snd g) \\Rightarrow a = b$$$

Lean4

@[reassoc]
theorem w' {X Y Z : C} {f : X ⟶ Z} (hf : F.relativelyRepresentable (F.map f)) (g : Y ⟶ Z) [Full F] [Faithful F] :
    hf.fst' (F.map g) ≫ f = hf.snd (F.map g) ≫ g :=
  F.map_injective <| by simp [(hf.w (F.map g))]

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