Module

Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace

5 declarations indexed from sourceView source ↗

Module documentation

Smooth exists smooth Of Relative Dimension of preconnected Space

Imports4

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.Tactic.Algebraize

Imported by2

theorem

appLE_basicOpen_basicOpen

L37 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace.R1NeronObjE7.appLE_basicOpen_basicOpen

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom
section descend
variable {P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}

Lean source · statement

theorem appLE_basicOpen_basicOpen
    (hPa : StableUnderCompositionWithLocalizationAwayTarget P) (hPl : LocalizationAwayPreserves P)
    {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.affineOpens) (V : X.affineOpens)
    (e : V.1 ≤ f ⁻¹ᵁ U.1) (h : P (f.appLE U V e).hom)
    (r : Γ(Y, U)) (s : Γ(X, X.basicOpen (f.appLE U V e r)))
    (e' : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r) :
    P (f.appLE (Y.basicOpen r) (X.basicOpen s) e').hom

theorem

eq_of_isStandardSmoothOfRelativeDimension_appLE

L62 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace.R1NeronObjE7.eq_of_isStandardSmoothOfRelativeDimension_appLE

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom

Lean source · statement

theorem eq_of_isStandardSmoothOfRelativeDimension_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (x : X)
    {n n' : ℕ}
    (U : Y.affineOpens) (V : X.affineOpens) (hx : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1)
    (h : (f.appLE U V e).hom.IsStandardSmoothOfRelativeDimension n)
    (U' : Y.affineOpens) (V' : X.affineOpens) (hx' : x ∈ V'.1) (e' : V'.1 ≤ f ⁻¹ᵁ U'.1)
    (h' : (f.appLE U' V' e').hom.IsStandardSmoothOfRelativeDimension n') : n = n'

theorem

exists_chart

L106 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace.R1NeronObjE7.exists_chart

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom

Lean source · statement

theorem exists_chart {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] (x : X) :
    ∃ (n : ℕ) (U : Y.affineOpens) (V : X.affineOpens) (_ : x ∈ V.1) (e : V.1 ≤ f ⁻¹ᵁ U.1),
      (f.appLE U V e).hom.IsStandardSmoothOfRelativeDimension n

theorem

exists_smoothOfRelativeDimension_of_preconnectedSpace

L114 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace.R1NeronObjE7.exists_smoothOfRelativeDimension_of_preconnectedSpace

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace
universe u
namespace R1NeronObjE7
open AlgebraicGeometry CategoryTheory RingHom

Lean source · statement

theorem exists_smoothOfRelativeDimension_of_preconnectedSpace {X Y : Scheme.{u}} (f : X ⟶ Y)
    [Smooth f] [PreconnectedSpace X] : ∃ n : ℕ, SmoothOfRelativeDimension n f

theorem

exists_smoothOfRelativeDimension_of_preconnectedSpace

L144 ↗

AlgebraicGeometry.Smooth.exists_smoothOfRelativeDimension_of_preconnectedSpace

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_smoothOfRelativeDimension_of_preconnectedSpace
universe u
open AlgebraicGeometry CategoryTheory in

Lean source · statement

theorem _root_.AlgebraicGeometry.Smooth.exists_smoothOfRelativeDimension_of_preconnectedSpace
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Smooth f] [PreconnectedSpace X] :
    ∃ n : ℕ, SmoothOfRelativeDimension n f

Module documentation

Smooth exists smooth Of Relative Dimension of preconnected Space

Declarations

appLE_basicOpen_basicOpen

eq_of_isStandardSmoothOfRelativeDimension_appLE

exists_chart

exists_smoothOfRelativeDimension_of_preconnectedSpace

exists_smoothOfRelativeDimension_of_preconnectedSpace