coneπApp_eq — Mathlib

English

For any j, j' and morphisms α: j' → i0, β: j' → j, the π-app is given by the inverse of isoMap composed with F.map β.

Русский

Для любых объектов и морфизмов π-применение задаётся через обратную сторону изоморфизма и отображение F.map.

LaTeX

$$$h.coneπApp j = (h.isoMap(\alpha)(⟨id⟩))^{-1} \circ F.map(\beta)$$$

Lean4

theorem coneπApp_eq (j j' : J) (α : j' ⟶ i₀) (β : j' ⟶ j) : h.coneπApp j = (h.isoMap α ⟨𝟙 _⟩).inv ≫ F.map β :=
  by
  obtain ⟨s, γ, δ, h₁, h₂⟩ := IsCofiltered.bowtie (IsCofiltered.minToRight i₀ j) β (IsCofiltered.minToLeft i₀ j) α
  dsimp [coneπApp]
  rw [← cancel_epi ((h.isoMap α ⟨𝟙 _⟩).hom), isoMap_hom, isoMap_hom_inv_id_assoc, ← cancel_epi (h.isoMap δ ⟨α⟩).hom,
    isoMap_hom, ← F.map_comp δ β, ← h₁, F.map_comp, ← F.map_comp_assoc, ← h₂, F.map_comp_assoc, isoMap_hom_inv_id_assoc]

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