Module

HenselianLocalRing_exists_algHom_lift_of_etale.lean

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_algHom_lift_of_etale

4 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring exists alg Hom lift of etale

Imports2

Mathlib.RingTheory.Henselian
Mathlib.RingTheory.Unramified.LocalStructure

Imported by5

theorem

standardEtalePair_residueSection_exists

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_algHom_lift_of_etale.W2Port.standardEtalePair_residueSection_exists

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_etale
universe u
open Polynomial IsLocalRing
namespace W2Port
section StandardEtalePairSections
variable {R : Type u} [CommRing R] [HenselianLocalRing R]

Lean source · statement

theorem standardEtalePair_residueSection_exists
    (P : StandardEtalePair R) (φ : P.Ring →ₐ[R] ResidueField R) :
    ∃ ret : P.Ring →ₐ[R] R,
      ∀ s : P.Ring, algebraMap R (ResidueField R) (ret s) = φ s

theorem

isStandardEtale_residueSection_exists

L81 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_algHom_lift_of_etale.W2Port.isStandardEtale_residueSection_exists

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_etale
universe u
open Polynomial IsLocalRing
namespace W2Port
section IsStandardEtaleSections
variable {R : Type u} [CommRing R] [HenselianLocalRing R]

Lean source · statement

theorem isStandardEtale_residueSection_exists
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.IsStandardEtale R S]
    (φ : S →ₐ[R] ResidueField R) :
    ∃ ret : S →ₐ[R] R, ∀ s : S, algebraMap R (ResidueField R) (ret s) = φ s

theorem

etale_residueSection_exists_of_henselianLocalRing

L98 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_algHom_lift_of_etale.W2Port.etale_residueSection_exists_of_henselianLocalRing

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_etale
universe u
open Polynomial IsLocalRing
namespace W2Port
section Gluing
variable {R : Type u} [CommRing R] [HenselianLocalRing R]

Lean source · statement

theorem etale_residueSection_exists_of_henselianLocalRing
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Etale R S]
    (φ : S →ₐ[R] ResidueField R) :
    ∃ ret : S →ₐ[R] R, ∀ s : S, algebraMap R (ResidueField R) (ret s) = φ s

theorem

exists_algHom_lift_of_etale

L130 ↗

HenselianLocalRing.exists_algHom_lift_of_etale

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_etale
universe u
open Polynomial IsLocalRing

Lean source · statement

theorem _root_.HenselianLocalRing.exists_algHom_lift_of_etale
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Etale R S]
    (φ : S →ₐ[R] IsLocalRing.ResidueField R) :
    ∃ ψ : S →ₐ[R] R, ∀ s : S, algebraMap R (IsLocalRing.ResidueField R) (ψ s) = φ s

Module documentation

Henselian Local Ring exists alg Hom lift of etale

Declarations

standardEtalePair_residueSection_exists

isStandardEtale_residueSection_exists

etale_residueSection_exists_of_henselianLocalRing

exists_algHom_lift_of_etale