monoLift_comp — Mathlib

English

For a mono f, monoLift f g hg lifts g along f and yields equality with g after composing with f.

Русский

Для монофункции f модель моноLift восстанавливает g через f и дает равенство после композиции с f.

LaTeX

$$$$ [Mono f] \\Rightarrow (g: T \\to Y) (hg: g \\circ cokernel.π f = 0) \\Rightarrow monoLift f g hg \\circ f = g. $$$$

Lean4

@[reassoc (attr := simp)]
theorem monoLift_comp [Mono f] {T : C} (g : T ⟶ Y) (hg : g ≫ cokernel.π f = 0) : monoLift f g hg ≫ f = g :=
  (monoIsKernelOfCokernel _ (colimit.isColimit _)).fac (KernelFork.ofι _ hg) WalkingParallelPair.zero

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