coconeιApp_eq — Mathlib

English

The cocone component coconeπApp j is equal to the composite F.map α followed by the inverse of isoMap β.

Русский

Компонента конуса coconeιApp равна композиции F.map α затем обратной стороны от isoMap β.

LaTeX

$$h.coconeπApp j = F.map α ≫ (h.isoMap β⟨id⟩)^{-1}$$

Lean4

theorem coconeιApp_eq (j j' : J) (α : j ⟶ j') (β : i₀ ⟶ j') : h.coconeιApp j = F.map α ≫ (h.isoMap β ⟨𝟙 _⟩).inv :=
  by
  obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α
  dsimp [coconeιApp]
  rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id, comp_id, ←
    cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ, ← h₂, F.map_comp, ← F.map_comp β δ, ←
    h₁, F.map_comp, isoMap_inv_hom_id_assoc]

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