Module

SmoothOfClosedPoints.lean

Nyll.AlgebraicCurves.Geometry.Schemes.SmoothOfClosedPoints

11 declarations indexed from sourceView source ↗

Module documentation

Smooth Of Closed Points

Imports1

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

bijective_algebraMap_quotient

L30 ↗

SmoothOfClosedPoints.bijective_algebraMap_quotient

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Nullstellensatz
variable (k : Type*) {S : Type*} [Field k] [IsAlgClosed k] [CommRing S] [Algebra k S]
  [Algebra.FiniteType k S] (m : Ideal S) [m.IsMaximal]

Lean source · statement

theorem bijective_algebraMap_quotient : Function.Bijective (algebraMap k (S ⧸ m))

theorem

mem_sq_of_algebraMap_mem_sq

L48 ↗

SmoothOfClosedPoints.mem_sq_of_algebraMap_mem_sq

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

theorem mem_sq_of_algebraMap_mem_sq [hm : m.IsMaximal] (hg : g ∉ m) {x : S}
    (hx : algebraMap S T x ∈ Ideal.map (algebraMap S T) m ^ 2) : x ∈ m ^ 2

theorem

comap_map_eq

L71 ↗

SmoothOfClosedPoints.comap_map_eq

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

theorem comap_map_eq [hm : m.IsMaximal] (hg : g ∉ m) : (Ideal.map (algebraMap S T) m).comap
  (algebraMap S T) = m

theorem

exists_sub_algebraMap_mem

L76 ↗

SmoothOfClosedPoints.exists_sub_algebraMap_mem

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

theorem exists_sub_algebraMap_mem [hm : m.IsMaximal] (hg : g ∉ m)
    (hk : Function.Surjective (algebraMap k (S ⧸ m))) (t : T) :
    ∃ c : k, t - algebraMap k T c ∈ Ideal.map (algebraMap S T) m

def

mapCotangent

L112 ↗

SmoothOfClosedPoints.mapCotangent

Documentation

The map on cotangent spaces induced by the localization homomorphism.

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

def mapCotangent :
    m.Cotangent →ₗ[k] (Ideal.map (algebraMap S T) m).Cotangent

theorem

mapCotangent_toCotangent

L117 ↗

SmoothOfClosedPoints.mapCotangent_toCotangent

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

theorem mapCotangent_toCotangent (x : m) :
    mapCotangent (k := k) m T (m.toCotangent x)
      = (Ideal.map (algebraMap S T) m).toCotangent
          ⟨algebraMap S T x, Ideal.mem_map_of_mem (algebraMap S T) x.2⟩

theorem

mapCotangent_bijective

L123 ↗

SmoothOfClosedPoints.mapCotangent_bijective

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

theorem mapCotangent_bijective [hm : m.IsMaximal] (hg : g ∉ m)
    (hk : Function.Surjective (algebraMap k (S ⧸ m))) :
    Function.Bijective (mapCotangent (k := k) m T)

def

mapCotangentEquiv

L156 ↗

SmoothOfClosedPoints.mapCotangentEquiv

Documentation

The cotangent space equivalence for localization away from the maximal ideal.

Source context 5 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Localization
variable {k : Type*} {S : Type*} [Field k] [CommRing S] [Algebra k S]
  (m : Ideal S) {g : S}
  (T : Type*) [CommRing T] [Algebra S T] [Algebra k T] [IsScalarTower k S T]
  [IsLocalization.Away g T]

Lean source · statement

def mapCotangentEquiv [m.IsMaximal] (hg : g ∉ m)
    (hk : Function.Surjective (algebraMap k (S ⧸ m))) :
    m.Cotangent ≃ₗ[k] (Ideal.map (algebraMap S T) m).Cotangent

theorem

finrank_cotangent_ker_eq

L170 ↗

SmoothOfClosedPoints.finrank_cotangent_ker_eq

Source context 6 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints
section Conormal
variable {k : Type*} [Field k] {T : Type*} [CommRing T] [Algebra k T]
  {κ : Type*} [Field κ] [Algebra k κ] (ψ : T →ₐ[k] κ) (hψ : Function.Surjective ψ)
  (hk : Function.Bijective (algebraMap k κ))
include hψ hk in

Lean source · statement

theorem finrank_cotangent_ker_eq [Nontrivial T] [Algebra.FormallySmooth k T]
    [Module.Free T Ω[T⁄k]] [Module.Finite T Ω[T⁄k]] :
    Module.finrank k (RingHom.ker (ψ : T →+* κ)).Cotangent = Module.finrank T Ω[T⁄k]

theorem

exists_isStandardSmoothOfRelativeDimension_of_formallySmooth

L207 ↗

SmoothOfClosedPoints.exists_isStandardSmoothOfRelativeDimension_of_formallySmooth

Source context 3 commands

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

universe u
open CategoryTheory
namespace SmoothOfClosedPoints

Lean source · statement

theorem exists_isStandardSmoothOfRelativeDimension_of_formallySmooth
    (k : Type u) (S : Type u) [Field k] [IsAlgClosed k] [CommRing S] [Algebra k S]
    [Algebra.FiniteType k S] (m : Ideal S) [hm : m.IsMaximal] (r : ℕ)
    (hfs : Algebra.FormallySmooth k (Localization.AtPrime m))
    (hr : Module.finrank k m.Cotangent = r) :
    ∃ g ∉ m, Algebra.IsStandardSmoothOfRelativeDimension r k (Localization.Away g)

theorem

of_forall_isClosed

L259 ↗

AlgebraicGeometry.SmoothOfRelativeDimension.of_forall_isClosed

Source context 3 commands

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

universe u
open CategoryTheory
namespace AlgebraicGeometry

Lean source · statement

theorem SmoothOfRelativeDimension.of_forall_isClosed
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} [CompactSpace X]
    (f : X ⟶ Spec (.of k)) (r : ℕ)
    (h : ∀ z : X, IsClosed ({z} : Set X) →
      ∃ (S : Type u) (_ : CommRing S) (_ : Algebra k S) (_ : Algebra.FiniteType k S)
        (ι : Spec (.of S) ⟶ X) (_ : IsOpenImmersion ι)
        (_ : ι ≫ f = Spec.map (CommRingCat.ofHom (algebraMap k S)))
        (p : PrimeSpectrum S), ι p = z ∧
          Algebra.FormallySmooth k (Localization.AtPrime p.asIdeal) ∧
          Module.finrank k p.asIdeal.Cotangent = r) :
    SmoothOfRelativeDimension r f

Module documentation

Smooth Of Closed Points

Declarations