liftAux_map' — Mathlib

English

A variaton of hom-ext stability for right Kan-extensions under RanIsSheaf conditions.

Русский

Разновидность устойчивости hom-ext для правого Кан-расширения в условиях RanIsSheaf.

LaTeX

$$$\\text{hom\_ext} : \\dots$$$

Lean4

theorem liftAux_map' {Y Y' : C} (f : G.obj Y ⟶ X) (f' : G.obj Y' ⟶ X) {W : C} (a : W ⟶ Y) (b : W ⟶ Y')
    (w : G.map a ≫ f = G.map b ≫ f') : liftAux hF α s f ≫ F.map a.op = liftAux hF α s f' ≫ F.map b.op :=
  by
  apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable (G.map a ≫ f) S.2)⟩
  rintro ⟨T, g, hg⟩
  dsimp
  have eq₁ := liftAux_map hF α s f (g ≫ a) ⟨_, _, hg⟩ (𝟙 _) (by simp)
  have eq₂ := liftAux_map hF α s f' (g ≫ b) ⟨_, _, hg⟩ (𝟙 _) (by simp [w])
  dsimp at eq₁ eq₂
  simp only [Functor.map_comp, Functor.map_id, Category.id_comp] at eq₁ eq₂
  simp only [Category.assoc, eq₁, eq₂]

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