mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv

English

Symmetric extensionality in Grothendieck Hom with base equality and fiber coherence under conjugation.

Русский

Симметричная экстенсиональность для Grothendieck Hom: основание совпадает и волокна согласованы через сопряжение.

LaTeX

$$$f.base = g.base \\land f.fiber = g.fiber \\Rightarrow f=g$$$

Lean4

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

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