The small affine Zariski site as an open cover

This file records that the affine opens of a scheme X, indexed by its small affine Zariski site X.AffineZariskiSite, form an open cover of X, together with the transition maps of the pulled-back directed affine cover.

Transition maps of the pulled-back directed affine cover

Let q : T ⟶ X be a morphism of schemes. Pulling back Mathlib's directed cover of X by its affine opens (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover) along q gives a locally directed cover of T, whose member over an affine open U is identified with the inverse image q⁻¹ U by AlgebraicGeometry.pullbackRestrictIsoRestrict. This file records that, under these identifications, the transition maps of the pulled-back cover are the inclusions of inverse images. This is the compatibility needed to glue morphisms out of T along this cover with AlgebraicGeometry.Scheme.OpenCover.glueMorphismsOfLocallyDirected.

Main results

• Scheme.AffineZariskiSite.isOpenCover_toOpens: the affine opens of X, indexed by the small affine Zariski site, form an open cover of X.
• Scheme.AffineZariskiSite.directedCover_pullback₁_trans_pullbackRestrictIsoRestrict_hom: the transition map of (directedCover X).pullback₁ q along U ⟶ V is the inclusion q⁻¹ U ⟶ q⁻¹ V.

theorem AlgebraicGeometry.Scheme.AffineZariskiSite.isOpenCover_toOpens (X : Scheme) : TopologicalSpace.IsOpenCover fun (U : X.AffineZariskiSite) => U.toOpens

The affine opens of X cover X, indexed by the small affine Zariski site.

theorem TauCeti.AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_pullback₁_trans_pullbackRestrictIsoRestrict_hom {X T : AlgebraicGeometry.Scheme} (q : T ⟶ X) {U V : X.AffineZariskiSite} (i : U ⟶ V) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ q (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X)) i) (AlgebraicGeometry.pullbackRestrictIsoRestrict q V.toOpens).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict q U.toOpens).hom (T.homOfLE ⋯)

Under the identification of the members of the pulled-back directed affine cover with inverse images of affine opens, its transition map along U ⟶ V is the inclusion q⁻¹ U ⟶ q⁻¹ V.

theorem TauCeti.AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_pullback₁_trans_pullbackRestrictIsoRestrict_hom_assoc {X T : AlgebraicGeometry.Scheme} (q : T ⟶ X) {U V : X.AffineZariskiSite} (i : U ⟶ V) {Z : AlgebraicGeometry.Scheme} (h : ↑((TopologicalSpace.Opens.map q.base).obj V.toOpens) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.trans (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ q (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X)) i) (AlgebraicGeometry.pullbackRestrictIsoRestrict q V.toOpens).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackRestrictIsoRestrict q U.toOpens).hom (T.homOfLE ⋯)) h

Under the identification of the members of the pulled-back directed affine cover with inverse images of affine opens, its transition map along U ⟶ V is the inclusion q⁻¹ U ⟶ q⁻¹ V.