NYLL
Module

smoothOfRelativeDimension_of_finrank_cotangentSpace_eq.lean

Nyll.AlgebraicCurves.Geometry.Deformation.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
5 declarations indexed from sourceView source ↗

Module documentation

smooth Of Relative Dimension of finrank cotangent Space eq

Imports1
Imported by3

Declarations

theorem

finrank_cotangentSpace_eq_of_isLocalization

L30 ↗
AlgebraicCurves.Geometry.Deformation.Proofs.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq.P2mRelDim.finrank_cotangentSpace_eq_of_isLocalization
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite TensorProduct
universe u
namespace P2mRelDim
Lean source · statement
theorem finrank_cotangentSpace_eq_of_isLocalization
    {R A S : Type u} [CommRing R] [CommRing A] [CommRing S] [IsLocalRing S]
    [Algebra R A] [Algebra A S] [Algebra R S] [IsScalarTower R A S]
    (M : Submonoid A) [IsLocalization M S] [Nontrivial A]
    (m : ℕ) [Algebra.IsStandardSmoothOfRelativeDimension m R A]
    (hres : Function.Bijective (algebraMap R (IsLocalRing.ResidueField S))) :
    Module.finrank (IsLocalRing.ResidueField S) (IsLocalRing.CotangentSpace S) = m
theorem

surjective_residueFieldMap_of_section

L72 ↗
AlgebraicCurves.Geometry.Deformation.Proofs.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq.P2mRelDim.surjective_residueFieldMap_of_section
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite TensorProduct
universe u
namespace P2mRelDim
Lean source · statement
theorem surjective_residueFieldMap_of_section {X Y : Scheme.{u}} (f : X ⟶ Y) (z : Y ⟶ X)
    (hz : z ≫ f = 𝟙 Y) (y : Y) :
    Function.Surjective (f.residueFieldMap (z.base y))
theorem

surjective_evaluation_top_Spec_field

L92 ↗
AlgebraicCurves.Geometry.Deformation.Proofs.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq.P2mRelDim.surjective_evaluation_top_Spec_field
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite TensorProduct
universe u
namespace P2mRelDim
Lean source · statement
theorem surjective_evaluation_top_Spec_field (K : Type u) [Field K] (y : Spec (CommRingCat.of K)) :
    Function.Surjective ((Spec (CommRingCat.of K)).evaluation ⊤ y trivial)
theorem

main

L111 ↗
AlgebraicCurves.Geometry.Deformation.Proofs.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq.P2mRelDim.main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite TensorProduct
universe u
namespace P2mRelDim
Lean source · statement
theorem main {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))
    [Smooth f] [IrreducibleSpace X]
    (z : Spec (CommRingCat.of K) ⟶ X) (hz : z ≫ f = 𝟙 (Spec (CommRingCat.of K))) (n : ℕ)
    (hn : Module.finrank
        (IsLocalRing.ResidueField (X.presheaf.stalk (z.base (IsLocalRing.closedPoint K))))
        (IsLocalRing.CotangentSpace (X.presheaf.stalk (z.base (IsLocalRing.closedPoint K)))) = n) :
    SmoothOfRelativeDimension n f
theorem

smoothOfRelativeDimension_of_finrank_cotangentSpace_eq

L191 ↗
AlgebraicGeometry.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Deformation.Proofs
namespace smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
open CategoryTheory AlgebraicGeometry TopologicalSpace Opposite TensorProduct
universe u
Lean source · statement
theorem _root_.AlgebraicGeometry.smoothOfRelativeDimension_of_finrank_cotangentSpace_eq
    {K : Type u} [Field K] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of K))
    [Smooth f] [IrreducibleSpace X]
    (z : Spec (CommRingCat.of K) ⟶ X) (hz : z ≫ f = 𝟙 (Spec (CommRingCat.of K))) (n : ℕ)
    (hn : Module.finrank
        (IsLocalRing.ResidueField (X.presheaf.stalk (z.base (IsLocalRing.closedPoint K))))
        (IsLocalRing.CotangentSpace (X.presheaf.stalk (z.base (IsLocalRing.closedPoint K)))) = n) :
    SmoothOfRelativeDimension n f

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