Module

Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing

3 declarations indexed from sourceView source ↗

Module documentation

Smooth exists comp eq id and spec Map comp eq of henselian Local Ring

Imports3

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.LocalRing.ResidueField.Defs
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_exists_algHom_lift_of_isSmoothAt

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

exists_lift_of_smooth

L35 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing.HenselSmoothSection.exists_lift_of_smooth

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing
universe u
open IsLocalRing CategoryTheory AlgebraicGeometry
namespace HenselSmoothSection
variable {R : Type u} [CommRing R] [HenselianLocalRing R]

Lean source · statement

theorem exists_lift_of_smooth
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Smooth R S]
    (φ : S →ₐ[R] ResidueField R) :
    ∃ ψ : S →ₐ[R] R, ∀ s, algebraMap R (ResidueField R) (ψ s) = φ s

theorem

exists_section

L42 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing.HenselSmoothSection.exists_section

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing
universe u
open IsLocalRing CategoryTheory AlgebraicGeometry
namespace HenselSmoothSection
variable {R : Type u} [CommRing R] [HenselianLocalRing R]

Lean source · statement

theorem exists_section {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of R)) [Smooth f]
    (x₀ : Spec (CommRingCat.of (ResidueField R)) ⟶ X)
    (hx₀ : x₀ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R (ResidueField R)))) :
    ∃ s : Spec (CommRingCat.of R) ⟶ X, s ≫ f = 𝟙 _ ∧
      Spec.map (CommRingCat.ofHom (algebraMap R (ResidueField R))) ≫ s = x₀

theorem

exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing

L96 ↗

AlgebraicGeometry.Smooth.exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Smooth_exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing
universe u
open IsLocalRing CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Smooth.exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing
    {R : Type u} [CommRing R] [HenselianLocalRing R] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of R)) [Smooth f]
    (x₀ : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) ⟶ X)
    (hx₀ : x₀ ≫ f =
      Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R)))) :
    ∃ s : Spec (CommRingCat.of R) ⟶ X, s ≫ f = 𝟙 _ ∧
      Spec.map (CommRingCat.ofHom (algebraMap R (IsLocalRing.ResidueField R))) ≫ s = x₀

Module documentation

Smooth exists comp eq id and spec Map comp eq of henselian Local Ring

Declarations

exists_lift_of_smooth

exists_section

exists_comp_eq_id_and_specMap_comp_eq_of_henselianLocalRing