English
For x : S.functor ⟶ P and g : yoneda.obj X ⟶ P, one has S.functorInclusion ≫ g = x if and only if (natTransEquivCompatibleFamily x).1.IsAmalgamation (yonedaEquiv g).
Русский
Для x : S.functor ⟶ P и g : yoneda.obj X ⟶ P верно, что S.functorInclusion ≫ g = x тогда и только тогда, когда (natTransEquivCompatibleFamily x).1.IsAmalgamation (yonedaEquiv g).
LaTeX
$$S.functorInclusion ≫ g = x ⇔ (natTransEquivCompatibleFamily x).1.IsAmalgamation (yonedaEquiv g)$$
Lean4
/-- (Implementation). A lemma useful to prove `isSheafFor_iff_yonedaSheafCondition`. -/
theorem extension_iff_amalgamation {P : Cᵒᵖ ⥤ Type v₁} (x : S.functor ⟶ P) (g : yoneda.obj X ⟶ P) :
S.functorInclusion ≫ g = x ↔ (natTransEquivCompatibleFamily x).1.IsAmalgamation (yonedaEquiv g) :=
by
change _ ↔ ∀ ⦃Y : C⦄ (f : Y ⟶ X) (h : S f), P.map f.op (yonedaEquiv g) = x.app (op Y) ⟨f, h⟩
constructor
· rintro rfl Y f hf
rw [yonedaEquiv_naturality]
simp [yonedaEquiv_apply]
· intro h
ext Y ⟨f, hf⟩
convert h f hf
rw [yonedaEquiv_naturality]
simp [yonedaEquiv]
