Module

smoothOfRelativeDimension_of_irreducibleSpace.lean

Nyll.AlgebraicCurves.Geometry.Schemes.smoothOfRelativeDimension_of_irreducibleSpace

4 declarations indexed from sourceView source ↗

Module documentation

smooth Of Relative Dimension of irreducible Space

Imports7

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.Localization.Defs
Mathlib.RingTheory.Nilpotent.Lemmas
Mathlib.Topology.Irreducible
Mathlib.Tactic.Algebraize

Imported by3

theorem

eq_of_isStandardSmoothOfRelativeDimension

L37 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace.RelativeDimensionAgreement.eq_of_isStandardSmoothOfRelativeDimension

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
noncomputable section
namespace RelativeDimensionAgreement

Lean source · statement

theorem eq_of_isStandardSmoothOfRelativeDimension {R S : Type u} [CommRing R] [CommRing S]
    [Nontrivial S] {m n : ℕ} (f : R →+* S) (hm : f.IsStandardSmoothOfRelativeDimension m)
    (hn : f.IsStandardSmoothOfRelativeDimension n) : m = n

theorem

nontrivial_localization_away

L47 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace.RelativeDimensionAgreement.nontrivial_localization_away

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
noncomputable section
namespace RelativeDimensionAgreement

Lean source · statement

theorem nontrivial_localization_away {S : Type u} [CommRing S] {t : S} (ht : ¬IsNilpotent t) :
    Nontrivial (Localization.Away t)

theorem

exists_not_isNilpotent

L55 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace.RelativeDimensionAgreement.exists_not_isNilpotent

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
noncomputable section
namespace RelativeDimensionAgreement

Lean source · statement

theorem exists_not_isNilpotent {S : Type u} [CommRing S] [Nontrivial S] {s : Set S}
    (hs : Ideal.span s = ⊤) : ∃ t ∈ s, ¬IsNilpotent t

theorem

smoothOfRelativeDimension_of_irreducibleSpace

L68 ↗

AlgebraicGeometry.smoothOfRelativeDimension_of_irreducibleSpace

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.smoothOfRelativeDimension_of_irreducibleSpace
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpace
noncomputable section
open RelativeDimensionAgreement in

Lean source · statement

theorem _root_.AlgebraicGeometry.smoothOfRelativeDimension_of_irreducibleSpace (n : ℕ) {X Y :
  Scheme.{u}} (f : X ⟶ Y) [IrreducibleSpace X] [Smooth f]
    (V : X.Opens) (hV : (V : Set X).Nonempty) [SmoothOfRelativeDimension n (V.ι ≫ f)] :
    SmoothOfRelativeDimension n f

Module documentation

smooth Of Relative Dimension of irreducible Space

Declarations

eq_of_isStandardSmoothOfRelativeDimension

nontrivial_localization_away

exists_not_isNilpotent

smoothOfRelativeDimension_of_irreducibleSpace