Lean4
/-- We get a family of gluing data by taking `U i = X i` and `V i j = (hf i).rep.pullback (f j)`. -/
@[simps]
noncomputable def glueData : GlueData where
J := ι
U := X
V := fun (i, j) ↦ (hf i).rep.pullback (f j)
f i j := (hf i).rep.fst' (f j)
f_mono i
j :=
have := (hf j).property _ _ _ ((hf i).1.isPullback' (f j)).flip
IsOpenImmersion.mono _
f_id i := IsOpenImmersion.isIso_fst'_self IsOpenImmersion.le_monomorphisms (hf i)
t i j := (hf i).rep.symmetry (hf j).rep
t_id
i := by
apply (hf i).rep.hom_ext' <;> simp [IsOpenImmersion.fst'_self_eq_snd IsOpenImmersion.le_monomorphisms (hf i)]
t' i j k := lift₃ _ _ _ (pullback₃.p₂ _ _ _) (pullback₃.p₃ _ _ _) (pullback₃.p₁ _ _ _) (by simp) (by simp)
t_fac i j k := (hf j).rep.hom_ext' (by simp) (by simp)
cocycle i j k := pullback₃.hom_ext (by simp) (by simp) (by simp)
f_open i j := (hf j).property _ _ _ ((hf i).1.isPullback' (f j)).flip
