mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom

English

Alternative extensionality lemma in Grothendieck setting for Hom in the LocallyDiscrete context.

Русский

Альтернативная лемма экстенсиональности для Hom в контексте LocallyDiscrete Гротендикa.

LaTeX

$$$f = g \\Rightarrow base(f)=base(g)$ and other fiber relations$$$

Lean4

@[to_app (attr := reassoc)]
theorem mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom (hf : f₀₁ ≫ f₁₃ = f) :
    (F.mapComp' f₀₁ f₁₃ f).inv ≫ (F.mapComp' f₀₂ f₂₃ f).hom =
      F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫ (α_ _ _ _).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ :=
  by
  rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f hf).hom, Iso.hom_inv_id_assoc,
    F.mapComp'₀₁₃_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf]
  simp

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