NYLL
Module

exists_etale_of_formallyUnramified_stalkMap.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_etale_of_formallyUnramified_stalkMap
8 declarations indexed from sourceView source ↗

Module documentation

exists etale of formally Unramified stalk Map

Imports12
  • Mathlib.AlgebraicGeometry.Morphisms.Etale
  • Mathlib.AlgebraicGeometry.Morphisms.Smooth
  • Mathlib.AlgebraicGeometry.Stalk
  • Mathlib.RingTheory.Etale.Locus
  • Mathlib.RingTheory.Kaehler.JacobiZariski
  • Mathlib.RingTheory.Smooth.Basic
  • Mathlib.RingTheory.LocalRing.Module
  • Mathlib.RingTheory.LocalRing.ResidueField.Defs
  • Mathlib.RingTheory.OrzechProperty
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.Dimension.Free
  • Mathlib.Tactic.Algebraize
Imported by2

Declarations

def

cotangentEquivOfEq

L49 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.JacobianCriterionAux.cotangentEquivOfEq
Documentation

Transport of the cotangent space along equality of ideals.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace JacobianCriterionAux
section rank
variable {R B : Type*} [CommRing R] [CommRing B] [IsLocalRing B] [Algebra R B]
Lean source · statement
def cotangentEquivOfEq {S : Type*} [CommRing S] {I J : Ideal S} (h : I = J) :
    I.Cotangent ≃ₗ[S] J.Cotangent
theorem

finrank_kaehlerDifferential_eq_finrank_cotangentSpace

L52 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.JacobianCriterionAux.finrank_kaehlerDifferential_eq_finrank_cotangentSpace
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace JacobianCriterionAux
section rank
variable {R B : Type*} [CommRing R] [CommRing B] [IsLocalRing B] [Algebra R B]
Lean source · statement
theorem finrank_kaehlerDifferential_eq_finrank_cotangentSpace
    [Algebra.FormallySmooth R B] [Algebra.EssFiniteType R B]
    (hB : Function.Bijective (algebraMap R (ResidueField B))) :
    Module.finrank B Ω[B⁄R] = Module.finrank (ResidueField B) (CotangentSpace B)
theorem

bijective_algebraMap_residueField_of_section

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.JacobianCriterionAux.bijective_algebraMap_residueField_of_section
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace JacobianCriterionAux
section rank
variable {R B : Type*} [CommRing R] [CommRing B] [IsLocalRing B] [Algebra R B]
Lean source · statement
theorem bijective_algebraMap_residueField_of_section {R₀ : Type*} [CommRing R₀] [Nontrivial R₀]
    (hR : IsField R) (s : B →+* R₀) (hs : Function.Surjective (s.comp (algebraMap R B))) :
    Function.Bijective (algebraMap R (ResidueField B))
theorem

formallySmooth_of_formallyUnramified_of_finrank_eq

L116 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.JacobianCriterionAux.formallySmooth_of_formallyUnramified_of_finrank_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace JacobianCriterionAux
section core
variable {R A B : Type*} [CommRing R] [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
  [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
  [Algebra.FormallySmooth R A] [Algebra.FormallySmooth R B]
  [Algebra.EssFiniteType R A] [Algebra.EssFiniteType R B]
  [Algebra.FormallyUnramified A B]
Lean source · statement
theorem formallySmooth_of_formallyUnramified_of_finrank_eq
    (hA : Function.Bijective (algebraMap R (ResidueField A)))
    (hB : Function.Bijective (algebraMap R (ResidueField B)))
    (hdim : Module.finrank (ResidueField B) (CotangentSpace B) =
      Module.finrank (ResidueField A) (CotangentSpace A)) :
    Algebra.FormallySmooth A B
theorem

isField_stalk_Spec_of_field

L158 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.AlgebraicGeometry.isField_stalk_Spec_of_field
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits JacobianCriterionAux
Lean source · statement
theorem isField_stalk_Spec_of_field {K : Type u} [Field K] (p : ↥(Spec (.of K))) :
    IsField ((Spec (.of K)).presheaf.stalk p)
theorem

exists_etale_of_formallySmooth_of_formallyUnramified_stalkMap

L165 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.AlgebraicGeometry.exists_etale_of_formallySmooth_of_formallyUnramified_stalkMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits JacobianCriterionAux
Lean source · statement
theorem exists_etale_of_formallySmooth_of_formallyUnramified_stalkMap
    {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
    (U : Y.Opens) (hU : IsAffineOpen U) (V : X.Opens) (hV : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U)
    (hxV : x ∈ V) (hfp : (f.appLE U V hVU).hom.FinitePresentation)
    (H : (f.stalkMap x).hom.FormallySmooth) (H' : (f.stalkMap x).hom.FormallyUnramified) :
    ∃ W : X.Opens, x ∈ W ∧ Etale (W.ι ≫ f)
theorem

exists_etale_of_formallyUnramified_stalkMap_aux

L221 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap.AlgebraicGeometry.exists_etale_of_formallyUnramified_stalkMap_aux
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits JacobianCriterionAux
Lean source · statement
theorem exists_etale_of_formallyUnramified_stalkMap_aux
    {K : Type u} [Field K] {X Y : Scheme.{u}}
    (sX : X ⟶ Spec (.of K)) (sY : Y ⟶ Spec (.of K)) [Smooth sX] [Smooth sY]
    (f : X ⟶ Y) (hf : f ≫ sY = sX)
    (σ : Spec (.of K) ⟶ X) (hσ : σ ≫ sX = 𝟙 _)
    (hfu : (f.stalkMap (σ.base (IsLocalRing.closedPoint K))).hom.FormallyUnramified)
    (hdim : Module.finrank
        (IsLocalRing.ResidueField (X.presheaf.stalk (σ.base (IsLocalRing.closedPoint K))))
        (IsLocalRing.CotangentSpace (X.presheaf.stalk (σ.base (IsLocalRing.closedPoint K)))) =
      Module.finrank
        (IsLocalRing.ResidueField
          (Y.presheaf.stalk (f.base (σ.base (IsLocalRing.closedPoint K)))))
        (IsLocalRing.CotangentSpace
          (Y.presheaf.stalk (f.base (σ.base (IsLocalRing.closedPoint K)))))) :
    ∃ U : X.Opens, σ.base (IsLocalRing.closedPoint K) ∈ U ∧ Etale (U.ι ≫ f)
theorem

exists_etale_of_formallyUnramified_stalkMap

L313 ↗
AlgebraicGeometry.exists_etale_of_formallyUnramified_stalkMap
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_of_formallyUnramified_stalkMap
open _root_.AlgebraicGeometry
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
universe u
open TensorProduct IsLocalRing
Lean source · statement
theorem _root_.AlgebraicGeometry.exists_etale_of_formallyUnramified_stalkMap
    {K : Type u} [Field K] {X Y : Scheme.{u}}
    (sX : X ⟶ Spec (.of K)) (sY : Y ⟶ Spec (.of K)) [Smooth sX] [Smooth sY]
    (f : X ⟶ Y) (hf : f ≫ sY = sX)
    (σ : Spec (.of K) ⟶ X) (hσ : σ ≫ sX = 𝟙 _)
    (hfu : (f.stalkMap (σ.base (IsLocalRing.closedPoint K))).hom.FormallyUnramified)
    (hdim : Module.finrank
        (IsLocalRing.ResidueField (X.presheaf.stalk (σ.base (IsLocalRing.closedPoint K))))
        (IsLocalRing.CotangentSpace (X.presheaf.stalk (σ.base (IsLocalRing.closedPoint K)))) =
      Module.finrank
        (IsLocalRing.ResidueField
          (Y.presheaf.stalk (f.base (σ.base (IsLocalRing.closedPoint K)))))
        (IsLocalRing.CotangentSpace
          (Y.presheaf.stalk (f.base (σ.base (IsLocalRing.closedPoint K)))))) :
    ∃ U : X.Opens, σ.base (IsLocalRing.closedPoint K) ∈ U ∧ Etale (U.ι ≫ f)

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