gluedCover — Mathlib

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
Похожие утверждения