NYLL
Module

FiniteFaithfullyFlat.lean

Nyll.AlgebraicCurves.Geometry.Descent.FiniteFaithfullyFlat
2 declarations indexed from sourceView source ↗

Module documentation

Effective descent along finite faithfully flat covers

The quotient of the actual finite locally free equivalence relation associated with a covering action supplies its descended scheme. Finite presentation is sufficient; no separability of the covering algebra is needed. In particular this applies to arbitrary finite field extensions, including purely inseparable ones.

Imports8
Imported by2

Declarations

theorem

effective_of_finite_faithfullyFlat

L43 ↗
AlgebraicGeometry.DescentAction.effective_of_finite_faithfullyFlat
Documentation

A descent action over a finite, finitely presented, faithfully flat algebra is effective when every finite set of points of its source has an affine neighborhood.

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.DescentAction
Lean source · statement
theorem effective_of_finite_faithfullyFlat
    (R : Type u) [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R'] [Module.Finite R R']
    [Algebra.FinitePresentation R R'] [Module.FaithfullyFlat R R']
    {X' : Scheme.{u}} {x' : X' ⟶ Spec (CommRingCat.of R')}
    (A : DescentAction (Spec.map (CommRingCat.ofHom (algebraMap R R'))) x')
    (haff : ∀ S : Finset X', ∃ U : X'.Opens, IsAffineOpen U ∧ ∀ x ∈ S, x ∈ U) :
    A.Effective
theorem

effective_of_finite_fieldExtension

L95 ↗
AlgebraicGeometry.DescentAction.effective_of_finite_fieldExtension
Documentation

Effective descent along any finite field extension. Finite presentation follows from finite generation over the Noetherian base field, and faithful flatness from the nonzero vector-space structure of the extension.

Source context 3 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.DescentAction
Lean source · statement
theorem effective_of_finite_fieldExtension
    (K L : Type u) [Field K] [Field L] [Algebra K L] [Module.Finite K L]
    {X' : Scheme.{u}} {x' : X' ⟶ Spec (CommRingCat.of L)}
    (A : DescentAction (Spec.map (CommRingCat.ofHom (algebraMap K L))) x')
    (haff : ∀ S : Finset X', ∃ U : X'.Opens, IsAffineOpen U ∧ ∀ x ∈ S, x ∈ U) :
    A.Effective

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