Documentation

Mathlib.AlgebraicGeometry.OpenImmersion

Open immersions of schemes #

@[reducible, inline]

A morphism of Schemes is an open immersion if it is an open immersion as a morphism of LocallyRingedSpaces

Equations
Instances For

    To show that a locally ringed space is a scheme, it suffices to show that it has a jointly surjective family of open immersions from affine schemes.

    Equations
    Instances For
      @[deprecated AlgebraicGeometry.IsOpenImmersion.isOpen_range]

      Alias of AlgebraicGeometry.IsOpenImmersion.isOpen_range.

      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

        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 }
          @[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)
          @[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_J {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : (x : 𝒰.J) → (𝒰.obj x).OpenCover) :
          (𝒰.bind f).J = ((i : 𝒰.J) × (f i).J)
          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_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_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_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_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
                  @[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

                  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

                    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.Scheme.Spec.obj { unop := 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}
                          @[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

                            If X ⟶ Y is an open immersion, and Y is a scheme, then so is X.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem AlgebraicGeometry.Scheme.restrict_carrier {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                              (X.restrict h).toPresheafedSpace = U
                              @[simp]
                              theorem AlgebraicGeometry.Scheme.restrict_presheaf_obj {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X✝.toPresheafedSpace} (h : OpenEmbedding f) (X : (TopologicalSpace.Opens U)ᵒᵖ) :
                              (X✝.restrict h).presheaf.obj X = X✝.presheaf.obj { unop := .functor.obj X.unop }
                              @[simp]
                              theorem AlgebraicGeometry.Scheme.restrict_presheaf_map {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                              ∀ {X_1 Y : (TopologicalSpace.Opens U)ᵒᵖ} (f_1 : X_1 Y), (X.restrict h).presheaf.map f_1 = X.presheaf.map (.functor.map f_1.unop).op

                              The restriction of a Scheme along an open embedding.

                              Equations
                              Instances For
                                theorem AlgebraicGeometry.Scheme.restrict_toPresheafedSpace {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                                (X.restrict h).toPresheafedSpace = X.restrict h
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.ofRestrict_val_base {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                                (X.ofRestrict h).val.base = f
                                @[simp]
                                theorem AlgebraicGeometry.Scheme.ofRestrict_val_c_app {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) (V : (TopologicalSpace.Opens X.toPresheafedSpace)ᵒᵖ) :
                                (X.ofRestrict h).val.c.app V = X.presheaf.map (.adjunction.counit.app V.unop).op
                                def AlgebraicGeometry.Scheme.ofRestrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                                X.restrict h X

                                The canonical map from the restriction to the subspace.

                                Equations
                                • X.ofRestrict h = X.ofRestrict h
                                Instances For
                                  instance AlgebraicGeometry.IsOpenImmersion.ofRestrict {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U TopCat.of X.toPresheafedSpace} (h : OpenEmbedding f) :
                                  Equations
                                  • =

                                  An open immersion induces an isomorphism from the domain onto the image

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_snd_of_left {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X Z) (g : Y Z) [H : AlgebraicGeometry.IsOpenImmersion f] :
                                    Set.range CategoryTheory.Limits.pullback.snd.val.base = ((TopologicalSpace.Opens.map g.val.base).obj { carrier := Set.range f.val.base, is_open' := }).carrier
                                    theorem AlgebraicGeometry.IsOpenImmersion.range_pullback_fst_of_right {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X Z) (g : Y Z) [H : AlgebraicGeometry.IsOpenImmersion f] :
                                    Set.range CategoryTheory.Limits.pullback.fst.val.base = ((TopologicalSpace.Opens.map g.val.base).obj { carrier := Set.range f.val.base, is_open' := }).carrier

                                    The universal property of open immersions: For an open immersion f : X ⟶ Z, given any morphism of schemes g : Y ⟶ Z whose topological image is contained in the image of f, we can lift this morphism to a unique Y ⟶ X that commutes with these maps.

                                    Equations
                                    Instances For

                                      Two open immersions with equal range are isomorphic.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[reducible, inline]

                                        The functor opens X ⥤ opens Y associated with an open immersion f : X ⟶ Y.

                                        Equations
                                        Instances For
                                          def AlgebraicGeometry.Scheme.Hom.invApp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : TopologicalSpace.Opens X.toPresheafedSpace) :
                                          X.presheaf.obj { unop := U } Y.presheaf.obj { unop := (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U }

                                          The isomorphism Γ(X, U) ⟶ Γ(Y, f(U)) induced by an open immersion f : X ⟶ Y.

                                          Equations
                                          Instances For

                                            The fg argument is to avoid nasty stuff about dependent types.

                                            theorem AlgebraicGeometry.Scheme.image_basicOpen {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : TopologicalSpace.Opens X.toPresheafedSpace} (r : (X.presheaf.obj { unop := U })) :

                                            The image of an open immersion as an open set.

                                            Equations
                                            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
                                              @[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'_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 (𝒰.map x) f
                                                @[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

                                                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
                                                  theorem AlgebraicGeometry.Scheme.OpenCover.iUnion_range {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) :
                                                  ⋃ (i : 𝒰.J), Set.range (𝒰.map i).val.base = Set.univ
                                                  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_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_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_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
                                                    • One or more equations did not get rendered due to their size.
                                                    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.Scheme.Spec.obj { unop := 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_f {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) :
                                                        ∀ (a : X.toPresheafedSpace), 𝓤.openCover.f a = 𝓤.f a
                                                        @[simp]
                                                        theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_obj {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (j : 𝓤.J) :
                                                        𝓤.openCover.obj j = AlgebraicGeometry.Scheme.Spec.obj { unop := 𝓤.obj j }
                                                        @[simp]
                                                        theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_J {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) :
                                                        𝓤.openCover.J = 𝓤.J
                                                        @[simp]
                                                        theorem AlgebraicGeometry.Scheme.AffineOpenCover.openCover_map {X : AlgebraicGeometry.Scheme} (𝓤 : X.AffineOpenCover) (j : 𝓤.J) :
                                                        𝓤.openCover.map j = 𝓤.map 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.Scheme.Spec.obj { unop := 𝓤.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