English
There is an instance showing that a cover functor composed with forget is locally directed.
Русский
Существует инстанс, доказывающий, что покрытие образует локально-направленное множество при композиции с забывающим функтором.
LaTeX
$$$(\mathcal{U}.functorOfLocallyDirected \circ forget).IsLocallyDirected$$$
Lean4
/-- If `𝒰` is an open cover such that the images of the components form a basis of the topology
of `X`, `𝒰` is directed by the ordering of subset inclusion of the images. -/
def ofIsBasisOpensRange {𝒰 : X.OpenCover} [Preorder 𝒰.I₀]
(hle : ∀ {i j : 𝒰.I₀}, i ≤ j ↔ (𝒰.f i).opensRange ≤ (𝒰.f j).opensRange)
(H : TopologicalSpace.Opens.IsBasis (Set.range <| fun i ↦ (𝒰.f i).opensRange)) : 𝒰.LocallyDirected
where
trans {i j} hij := IsOpenImmersion.lift (𝒰.f j) (𝒰.f i) (hle.mp (leOfHom hij))
trans_id i := by rw [← cancel_mono (𝒰.f i)]; simp
trans_comp hij hjk := by rw [← cancel_mono (𝒰.f _)]; simp
directed {i j}
x :=
by
have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).base x ∈ (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).opensRange := ⟨x, rfl⟩
obtain ⟨k, ⟨k, rfl⟩, ⟨y, hy⟩, h⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp H this
refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩
· rw [Scheme.Hom.opensRange_comp]
exact Set.image_subset_range _ _
· simp_rw [pullback.condition, Scheme.Hom.opensRange_comp]
exact Set.image_subset_range _ _
· apply (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).isOpenEmbedding.injective
rw [← Scheme.comp_base_apply, pullback.lift_fst_assoc, IsOpenImmersion.lift_fac, hy]
