leftDerived_ext — Mathlib

English

LeftDerivedExt asserts the homomorphism-extensionality for left-derived lift: two morphisms γ1, γ2 with equal whiskerLeft by α coincide.

Русский

LeftDerivedExt утверждает эквивалентность между γ1 и γ2, если их обрамление через whiskerLeft по α совпадает.

LaTeX

$$$$ \\forall G, \\gamma_1, \\gamma_2:\\;\\gamma_1 = \\gamma_2 \\;\\text{if } \\mathrm{whiskerLeft}\\; L\\; \\gamma_1 \\;\\circ \\alpha = \\mathrm{whiskerLeft}\\; L\\; \\gamma_2 \\;\\circ \\alpha. $$$$

Lean4

theorem leftDerived_ext (G : D ⥤ H) (γ₁ γ₂ : G ⟶ LF) (hγ : whiskerLeft L γ₁ ≫ α = whiskerLeft L γ₂ ≫ α) : γ₁ = γ₂ :=
  have := IsLeftDerivedFunctor.isRightKanExtension LF α W
  LF.hom_ext_of_isRightKanExtension α γ₁ γ₂ hγ

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