English
Generalized compatibility condition for gluing; see above for the specific forms.
Русский
Обобщённое условие совместимости для склейки; см. выше конкретные формы.
LaTeX
$$Eq (CategoryTheory.Functor.category.comp (CategoryTheory.yoneda.map a) (f i)) (CategoryTheory.Functor.category.comp (CategoryTheory.yoneda.map b) (f j)) -> Eq (CategoryTheory.Scheme.instCategory.comp a (toGlued hf i)) (CategoryTheory.Scheme.instCategory.comp b (toGlued hf j))$$
Lean4
theorem overEquiv_generate_toPresieveOver_eq_ofArrows {X : Over S} (𝒰 : Cover.{u} (precoverage P) X.left) [𝒰.Over S] :
Sieve.overEquiv X (Sieve.generate 𝒰.toPresieveOver) = Sieve.ofArrows 𝒰.X 𝒰.f :=
by
ext V f
simp only [Sieve.overEquiv_iff, Functor.const_obj_obj, Sieve.generate_apply]
constructor
· rintro ⟨U, h, g, ⟨k⟩, hcomp⟩
exact ⟨𝒰.X k, h.left, 𝒰.f k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩
· rintro ⟨U, h, g, ⟨k⟩, hcomp⟩
have : 𝒰.f k ≫ X.hom = 𝒰.X k ↘ S := comp_over (𝒰.f k) S
refine ⟨(𝒰.X k).asOver S, Over.homMk h (by simp [← hcomp, this]), (𝒰.f k).asOver S, ⟨k⟩, ?_⟩
ext : 1
simpa
