Module

HenselianLocalRing_of_moduleFinite_of_isLocalRing.lean

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_of_moduleFinite_of_isLocalRing

2 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring of module Finite of is Local Ring

Imports1

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite

Imported by2

theorem

main

L33 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_of_moduleFinite_of_isLocalRing.HensFinAux.main

Documentation

A finite local algebra over a henselian local ring lifts simple roots of monic polynomials.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_of_moduleFinite_of_isLocalRing
universe u v
namespace HensFinAux
open IsLocalRing Polynomial
open _root_.HenselianLocalRing
  (exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite)

Lean source · statement

theorem main (R : Type u) [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [IsLocalRing S] [Algebra R S] [Module.Finite R S]
    (f : S[X]) (hf : f.Monic) (a₀ : S) (h₁ : f.eval a₀ ∈ maximalIdeal S)
    (h₂ : IsUnit (f.derivative.eval a₀)) : ∃ a : S, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal S

theorem

of_moduleFinite_of_isLocalRing

L201 ↗

HenselianLocalRing.of_moduleFinite_of_isLocalRing