Module

exists_etale_nhd_section_of_smooth.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_etale_nhd_section_of_smooth

3 declarations indexed from sourceView source ↗

Module documentation

exists etale nhd section of smooth

Imports17

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.RingTheory.RingHom.Smooth
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.Smooth.StandardSmoothOfFree
Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.Algebra.MvPolynomial.Basic
Mathlib.RingTheory.TensorProduct.Maps
Mathlib.Tactic.Choose
Batteries.Tactic.Init
Mathlib.Tactic.Set

Imported by2

theorem

exists_etale_of_smooth_of_algHom_residueField

L47 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_nhd_section_of_smooth.EtaleNhd.exists_etale_of_smooth_of_algHom_residueField

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_nhd_section_of_smooth
universe u
open scoped TensorProduct
namespace EtaleNhd
open IsLocalRing

Lean source · statement

theorem exists_etale_of_smooth_of_algHom_residueField
    {R : Type u} [CommRing R] [IsLocalRing R] {B : Type u} [CommRing B] [Algebra R B]
      [Algebra.Smooth R B]
    (ψ : B →ₐ[R] ResidueField R) :
    ∃ (E : Type u) (_ : CommRing E) (_ : Algebra R E) (_ : Algebra.Etale R E) (𝔫 : Ideal E) (_ :
      𝔫.IsMaximal)
      (h𝔫 : maximalIdeal R ≤ 𝔫.comap (algebraMap R E)) (_ : ∀ e : E, ∃ r : R, e - algebraMap R E r
        ∈ 𝔫)
      (β : B →ₐ[R] E),
      (Ideal.Quotient.mk 𝔫).comp β.toRingHom = (Ideal.quotientMap 𝔫 (algebraMap R E) h𝔫).comp
        ψ.toRingHom

theorem

main

L172 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_nhd_section_of_smooth.EtaleNhd.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_nhd_section_of_smooth
universe u
open scoped TensorProduct
namespace EtaleNhd
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing

Lean source · statement

theorem main
    {R : Type u} [CommRing R] [IsLocalRing R]
    {U : Scheme.{u}} (f : U ⟶ Spec (CommRingCat.of R)) [Smooth f]
    (x : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) ⟶ U)
    (hx : x ≫ f = Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) :
    ∃ (E : Type u) (_ : CommRing E) (_ : Algebra R E) (_ : Algebra.Etale R E) (𝔫 : Ideal E) (_ :
      𝔫.IsMaximal)
      (h𝔫 : IsLocalRing.maximalIdeal R ≤ 𝔫.comap (algebraMap R E))
      (_ : ∀ e : E, ∃ r : R, e - algebraMap R E r ∈ 𝔫)
      (τ : Spec (CommRingCat.of E) ⟶ U),
      τ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R E)) ∧
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk 𝔫)) ≫ τ =
        Spec.map (CommRingCat.ofHom (Ideal.quotientMap 𝔫 (algebraMap R E) h𝔫)) ≫ x

theorem

exists_etale_nhd_section_of_smooth

L240 ↗

AlgebraicGeometry.exists_etale_nhd_section_of_smooth

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.exists_etale_nhd_section_of_smooth
universe u
open scoped TensorProduct
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.exists_etale_nhd_section_of_smooth
    {R : Type u} [CommRing R] [IsLocalRing R]
    {U : Scheme.{u}} (f : U ⟶ Spec (CommRingCat.of R)) [Smooth f]
    (x : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) ⟶ U)
    (hx : x ≫ f = Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))) :
    ∃ (E : Type u) (_ : CommRing E) (_ : Algebra R E) (_ : Algebra.Etale R E) (𝔫 : Ideal E) (_ :
      𝔫.IsMaximal)
      (h𝔫 : IsLocalRing.maximalIdeal R ≤ 𝔫.comap (algebraMap R E))
      (_ : ∀ e : E, ∃ r : R, e - algebraMap R E r ∈ 𝔫)
      (τ : Spec (CommRingCat.of E) ⟶ U),
      τ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R E)) ∧
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk 𝔫)) ≫ τ =
        Spec.map (CommRingCat.ofHom (Ideal.quotientMap 𝔫 (algebraMap R E) h𝔫)) ≫ x

Module documentation

exists etale nhd section of smooth

Declarations

exists_etale_of_smooth_of_algHom_residueField

main

exists_etale_nhd_section_of_smooth