Lean4
/-- This is a constructor of `TopCat.GlueData` whose arguments are in terms of elements and
intersections rather than subobjects and pullbacks. Please refer to `TopCat.GlueData.MkCore` for
details. -/
def mk' (h : MkCore.{u}) : TopCat.GlueData where
J := h.J
U := h.U
V i := (Opens.toTopCat _).obj (h.V i.1 i.2)
f i j := (h.V i j).inclusion'
f_id i := (h.V_id i).symm ▸ (Opens.inclusionTopIso (h.U i)).isIso_hom
f_open := fun i j : h.J => (h.V i j).isOpenEmbedding
t := h.t
t_id i := by ext; rw [h.t_id]; rfl
t' := h.t'
t_fac i j
k := by
delta MkCore.t'
rw [Category.assoc, Category.assoc, pullbackIsoProdSubtype_inv_snd, ← Iso.eq_inv_comp,
pullbackIsoProdSubtype_inv_fst_assoc]
ext ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
rfl
cocycle i j
k := by
delta MkCore.t'
simp_rw [← Category.assoc]
rw [Iso.comp_inv_eq]
simp only [Iso.inv_hom_id_assoc, Category.assoc, Category.id_comp]
rw [← Iso.eq_inv_comp, Iso.inv_hom_id]
ext1 ⟨⟨⟨x, hx⟩, ⟨x', hx'⟩⟩, rfl : x = x'⟩
dsimp only [Opens.coe_inclusion', hom_comp, hom_ofHom, ContinuousMap.comp_assoc, ContinuousMap.comp_apply,
ContinuousMap.coe_mk, hom_id, ContinuousMap.id_apply]
rw [Subtype.mk_eq_mk, Prod.mk_inj, Subtype.mk_eq_mk, Subtype.ext_iff, and_self_iff]
convert congr_arg Subtype.val (h.t_inv k i ⟨x, hx'⟩) using 3
refine Subtype.ext ?_
exact h.cocycle i j k ⟨x, hx⟩ hx'
f_mono _ _ := (TopCat.mono_iff_injective _).mpr fun _ _ h => Subtype.ext h
