Documentation

Mathlib.AlgebraicGeometry.Cover.Open

Open covers of schemes #

This file provides the basic API for open covers of schemes.

Main definition #

An open cover of X consists of a family of open immersions into X, and for each x : X an open immersion (indexed by f x) that covers x.

This is merely a coverage in the Zariski pretopology, and it would be optimal if we could reuse the existing API about pretopologies, However, the definitions of sieves and grothendieck topologies uses Props, so that the actual open sets and immersions are hard to obtain. Also, since such a coverage in the pretopology usually contains a proper class of immersions, it is quite hard to glue them, reason about finite covers, etc.

  • J : Type v

    index set of an open cover of a scheme X

  • obj : self.JAlgebraicGeometry.Scheme

    the subschemes of an open cover

  • map : (j : self.J) → self.obj j X

    the embedding of subschemes to X

  • f : X.toPresheafedSpaceself.J

    given a point of x : X, f x is the index of the subscheme which contains x

  • covers : ∀ (x : X.toPresheafedSpace), x Set.range (self.map (self.f x)).val.base

    the subschemes covers X

  • IsOpen : ∀ (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x)

    the embedding of subschemes are open immersions

Instances For
    theorem AlgebraicGeometry.Scheme.OpenCover.covers {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : X.toPresheafedSpace) :
    x Set.range (self.map (self.f x)).val.base

    the subschemes covers X

    the embedding of subschemes are open immersions

    @[deprecated AlgebraicGeometry.Scheme.OpenCover.covers]
    theorem AlgebraicGeometry.Scheme.OpenCover.Covers {X : AlgebraicGeometry.Scheme} (self : X.OpenCover) (x : X.toPresheafedSpace) :
    x Set.range (self.map (self.f x)).val.base

    Alias of AlgebraicGeometry.Scheme.OpenCover.covers.


    the subschemes covers X

    The affine cover of a scheme.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • AlgebraicGeometry.Scheme.instInhabitedOpenCover = { default := X.affineCover }
      theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
      ⋃ (i : 𝒰.J), Set.range (𝒰.map i).val.base = Set.univ
      @[simp]
      theorem AlgebraicGeometry.Scheme.OpenCover.bind_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) :
      (𝒰.bind f).J = ((i : 𝒰.J) × (f i).J)
      @[simp]
      theorem AlgebraicGeometry.Scheme.OpenCover.bind_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) (x : (i : 𝒰.J) × (f i).J) :
      (𝒰.bind f).obj x = (f x.fst).obj x.snd
      @[simp]
      theorem AlgebraicGeometry.Scheme.OpenCover.bind_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) (x : (i : 𝒰.J) × (f i).J) :
      (𝒰.bind f).map x = CategoryTheory.CategoryStruct.comp ((f x.fst).map x.snd) (𝒰.map x.fst)
      def AlgebraicGeometry.Scheme.OpenCover.bind {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) :
      X.OpenCover

      Given an open cover { Uᵢ } of X, and for each Uᵢ an open cover, we may combine these open covers to form an open cover of X.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        An isomorphism X ⟶ Y is an open cover of Y.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem AlgebraicGeometry.Scheme.OpenCover.copy_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : JAlgebraicGeometry.Scheme) (map : (i : J) → obj i X) (e₁ : J 𝒰.J) (e₂ : (i : J) → obj i 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) :
          (𝒰.copy J obj map e₁ e₂✝ e₂).J = J
          @[simp]
          theorem AlgebraicGeometry.Scheme.OpenCover.copy_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : JAlgebraicGeometry.Scheme) (map : (i : J) → obj i X) (e₁ : J 𝒰.J) (e₂ : (i : J) → obj i 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) :
          ∀ (a : J), (𝒰.copy J obj map e₁ e₂✝ e₂).obj a = obj a
          @[simp]
          theorem AlgebraicGeometry.Scheme.OpenCover.copy_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : JAlgebraicGeometry.Scheme) (map : (i : J) → obj i X) (e₁ : J 𝒰.J) (e₂ : (i : J) → obj i 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) (i : J) :
          (𝒰.copy J obj map e₁ e₂✝ e₂).map i = map i
          def AlgebraicGeometry.Scheme.OpenCover.copy {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (J : Type u_1) (obj : JAlgebraicGeometry.Scheme) (map : (i : J) → obj i X) (e₁ : J 𝒰.J) (e₂ : (i : J) → obj i 𝒰.obj (e₁ i)) (e₂ : ∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂✝ i).hom (𝒰.map (e₁ i))) :
          X.OpenCover

          We construct an open cover from another, by providing the needed fields and showing that the provided fields are isomorphic with the original open cover.

          Equations
          • 𝒰.copy J obj map e₁ e₂✝ e₂ = { J := J, obj := obj, map := map, f := fun (x : X.toPresheafedSpace) => e₁.symm (𝒰.f x), covers := , IsOpen := }
          Instances For
            @[simp]
            theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Y) [CategoryTheory.IsIso f] :
            ∀ (x : 𝒰.J), (𝒰.pushforwardIso f).map x = CategoryTheory.CategoryStruct.comp (𝒰.map x) f
            @[simp]
            theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_J {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Y) [CategoryTheory.IsIso f] :
            (𝒰.pushforwardIso f).J = 𝒰.J
            @[simp]
            theorem AlgebraicGeometry.Scheme.OpenCover.pushforwardIso_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X Y) [CategoryTheory.IsIso f] :
            ∀ (x : 𝒰.J), (𝒰.pushforwardIso f).obj x = 𝒰.obj x

            The pushforward of an open cover along an isomorphism.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              @[simp]
              theorem AlgebraicGeometry.Scheme.OpenCover.add_f {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y X) [AlgebraicGeometry.IsOpenImmersion f] (x : X.toPresheafedSpace) :
              (𝒰.add f).f x = some (𝒰.f x)
              @[simp]
              theorem AlgebraicGeometry.Scheme.OpenCover.add_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y X) [AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J) :
              (𝒰.add f).map i = Option.rec f 𝒰.map i
              @[simp]
              theorem AlgebraicGeometry.Scheme.OpenCover.add_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : Y X) [AlgebraicGeometry.IsOpenImmersion f] (i : Option 𝒰.J) :
              (𝒰.add f).obj i = Option.rec Y 𝒰.obj i

              Adding an open immersion into an open cover gives another open cover.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_map {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) (x : 𝒰.J) :
                (𝒰.pullbackCover f).map x = CategoryTheory.Limits.pullback.fst f (𝒰.map x)
                @[simp]
                theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_f {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) (x : W.toPresheafedSpace) :
                (𝒰.pullbackCover f).f x = 𝒰.f (f.val.base x)
                @[simp]
                theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_obj {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) (x : 𝒰.J) :
                (𝒰.pullbackCover f).obj x = CategoryTheory.Limits.pullback f (𝒰.map x)
                @[simp]
                theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover_J {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) :
                (𝒰.pullbackCover f).J = 𝒰.J

                Given an open cover on X, we may pull them back along a morphism W ⟶ X to obtain an open cover of W.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_J {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) :
                  (𝒰.pullbackCover' f).J = 𝒰.J
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_map {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) (x : 𝒰.J) :
                  (𝒰.pullbackCover' f).map x = CategoryTheory.Limits.pullback.snd (𝒰.map x) f
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_obj {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) (x : 𝒰.J) :
                  (𝒰.pullbackCover' f).obj x = CategoryTheory.Limits.pullback (𝒰.map x) f
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.OpenCover.pullbackCover'_f {X : AlgebraicGeometry.Scheme} {W : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : W X) (x : W.toPresheafedSpace) :
                  (𝒰.pullbackCover' f).f x = 𝒰.f (f.val.base x)

                  Given an open cover on X, we may pull them back along a morphism f : W ⟶ X to obtain an open cover of W. This is similar to Scheme.OpenCover.pullbackCover, but here we take pullback (𝒰.map x) f instead of pullback f (𝒰.map x).

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_map {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace X.toPresheafedSpace] (x : { x : X.toPresheafedSpace // x .choose }) :
                    𝒰.finiteSubcover.map x = 𝒰.map (𝒰.f x)
                    @[simp]
                    theorem AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_obj {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace X.toPresheafedSpace] (x : { x : X.toPresheafedSpace // x .choose }) :
                    𝒰.finiteSubcover.obj x = 𝒰.obj (𝒰.f x)
                    def AlgebraicGeometry.Scheme.OpenCover.finiteSubcover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace X.toPresheafedSpace] :
                    X.OpenCover

                    Every open cover of a quasi-compact scheme can be refined into a finite subcover.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      instance AlgebraicGeometry.Scheme.instFintypeJFiniteSubcover {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [H : CompactSpace X.toPresheafedSpace] :
                      Fintype 𝒰.finiteSubcover.J
                      Equations
                      theorem AlgebraicGeometry.Scheme.OpenCover.compactSpace {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [Finite 𝒰.J] [H : ∀ (i : 𝒰.J), CompactSpace (𝒰.obj i).toPresheafedSpace] :
                      CompactSpace X.toPresheafedSpace
                      def AlgebraicGeometry.Scheme.OpenCover.inter {X : AlgebraicGeometry.Scheme} (𝒰₁ : X.OpenCover) (𝒰₂ : X.OpenCover) :
                      X.OpenCover

                      Given open covers { Uᵢ } and { Uⱼ }, we may form the open cover { Uᵢ ∩ Uⱼ }.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_map {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sTopologicalSpace.Opens X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ) (i : s) :
                        (X.openCoverOfSuprEqTop U hU).map i = X.ofRestrict
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_J {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sTopologicalSpace.Opens X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ) :
                        (X.openCoverOfSuprEqTop U hU).J = s
                        @[simp]
                        theorem AlgebraicGeometry.Scheme.openCoverOfSuprEqTop_obj {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sTopologicalSpace.Opens X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ) (i : s) :
                        (X.openCoverOfSuprEqTop U hU).obj i = X.restrict
                        def AlgebraicGeometry.Scheme.openCoverOfSuprEqTop {s : Type u_1} (X : AlgebraicGeometry.Scheme) (U : sTopologicalSpace.Opens X.toPresheafedSpace) (hU : ⨆ (i : s), U i = ) :
                        X.OpenCover

                        If U is a family of open sets that covers X, then X.restrict U forms an X.open_cover.

                        Equations
                        • X.openCoverOfSuprEqTop U hU = { J := s, obj := fun (i : s) => X.restrict , map := fun (i : s) => X.ofRestrict , f := fun (x : X.toPresheafedSpace) => .choose, covers := , IsOpen := }
                        Instances For

                          An affine open cover of X consists of a family of open immersions into X from spectra of rings.

                          • J : Type v

                            index set of an affine open cover of a scheme X

                          • obj : self.JCommRingCat

                            the ring associated to a component of an affine open cover

                          • map : (j : self.J) → AlgebraicGeometry.Spec (self.obj j) X

                            the embedding of subschemes to X

                          • f : X.toPresheafedSpaceself.J

                            given a point of x : X, f x is the index of the subscheme which contains x

                          • covers : ∀ (x : X.toPresheafedSpace), x Set.range (self.map (self.f x)).val.base

                            the subschemes covers X

                          • IsOpen : ∀ (x : self.J), AlgebraicGeometry.IsOpenImmersion (self.map x)

                            the embedding of subschemes are open immersions

                          Instances For
                            theorem AlgebraicGeometry.Scheme.AffineOpenCover.covers {X : AlgebraicGeometry.Scheme} (self : X.AffineOpenCover) (x : X.toPresheafedSpace) :
                            x Set.range (self.map (self.f x)).val.base

                            the subschemes covers X

                            theorem AlgebraicGeometry.Scheme.AffineOpenCover.IsOpen {X : AlgebraicGeometry.Scheme} (self : X.AffineOpenCover) (x : self.J) :

                            the embedding of subschemes are open immersions

                            @[simp]
                            theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_map {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (j : 𝓤.J) :
                            𝓤.openCover.map j = 𝓤.map j
                            @[simp]
                            theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) :
                            ∀ (a : X.toPresheafedSpace), 𝓤.openCover.f a = 𝓤.f a
                            @[simp]
                            theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_J {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) :
                            𝓤.openCover.J = 𝓤.J
                            @[simp]
                            theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_obj {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (j : 𝓤.J) :
                            𝓤.openCover.obj j = AlgebraicGeometry.Spec (𝓤.obj j)
                            def AlgebraicGeometry.Scheme.AffineOpenCover.openCover {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) :
                            X.OpenCover

                            The open cover associated to an affine open cover.

                            Equations
                            • 𝓤.openCover = { J := 𝓤.J, obj := fun (j : 𝓤.J) => AlgebraicGeometry.Spec (𝓤.obj j), map := 𝓤.map, f := 𝓤.f, covers := , IsOpen := }
                            Instances For

                              A choice of an affine open cover of a scheme.

                              Equations
                              • X.affineOpenCover = { J := X.affineCover.J, obj := fun (j : X.affineCover.J) => .choose, map := X.affineCover.map, f := X.affineCover.f, covers := , IsOpen := }
                              Instances For
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.openCover_affineOpenCover (X : AlgebraicGeometry.Scheme) :
                                X.affineOpenCover.openCover = X.affineCover
                                def AlgebraicGeometry.Scheme.OpenCover.affineRefinement {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) :
                                X.AffineOpenCover

                                Given any open cover 𝓤, this is an affine open cover which refines it. The morphism in the category of open covers which proves that this is indeed a refinement, see AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  structure AlgebraicGeometry.Scheme.OpenCover.Hom {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) (𝓥 : X.OpenCover) :
                                  Type (max u v)

                                  A morphism between open covers 𝓤 ⟶ 𝓥 indicates that 𝓤 is a refinement of 𝓥. Since open covers of schemes are indexed, the definition also involves a map on the indexing types.

                                  • idx : 𝓤.J𝓥.J

                                    The map on indexing types associated to a morphism of open covers.

                                  • app : (j : 𝓤.J) → 𝓤.obj j 𝓥.obj (self.idx j)

                                    The morphism between open subsets associated to a morphism of open covers.

                                  • isOpen : ∀ (j : 𝓤.J), AlgebraicGeometry.IsOpenImmersion (self.app j)
                                  • w : ∀ (j : 𝓤.J), CategoryTheory.CategoryStruct.comp (self.app j) (𝓥.map (self.idx j)) = 𝓤.map j
                                  Instances For
                                    theorem AlgebraicGeometry.Scheme.OpenCover.Hom.isOpen {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) :
                                    @[simp]
                                    theorem AlgebraicGeometry.Scheme.OpenCover.Hom.w {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) :
                                    CategoryTheory.CategoryStruct.comp (self.app j) (𝓥.map (self.idx j)) = 𝓤.map j
                                    @[simp]
                                    theorem AlgebraicGeometry.Scheme.OpenCover.Hom.w_assoc {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} (self : 𝓤.Hom 𝓥) (j : 𝓤.J) {Z : AlgebraicGeometry.Scheme} (h : X Z) :
                                    def AlgebraicGeometry.Scheme.OpenCover.Hom.id {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) :
                                    𝓤.Hom 𝓤

                                    The identity morphism in the category of open covers of a scheme.

                                    Equations
                                    Instances For
                                      def AlgebraicGeometry.Scheme.OpenCover.Hom.comp {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} {𝓦 : X.OpenCover} (f : 𝓤.Hom 𝓥) (g : 𝓥.Hom 𝓦) :
                                      𝓤.Hom 𝓦

                                      The composition of two morphisms in the category of open covers of a scheme.

                                      Equations
                                      Instances For
                                        @[simp]
                                        @[simp]
                                        theorem AlgebraicGeometry.Scheme.OpenCover.comp_idx_apply {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} {𝓦 : X.OpenCover} (f : 𝓤 𝓥) (g : 𝓥 𝓦) (j : 𝓤.J) :
                                        (CategoryTheory.CategoryStruct.comp f g).idx j = g.idx (f.idx j)
                                        @[simp]
                                        theorem AlgebraicGeometry.Scheme.OpenCover.comp_app {X : AlgebraicGeometry.Scheme} {𝓤 : X.OpenCover} {𝓥 : X.OpenCover} {𝓦 : X.OpenCover} (f : 𝓤 𝓥) (g : 𝓥 𝓦) (j : 𝓤.J) :
                                        def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement {X : AlgebraicGeometry.Scheme} (𝓤 : X.OpenCover) :
                                        𝓤.affineRefinement.openCover 𝓤

                                        Given any open cover 𝓤, this is an affine open cover which refines it.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem AlgebraicGeometry.Scheme.OpenCover.ext_elem {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (f : (X.presheaf.obj (Opposite.op U))) (g : (X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.J), (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) f = (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) g) :
                                          f = g

                                          If two global sections agree after restriction to each member of an open cover, then they agree globally.

                                          theorem AlgebraicGeometry.Scheme.zero_of_zero_cover {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (s : (X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) (h : ∀ (i : 𝒰.J), (AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) s = 0) :
                                          s = 0

                                          If the restriction of a global section to each member of an open cover is zero, then it is globally zero.

                                          theorem AlgebraicGeometry.Scheme.isNilpotent_of_isNilpotent_cover {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens X.toPresheafedSpace} (s : (X.presheaf.obj (Opposite.op U))) (𝒰 : X.OpenCover) [Finite 𝒰.J] (h : ∀ (i : 𝒰.J), IsNilpotent ((AlgebraicGeometry.Scheme.Hom.app (𝒰.map i) U) s)) :

                                          If a global section is nilpotent on each member of a finite open cover, then f is nilpotent.

                                          The basic open sets form an affine open cover of Spec R.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            We may bind the basic open sets of an open affine cover to form an affine cover that is also a basis.

                                            Equations
                                            Instances For

                                              The coordinate ring of a component in the affine_basis_cover.

                                              Equations
                                              Instances For
                                                theorem AlgebraicGeometry.Scheme.affineBasisCover_obj (X : AlgebraicGeometry.Scheme) (i : X.affineBasisCover.J) :
                                                X.affineBasisCover.obj i = AlgebraicGeometry.Spec (X.affineBasisCoverRing i)
                                                theorem AlgebraicGeometry.Scheme.affineBasisCover_map_range (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) (r : .choose) :
                                                Set.range (X.affineBasisCover.map x, r).val.base = (X.affineCover.map x).val.base '' (PrimeSpectrum.basicOpen r).carrier
                                                theorem AlgebraicGeometry.Scheme.affineBasisCover_is_basis (X : AlgebraicGeometry.Scheme) :
                                                TopologicalSpace.IsTopologicalBasis {x : Set X.toPresheafedSpace | ∃ (a : X.affineBasisCover.J), x = Set.range (X.affineBasisCover.map a).val.base}