Module

SmoothProperCurveBase.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurveBase

11 declarations indexed from sourceView source ↗

Module documentation

Scalar extensions of smooth proper curves, their sections and their basic fibre properties.

Imports5

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.Fiber
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver

Imported by128

instance

smooth_one

L31 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry

Lean source · statement

instance SmoothOfRelativeDimension.smooth_one {X S : Scheme.{u}} (f : X ⟶ S)
    [SmoothOfRelativeDimension 1 f] : Smooth f

instance

pullback_snd

L35 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry

Lean source · statement

instance SmoothOfRelativeDimension.pullback_snd (n : ℕ) {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
    [SmoothOfRelativeDimension n f] : SmoothOfRelativeDimension n (pullback.snd f g)

instance

pullback_fst

L42 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry

Lean source · statement

instance SmoothOfRelativeDimension.pullback_fst (n : ℕ) {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S)
    [SmoothOfRelativeDimension n g] : SmoothOfRelativeDimension n (pullback.fst f g)

instance

fiberToSpecResidueField

L49 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry

Lean source · statement

instance SmoothOfRelativeDimension.fiberToSpecResidueField (n : ℕ) {X S : Scheme.{u}} (f : X ⟶ S)
    [SmoothOfRelativeDimension n f] (s : S) :
    SmoothOfRelativeDimension n (f.fiberToSpecResidueField s)

instance

fiberToSpecResidueField

L58 ↗

AlgebraicGeometry.IsProper.fiberToSpecResidueField

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry

Lean source · statement

instance IsProper.fiberToSpecResidueField {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] (s : S) :
    IsProper (f.fiberToSpecResidueField s)

abbrev

specMap

L74 ↗

AlgebraicGeometry.SmoothProperCurve.specMap

Documentation

The spectrum map induced by the scalar extension.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry
namespace SmoothProperCurve
variable (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
section BaseChange
variable (T : Type u) [CommRing T] [Algebra R T]

Lean source · statement

abbrev specMap : Spec (CommRingCat.of T) ⟶ Spec (CommRingCat.of R)

abbrev

baseChange

L78 ↗

AlgebraicGeometry.SmoothProperCurve.baseChange

Documentation

The pullback curve along the spectrum map of a scalar extension.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry
namespace SmoothProperCurve
variable (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
section BaseChange
variable (T : Type u) [CommRing T] [Algebra R T]

Lean source · statement

abbrev baseChange : pullback c (specMap R T) ⟶ Spec (CommRingCat.of T)

def

sectionBaseChange

L89 ↗

AlgebraicGeometry.SmoothProperCurve.sectionBaseChange

Documentation

The section of the scalar-extension pullback induced by the original section.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry
namespace SmoothProperCurve
variable (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
section BaseChange
variable (T : Type u) [CommRing T] [Algebra R T]
variable {R c}

Lean source · statement

def sectionBaseChange (ε : SchemeHomOver (𝟙 _) c) : SchemeHomOver (𝟙 _) (baseChange R c T)

theorem

sectionBaseChange_coe_fst

L93 ↗

AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry
namespace SmoothProperCurve
variable (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
section BaseChange
variable (T : Type u) [CommRing T] [Algebra R T]
variable {R c}

Lean source · statement

theorem sectionBaseChange_coe_fst (ε : SchemeHomOver (𝟙 _) c) :
    (sectionBaseChange T ε).1 ≫ pullback.fst c (specMap R T) = specMap R T ≫ ε.1

theorem

sectionBaseChange_coe_snd

L97 ↗

AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry
namespace SmoothProperCurve
variable (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))
section BaseChange
variable (T : Type u) [CommRing T] [Algebra R T]
variable {R c}

Lean source · statement

theorem sectionBaseChange_coe_snd (ε : SchemeHomOver (𝟙 _) c) :
    (sectionBaseChange T ε).1 ≫ pullback.snd c (specMap R T) = 𝟙 _

instance

isIntegral_pullback_Spec_field

L103 ↗

AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits NeronModelInfra
universe u
namespace AlgebraicGeometry
namespace SmoothProperCurve
variable (R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (.of R))

Lean source · statement

instance isIntegral_pullback_Spec_field [GeometricallyIntegral c] {K : Type u} [Field K]
    (ξ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of R)) : IsIntegral (pullback c ξ)

Module documentation

Declarations