English
Congruence lemma: if two isColimit proofs hc1 hc2 are equal, then the corresponding isColimit produced by isColimitOfPreserves₂ are equal.
Русский
Лемма конгруэнции: если два доказательства isColimit hc1 hc2 равны, то соответствующий isColimit, полученный через isColimitOfPreserves₂, равен им.
LaTeX
$$$\\forall hc1 hc1' hc2 hc2' \\; Eq\\; hc1 hc1' \\rightarrow Eq\\; hc2 hc2' \\rightarrow \\; Eq\\; (isColimitOfPreserves₂ G hc1 hc2) (isColimitOfPreserves₂ G hc1' hc2')$$$
Lean4
/-- If a bifunctor preserves separately colimits of `K₁` in the first variable and colimits
of `K₂` in the second variable, then it preserves colimit of the pair `K₁, K₂`. -/
instance of_preservesColimits_in_each_variable [∀ x : C₂, PreservesColimit K₁ (G.flip.obj x)]
[∀ x : C₁, PreservesColimit K₂ (G.obj x)] : PreservesColimit₂ K₁ K₂ G where
nonempty_isColimit_mapCocone₂ {c₁} hc₁ {c₂}
hc₂ :=
let Q₀ : DiagramOfCocones (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G) :=
{ obj j₁ := G.obj (K₁.obj j₁) |>.mapCocone c₂
map f := { hom := G.map (K₁.map f) |>.app c₂.pt } }
let P : ∀ j₁, IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves _ hc₂
let E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun _ ↦ Iso.refl _)
let E₁ :
(Cocones.precompose E₀.hom).obj (coconeOfCoconeUncurry P <| G.mapCocone₂ c₁ c₂) ≅
(G.flip.obj c₂.pt).mapCocone c₁ :=
Cocones.ext (Iso.refl _)
(fun j₁ => by
dsimp [E₀, Q₀]
simp only [id_comp, comp_id]
let s : Cocone (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G |>.obj j₁) := ?_
change (P j₁).desc s = _
symm
apply (P j₁).hom_ext
intro j₂
haveI := (P j₁).fac s j₂
simp only [Functor.mapCocone_pt, Functor.const_obj_obj, Functor.mapCocone_ι_app, Q₀, s] at this
simp only [Functor.mapCocone_pt, Functor.const_obj_obj, Functor.mapCocone_ι_app, NatTrans.naturality, this,
Q₀, s])
⟨IsColimit.ofCoconeUncurry P <|
IsColimit.precomposeHomEquiv E₀ _ <| IsColimit.ofIsoColimit (isColimitOfPreserves _ hc₁) E₁.symm⟩
