gluing — Mathlib

Lean4
/-- Given `Uᵢ ×[Z] Y`, this is the glued fibred product `X ×[Z] Y`. -/
@[simps U V f t t', simps -isSimp J]
def gluing : Scheme.GlueData.{u} where
  J := 𝒰.I₀
  U i := pullback (𝒰.f i ≫ f) g
  V := fun ⟨i, j⟩ => v 𝒰 f g i j
  f _ _ := pullback.fst _ _
  f_id _ := inferInstance
  f_open := inferInstance
  t i j := t 𝒰 f g i j
  t_id i := t_id 𝒰 f g i
  t' i j k := t' 𝒰 f g i j k
  t_fac i j
    k := by
    apply pullback.hom_ext
    on_goal 1 => apply pullback.hom_ext
    all_goals simp only [t'_snd_fst_fst, t'_snd_fst_snd, t'_snd_snd, t_fst_fst, t_fst_snd, t_snd, Category.assoc]
  cocycle i j k := cocycle 𝒰 f g i j k
Похожие утверждения