Lean4
/-- The glue data associated with an open cover.
The canonical isomorphism `𝒰.gluedCover.glued ⟶ X` is provided by `𝒰.fromGlued`. -/
@[simps]
def gluedCover : Scheme.GlueData.{u} where
J := 𝒰.I₀
U := 𝒰.X
V := fun ⟨x, y⟩ => pullback (𝒰.f x) (𝒰.f y)
f _ _ := pullback.fst _ _
f_id _ := inferInstance
t _ _ := (pullbackSymmetry _ _).hom
t_id x := by simp
t' x y z := gluedCoverT' 𝒰 x y z
t_fac x y
z := by
apply pullback.hom_ext <;>
simp
-- The `cocycle` field could have been `by tidy` but lean timeouts.
cocycle x y z := glued_cover_cocycle 𝒰 x y z
f_open _ := inferInstance