English
A second form of compatibility-preserving for Over.map f with J, ensuring coherent gluing along pullbacks.
Русский
Второй формальный вид совместимости Over.map f с J, обеспечивающий когерентную склейку вдоль вытягиваний назад.
LaTeX
$$$\\forall f:\\,X\\to Y\\; (\\text{CompatiblePreserving}\\ (J.\\mathrm{over}\\,Y)\\ (\\mathrm{Over.map}\\ f))$$$
Lean4
theorem over_map_compatiblePreserving {X Y : C} (f : X ⟶ Y) : CompatiblePreserving (J.over Y) (Over.map f) where
compatible
{F Z _ x hx Y₁ Y₂ W f₁ f₂ g₁ g₂ hg₁ hg₂
h} := by
let W' : Over X := Over.mk (f₁.left ≫ Y₁.hom)
let g₁' : W' ⟶ Y₁ := Over.homMk f₁.left
let g₂' : W' ⟶ Y₂ := Over.homMk f₂.left (by simpa using (Over.forget _).congr_map h.symm =≫ Z.hom)
let e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl _) (by simpa [W'] using (Over.w f₁).symm)
convert congr_arg (F.val.map e.inv.op) (hx g₁' g₂' hg₁ hg₂ (by ext; exact (Over.forget _).congr_map h)) using 1
all_goals
dsimp [e, W', g₁', g₂']
rw [← FunctorToTypes.map_comp_apply]
apply congr_fun
congr 1
rw [← op_comp]
congr 1
ext
simp
