mapComp'₀₁₃_hom — Mathlib

English

Final statement of extensionality for Grothendieck Hom with base and fiber data equivalence.

Русский

Финальное утверждение экстенсиональности для Grothendieck Hom с данными основания и волокна.

LaTeX

$$$f = g \\text{ if base and fiber data coincide}$$$

Lean4

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

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