English
One can construct a glue data from an open cover by taking the opens U i as subobjects and defining the overlap maps via inclusions, with natural coherence conditions.
Русский
Можно построить данные склейки из открытого покрытия, взяв открытые множества U_i как подобъекты и задав отображения пересечений через включения, удовлетворяющие естественной когерентности.
LaTeX
$$def ofOpenSubsets : TopCat.GlueData.{u}$$
Lean4
/-- We may construct a glue data from a family of open sets. -/
@[simps! toGlueData_J toGlueData_U toGlueData_V toGlueData_t toGlueData_f]
def ofOpenSubsets : TopCat.GlueData.{u} :=
mk'.{u}
{ J
U := fun i => (Opens.toTopCat <| TopCat.of α).obj (U i)
V := fun _ j => (Opens.map <| Opens.inclusion' _).obj (U j)
t := fun i j => ofHom ⟨fun x => ⟨⟨x.1.1, x.2⟩, x.1.2⟩, by fun_prop⟩
V_id := fun i => by simp
t_id := fun i => by ext; rfl
t_inter := fun _ _ _ _ hx => hx
cocycle := fun _ _ _ _ _ => rfl }
