NYLL
Module

FiniteRelativeSpec.lean

Nyll.SchemeTheory.Modules.FiniteRelativeSpec
19 declarations indexed from sourceView source ↗

Module documentation

Relative spectra of quasicoherent sheaves of commutative algebras

The input is an actual sheaf of commutative rings and its structure map from the structure sheaf. Its underlying module is obtained by the existing restriction-of-scalars functor. Quasicoherence of that native module supplies the localization of the actual section rings. The existing affine Zariski relative gluing construction then gives the scheme and its finite structure morphism whenever the affine section algebras are finite.

Imports9
  • Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
  • Mathlib.Algebra.Category.ModuleCat.Sheaf
  • Mathlib.AlgebraicGeometry.Modules.Sheaf
  • Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
  • Mathlib.AlgebraicGeometry.Morphisms.Finite
  • Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
  • Mathlib.RingTheory.RingHom.Finite
  • Mathlib.RingTheory.Localization.Away.Basic
  • Nyll.SchemeTheory.Modules.QuasicoherentAffineLocalization
Imported by3

Declarations

theorem

isFinite_comp_iso

L36 ↗
AlgebraicGeometry.Scheme.RelativeSpec.isFinite_comp_iso
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
Lean source · statement
theorem isFinite_comp_iso {Y Z W : Scheme.{u}}
    (f : Y ⟶ Z) (e : Z ≅ W) (hf : IsFinite f)
    (hRespect : MorphismProperty.RespectsIso (@IsFinite : MorphismProperty Scheme.{u})) :
    IsFinite (f ≫ e.hom)
def

underlyingModule

L45 ↗
AlgebraicGeometry.Scheme.RelativeSpec.underlyingModule
Documentation

The underlying native module of a sheaf of commutative 𝒪_X-algebras.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
Lean source · statement
def underlyingModule (α : X.sheaf ⟶ A) : X.Modules
theorem

isLocalization_basicOpen

L58 ↗
AlgebraicGeometry.Scheme.RelativeSpec.isLocalization_basicOpen
Documentation

Quasicoherence of the underlying module makes the actual algebra restriction on every affine basic open a ring localization.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
Lean source · full declaration
theorem isLocalization_basicOpen (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent]
    (U : X.AffineZariskiSite) (f : Γ(X, U.1)) :
    let q := A.obj.map (homOfLE (X.basicOpen_le f)).op
    let : Algebra (A.obj.obj (op U.1)) (A.obj.obj (op (X.basicOpen f))) :=
      q.hom.toAlgebra
    IsLocalization.Away (α.hom.app (op U.1) f)
      (A.obj.obj (op (X.basicOpen f))) := by
  let B : CommRingCat.{u} := A.obj.obj (op U.1)
  let C : CommRingCat.{u} := A.obj.obj (op (X.basicOpen f))
  let q : B ⟶ C := A.obj.map (homOfLE (X.basicOpen_le f)).op
  let ι : Γ(X, U.1) →+* B := (α.hom.app (op U.1)).hom
  let ι' : Γ(X, X.basicOpen f) →+* C := (α.hom.app (op (X.basicOpen f))).hom
  let r : Γ(X, U.1) →+* Γ(X, X.basicOpen f) :=
    (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom
  let : Algebra B C := q.hom.toAlgebra
  change IsLocalization.Away (ι f) C
  have hnat (x : Γ(X, U.1)) : q.hom (ι x) = ι' (r x) := by
    exact (congrArg (fun e : Γ(X, U.1) ⟶ C => e.hom x)
      (α.hom.naturality (homOfLE (X.basicOpen_le f)).op)).symm
  obtain ⟨hsurj, hker⟩ :=
    Modules.basicOpenLocalization_of_isQuasicoherent
      (underlyingModule α) ⟨U.1, U.2⟩ f
  refine IsLocalization.Away.mk (ι f) ?_ ?_ ?_
  · change IsUnit (q.hom (ι f))
    rw [hnat]
    exact (RingedSpace.isUnit_res_basicOpen X.toRingedSpace f).map ι'
  · intro s
    obtain ⟨n, y, hy⟩ := hsurj s
    change q.hom y = ι' (r (f ^ n)) * s at hy
    refine ⟨n, y, ?_⟩
    change s * q.hom (ι f) ^ n = q.hom y
    have hp : q.hom (ι f) ^ n = ι' (r (f ^ n)) := by
      simp only [map_pow, hnat]
    rw [hp]
    exact (mul_comm s _).trans hy.symm
  · intro a b hab
    change q.hom a = q.hom b at hab
    have hz : (underlyingModule α).presheaf.map
        (homOfLE (X.basicOpen_le f)).op (a - b) = 0 := by
      change q.hom (a - b) = 0
      rw [map_sub, hab, sub_self]
    obtain ⟨n, hn⟩ := hker (a - b) hz
    refine ⟨n, ?_⟩
    change ι (f ^ n) * (a - b) = 0 at hn
    rw [map_pow, mul_sub, sub_eq_zero] at hn
    exact hn
theorem

coequifibered

L108 ↗
AlgebraicGeometry.Scheme.RelativeSpec.coequifibered
Documentation

The affine diagram is cartesian on rings because its actual section restriction maps are localizations.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
Lean source · statement
theorem coequifibered (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    (Functor.whiskerLeft (AffineZariskiSite.toOpensFunctor X).op α.hom).Coequifibered
def

gluingData

L116 ↗
AlgebraicGeometry.Scheme.RelativeSpec.gluingData
Documentation

The diagram of literal spectra of the section algebras.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
Lean source · statement
def gluingData (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    (AffineZariskiSite.directedCover X).RelativeGluingData
instance

gluingData_isLocallyDirected

L122 ↗
AlgebraicGeometry.Scheme.RelativeSpec.gluingData_isLocallyDirected
Documentation

The named gluing diagram uses the native locally directed colimit construction.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
Lean source · statement
instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected
def

scheme

L129 ↗
AlgebraicGeometry.Scheme.RelativeSpec.scheme
Documentation

The relative spectrum, constructed by gluing the affine section spectra.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
Lean source · statement
def scheme (α : X.sheaf ⟶ A) [(underlyingModule α).IsQuasicoherent] : Scheme.{u}
def

toBase

L133 ↗
AlgebraicGeometry.Scheme.RelativeSpec.toBase
Documentation

The structure morphism of the actual relative spectrum.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
Lean source · statement
def toBase (α : X.sheaf ⟶ A) [(underlyingModule α).IsQuasicoherent] : scheme α ⟶ X
def

openCover

L137 ↗
AlgebraicGeometry.Scheme.RelativeSpec.openCover
Documentation

The covering by the literal spectra of the affine section algebras.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
Lean source · statement
def openCover (α : X.sheaf ⟶ A) [(underlyingModule α).IsQuasicoherent] :
    (scheme α).OpenCover
instance

openCover_isOpenImmersion

L142 ↗
AlgebraicGeometry.Scheme.RelativeSpec.openCover_isOpenImmersion
Documentation

The covering morphisms retain their native open-immersion proofs.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
Lean source · statement
instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U)
theorem

openCover_toBase

L149 ↗
AlgebraicGeometry.Scheme.RelativeSpec.openCover_toBase
Documentation

Each affine model maps to the base by the given structure homomorphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem openCover_toBase (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    (openCover α).f U ≫ toBase α =
      Spec.map (α.hom.app (op U.1)) ≫ U.2.fromSpec
theorem

toBase_preimage

L163 ↗
AlgebraicGeometry.Scheme.RelativeSpec.toBase_preimage
Documentation

The affine models are precisely the inverse images of the corresponding affine opens of the base.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem toBase_preimage (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    toBase α ⁻¹ᵁ U.1 = ((openCover α).f U).opensRange
def

affineModelIso

L173 ↗
AlgebraicGeometry.Scheme.RelativeSpec.affineModelIso
Documentation

The preimage of an affine open is the spectrum of its actual algebra of sections. No affine representer is assumed as input.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
def affineModelIso (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    (toBase α ⁻¹ᵁ U.1).toScheme ≅ Spec (A.obj.obj (op U.1))
theorem

isPullback_affineModel

L187 ↗
AlgebraicGeometry.Scheme.RelativeSpec.isPullback_affineModel
Documentation

The affine model is a cartesian chart over the corresponding open of X.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem isPullback_affineModel (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsPullback (Spec.map (α.hom.app (op U.1)) ≫ U.2.isoSpec.inv)
      ((openCover α).f U) U.1.ι (toBase α)
theorem

restriction_openCover

L196 ↗
AlgebraicGeometry.Scheme.RelativeSpec.restriction_openCover
Documentation

Restriction of algebra sections induces the actual transition map between the affine charts of the glued relative spectrum.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem restriction_openCover (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent]
    {U V : X.AffineZariskiSite} (i : U ⟶ V) :
    Spec.map (A.obj.map ((AffineZariskiSite.toOpensFunctor X).map i).op) ≫
      (openCover α).f V = (openCover α).f U
theorem

isOpenImmersion_restriction

L205 ↗
AlgebraicGeometry.Scheme.RelativeSpec.isOpenImmersion_restriction
Documentation

A restriction of algebra sections is an open immersion on the actual spectra. This is the map used in the gluing diagram.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem isOpenImmersion_restriction (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent]
    {U V : X.AffineZariskiSite} (i : U ⟶ V) :
    IsOpenImmersion
      (Spec.map (A.obj.map ((AffineZariskiSite.toOpensFunctor X).map i).op))
theorem

restriction_opensRange

L213 ↗
AlgebraicGeometry.Scheme.RelativeSpec.restriction_opensRange
Documentation

The transition over a basic open has exactly the expected basic-open image.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · full declaration
theorem restriction_opensRange (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent]
    (U : X.AffineZariskiSite) (f : Γ(X, U.1)) :
    let : IsOpenImmersion (Spec.map (A.obj.map (homOfLE (X.basicOpen_le f)).op)) :=
      isOpenImmersion_restriction α (homOfLE (U.basicOpen_le f))
    (Spec.map (A.obj.map (homOfLE (X.basicOpen_le f)).op)).opensRange =
      PrimeSpectrum.basicOpen (α.hom.app (op U.1) f) :=
  AffineZariskiSite.opensRange_relativeGluingData_map
    ((AffineZariskiSite.toOpensFunctor X).op ⋙ A.obj)
    (Functor.whiskerLeft (AffineZariskiSite.toOpensFunctor X).op α.hom)
    (coequifibered α) f
theorem

affineModelIso_toBase

L227 ↗
AlgebraicGeometry.Scheme.RelativeSpec.affineModelIso_toBase
Documentation

The explicit affine isomorphism respects the structure maps.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem affineModelIso_toBase (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    (affineModelIso α U).hom ≫ Spec.map (α.hom.app (op U.1)) =
      (toBase α ∣_ U.1) ≫ U.2.isoSpec.hom
theorem

isFinite_toBase

L260 ↗
AlgebraicGeometry.Scheme.RelativeSpec.isFinite_toBase
Documentation

The constructed relative spectrum is finite over X when the affine section algebras are finite over their structure rings.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry.Scheme.RelativeSpec
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
/-- The named gluing diagram uses the native locally directed colimit construction. -/
local instance gluingData_isLocallyDirected (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] :
    ((gluingData α).functor ⋙ Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (gluingData α)
/-- The covering morphisms retain their native open-immersion proofs. -/
local instance openCover_isOpenImmersion (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent] (U : X.AffineZariskiSite) :
    IsOpenImmersion ((openCover α).f U) :=
  (openCover α).map_prop U
Lean source · statement
theorem isFinite_toBase (α : X.sheaf ⟶ A)
    [(underlyingModule α).IsQuasicoherent]
    (hfinite : ∀ U : X.AffineZariskiSite, (α.hom.app (op U.1)).hom.Finite) :
    IsFinite (toBase α)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.