Module

exists_section_comp_eq_of_smooth_of_henselianLocalRing.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_section_comp_eq_of_smooth_of_henselianLocalRing

2 declarations indexed from sourceView source ↗

Module documentation

exists section comp eq of smooth of henselian Local Ring

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.Ideal.Quotient.Operations
Nyll.AlgebraicCurves.Geometry.Schemes.exists_etale_nhd_section_of_smooth
Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_algHom_lift_of_etale

Imported by1

Nyll.AlgebraicCurves.Geometry.Schemes.All

theorem

main

L35 ↗

AlgebraicCurves.Geometry.Schemes.Proofs.exists_section_comp_eq_of_smooth_of_henselianLocalRing.HensSection.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_section_comp_eq_of_smooth_of_henselianLocalRing
universe u
namespace HensSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry IsLocalRing

Lean source · statement

theorem main
    {R : Type u} [CommRing R] [HenselianLocalRing 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))) :
    ∃ σ : Spec (CommRingCat.of R) ⟶ U, σ ≫ f = 𝟙 _ ∧
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)) ≫ σ = x

theorem

exists_section_comp_eq_of_smooth_of_henselianLocalRing

L89 ↗

AlgebraicGeometry.exists_section_comp_eq_of_smooth_of_henselianLocalRing

Source context 5 commands