NYLL
Module

HenselianLocalRing_exists_algHom_lift_of_isSmoothAt.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_exists_algHom_lift_of_isSmoothAt
4 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring exists alg Hom lift of is Smooth At

Imports1
Imported by4

Declarations

theorem

exists_lift_of_isStandardEtale_mvPolynomial

L32 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_algHom_lift_of_isSmoothAt.HenselSmoothLift.exists_lift_of_isStandardEtale_mvPolynomial
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_isSmoothAt
universe u
open IsLocalRing TensorProduct
namespace HenselSmoothLift
variable {R : Type u} [CommRing R] [HenselianLocalRing R]
Lean source · statement
theorem exists_lift_of_isStandardEtale_mvPolynomial
    {n : ℕ} (A : Type u) [CommRing A] [Algebra R A]
    [Algebra (MvPolynomial (Fin n) R) A] [IsScalarTower R (MvPolynomial (Fin n) R) A]
    [Algebra.IsStandardEtale (MvPolynomial (Fin n) R) A]
    (φ : A →ₐ[R] ResidueField R) :
    ∃ ψ : A →ₐ[R] R, ∀ a, algebraMap R (ResidueField R) (ψ a) = φ a
theorem

exists_lift_of_isSmoothAt

L91 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_algHom_lift_of_isSmoothAt.HenselSmoothLift.exists_lift_of_isSmoothAt
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_isSmoothAt
universe u
open IsLocalRing TensorProduct
namespace HenselSmoothLift
variable {R : Type u} [CommRing R] [HenselianLocalRing R]
Lean source · statement
theorem exists_lift_of_isSmoothAt
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    (φ : S →ₐ[R] ResidueField R)
    [(RingHom.ker φ).IsPrime] [Algebra.IsSmoothAt R (RingHom.ker φ)] :
    ∃ ψ : S →ₐ[R] R, ∀ s, algebraMap R (ResidueField R) (ψ s) = φ s
theorem

exists_lift_of_smooth

L112 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_algHom_lift_of_isSmoothAt.HenselSmoothLift.exists_lift_of_smooth
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_algHom_lift_of_isSmoothAt
universe u
open IsLocalRing TensorProduct
namespace HenselSmoothLift
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_algHom_lift_of_isSmoothAt

L121 ↗
HenselianLocalRing.exists_algHom_lift_of_isSmoothAt
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_isSmoothAt
universe u
open IsLocalRing TensorProduct
Lean source · statement
theorem _root_.HenselianLocalRing.exists_algHom_lift_of_isSmoothAt
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.FinitePresentation R S]
    (φ : S →ₐ[R] IsLocalRing.ResidueField R)
    [(RingHom.ker φ).IsPrime] [Algebra.IsSmoothAt R (RingHom.ker φ)] :
    ∃ ψ : S →ₐ[R] R, ∀ s : S, algebraMap R (IsLocalRing.ResidueField R) (ψ s) = φ s

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.