Module

GeneratedFiniteAlgebra.lean

Nyll.SchemeTheory.Modules.GeneratedFiniteAlgebra

4 declarations indexed from sourceView source ↗

Module documentation

A finite relative scheme generated by a finite quasicoherent submodule

The section algebra is generated inside the given integral ambient algebra. Finitely generated module sections therefore give finite section algebras. The native cartesian affine charts of the previously constructed gluing then prove finiteness of its actual structure morphism.

Imports5

Nyll.SchemeTheory.Modules.GeneratedAlgebraLocalization
Nyll.SchemeTheory.RingTheory.SubmoduleAdjoinLocalization
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Mathlib.RingTheory.RingHom.Finite

Imported by2

theorem

finite_codRestrict_of_eq

L30 ↗

AlgebraicGeometry.Scheme.GeneratedAlgebra.finite_codRestrict_of_eq

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra

Lean source · statement

theorem finite_codRestrict_of_eq
    {R B : Type u} [CommRing R] [CommRing B] (ι : R →+* B)
    (C C' : Subring B) (hC : C = C')
    (hι : ∀ r, ι r ∈ C) (hι' : ∀ r, ι r ∈ C')
    (hfinite : (ι.codRestrict C' hι').Finite) :
    (ι.codRestrict C hι).Finite

theorem

isFinite_comp_iso

L39 ↗

AlgebraicGeometry.Scheme.GeneratedAlgebra.isFinite_comp_iso

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra

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)

theorem

finite_structureMap

L51 ↗

AlgebraicGeometry.Scheme.GeneratedAlgebra.finite_structureMap

Documentation

Finite module generators inside the actual integral section algebra produce a finite structure map to the generated section ring.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule α))

Lean source · statement

theorem finite_structureMap (U : X.AffineZariskiSite)
    (hIntegral : (α.hom.app (op U.1)).hom.IsIntegral)
    (hFinite : (N.toSubmodule.obj (op U.1)).FG) :
    ((structureMap α N.toSubmodule).app (op U.1)).hom.Finite

theorem

isFinite_toBase

L79 ↗

AlgebraicGeometry.Scheme.GeneratedAlgebra.isFinite_toBase

Documentation

The actual glued relative scheme generated by a finite quasicoherent submodule of an integral algebra is finite over the original base.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule α))
variable [(RelativeSpec.underlyingModule α).IsQuasicoherent]
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]

Lean source · statement

theorem isFinite_toBase
    (hIntegral : ∀ U : X.AffineZariskiSite, (α.hom.app (op U.1)).hom.IsIntegral)
    (hFinite : ∀ U : X.AffineZariskiSite, (N.toSubmodule.obj (op U.1)).FG) :
    IsFinite (toBase α N)

Module documentation

A finite relative scheme generated by a finite quasicoherent submodule

Declarations

finite_codRestrict_of_eq

isFinite_comp_iso

finite_structureMap

isFinite_toBase