mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight

English

Extensional principle for Grothendieck Hom in the Grothendieckized LocallyDiscrete setting with base and fiber data.

Русский

Экстенсиональное свойство для Grothendieck Hom в обобщённом LocallyDiscrete контексте с данными основания и волокна.

LaTeX

$$$\\forall f,g, base(f)=base(g) \\land fiber(f)=fiber(g) \\Rightarrow f=g$$$

Lean4

@[to_app (attr := reassoc)]
theorem mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight (hf : f₀₂ ≫ f₂₃ = f) :
    (F.mapComp' f₀₂ f₂₃ f).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
      (F.mapComp' f₀₁ f₁₃ f).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫ (α_ _ _ _).inv :=
  by
  rw [F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ f h₀₂ h₁₃ (by cat_disch)]
  simp

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