English
Equality of two expressions for ιMapBifunctorBifunctor₂₃MapObj when the second index is adjusted by hpq.
Русский
Равенство двух выражений для ιMapBifunctorBifunctor₂₃MapObj при скорректированном втором индексе hpq.
LaTeX
$$$$ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i_1 i_2 i_3 j h = (F.obj (X_1 i_1)).map (ιMapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3 i_2 i_3 i_2₃ h₂₃) ≫ ιMapBifunctorMapObj F ρ₂₃.q X_1 (mapBifunctorMapObj G₂₃ ρ₂₃.p X_2 X_3) i_1 i₂₃ j (by rw [← h, ← h₂₃, ← ρ₂₃.hpq]) $$$$
Lean4
/-- The cofan `cofan₃MapBifunctorBifunctor₂₃MapObj` is a colimit, see the induced isomorphism
`mapBifunctorComp₁₂MapObjIso`. -/
noncomputable def isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (j : J) :
IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j) :=
by
let c₂₃ := fun i₂₃ => (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
have h₂₃ : ∀ i₂₃, IsColimit (c₂₃ i₂₃) := fun i₂₃ =>
(((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).isColimitCofanMapObj ρ₂₃.p i₂₃
let c := (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
have hc : IsColimit c :=
(((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).isColimitCofanMapObj ρ₂₃.q j
let c₂₃' := fun (i : ρ₂₃.q ⁻¹' { j }) => (F.obj (X₁ i.1.1)).mapCocone (c₂₃ i.1.2)
have hc₂₃' : ∀ i, IsColimit (c₂₃' i) := fun i => isColimitOfPreserves _ (h₂₃ i.1.2)
let Z := (((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
let p' : I₁ × I₂ × I₃ → I₁ × ρ₂₃.I₂₃ := fun ⟨i₁, i₂, i₃⟩ => ⟨i₁, ρ₂₃.p ⟨i₂, i₃⟩⟩
let e : ∀ (i₁ : I₁) (i₂₃ : ρ₂₃.I₂₃), p' ⁻¹' {(i₁, i₂₃)} ≃ ρ₂₃.p ⁻¹' { i₂₃ } := fun i₁ i₂₃ =>
{ toFun := fun ⟨⟨i₁', i₂, i₃⟩, hi⟩ => ⟨⟨i₂, i₃⟩, by cat_disch⟩
invFun := fun ⟨⟨i₂, i₃⟩, hi⟩ => ⟨⟨i₁, i₂, i₃⟩, by cat_disch⟩
left_inv := fun ⟨⟨i₁', i₂, i₃⟩, hi⟩ =>
by
obtain rfl : i₁ = i₁' := by cat_disch
rfl }
let c₂₃'' : ∀ (i : ρ₂₃.q ⁻¹' { j }), CofanMapObjFun Z p' (i.1.1, i.1.2) := fun ⟨⟨i₁, i₂₃⟩, hi⟩ =>
by
refine
(Cocones.precompose (Iso.hom ?_)).obj
((Cocones.whiskeringEquivalence (Discrete.equivalence (e i₁ i₂₃))).functor.obj (c₂₃' ⟨⟨i₁, i₂₃⟩, hi⟩))
refine Discrete.natIso (fun ⟨⟨i₁', i₂, i₃⟩, hi⟩ => eqToIso ?_)
obtain rfl : i₁' = i₁ := congr_arg _root_.Prod.fst hi
rfl
have h₂₃'' : ∀ i, IsColimit (c₂₃'' i) := fun _ =>
(IsColimit.precomposeHomEquiv _ _).symm (IsColimit.whiskerEquivalenceEquiv _ (hc₂₃' _))
refine
IsColimit.ofIsoColimit
(isColimitCofanMapObjComp Z p' ρ₂₃.q r ρ₂₃.hpq j (fun ⟨i₁, i₂₃⟩ h => c₂₃'' ⟨⟨i₁, i₂₃⟩, h⟩)
(fun ⟨i₁, i₂₃⟩ h => h₂₃'' ⟨⟨i₁, i₂₃⟩, h⟩) c hc)
(Cocones.ext (Iso.refl _) (fun ⟨⟨i₁, i₂, i₃⟩, h⟩ => ?_))
dsimp [Cofan.inj, c₂₃'', Z, p', e]
rw [comp_id, id_comp]
rfl
