English
Given a sieve S on X and a cocone s over diagram S.arrows, the Yoneda family from that cocone is compatible.
Русский
Для опер—сита S на X и кокона s над диаграммой S.arrows семейство Yoneda совместимо.
LaTeX
$$FamilyOfElements.Compatible \;\big|\; yonedaFamilyOfElements_fromCocone S.arrows s$$
Lean4
theorem yonedaFamily_fromCocone_compatible (S : Sieve X) (s : Cocone (diagram S.arrows)) :
FamilyOfElements.Compatible <| yonedaFamilyOfElements_fromCocone S.arrows s :=
by
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ hf₁ hf₂ hgf
have Hs := s.ι.naturality
simp only [Functor.id_obj, yoneda_obj_obj, Opposite.unop_op, yoneda_obj_map, Quiver.Hom.unop_op]
dsimp [yonedaFamilyOfElements_fromCocone]
have hgf₁ : S.arrows (g₁ ≫ f₁) := by exact Sieve.downward_closed S hf₁ g₁
have hgf₂ : S.arrows (g₂ ≫ f₂) := by exact Sieve.downward_closed S hf₂ g₂
let F : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk (g₂ ≫ f₂) : Over X) := Over.homMk (𝟙 Z)
let F₁ : (Over.mk (g₁ ≫ f₁) : Over X) ⟶ (Over.mk f₁ : Over X) := Over.homMk g₁
let F₂ : (Over.mk (g₂ ≫ f₂) : Over X) ⟶ (Over.mk f₂ : Over X) := Over.homMk g₂
have hF := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ F
have hF₁ := @Hs ⟨Over.mk (g₁ ≫ f₁), hgf₁⟩ ⟨Over.mk f₁, hf₁⟩ F₁
have hF₂ := @Hs ⟨Over.mk (g₂ ≫ f₂), hgf₂⟩ ⟨Over.mk f₂, hf₂⟩ F₂
cat_disch
