NYLL
Module

HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.lean

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
41 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring exists Unique is Idempotent Elem mk eq of module Finite

Imports1
Imported by5

Declarations

def

poly

L35 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.poly
Documentation

The polynomial with the given finite vector of coefficients.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · statement
def poly {n : ℕ} (c : Fin n → T) : T[X]
theorem

coeff_poly

L37 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.coeff_poly
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · full declaration
theorem coeff_poly {n : ℕ} (c : Fin n → T) (j : ℕ) :
    (poly c).coeff j = if h : j < n then c ⟨j, h⟩ else 0 := by
  classical
  unfold poly
  rw [finsetSum_coeff]
  simp only [coeff_C_mul_X_pow]
  split_ifs with h
  · rw [Finset.sum_eq_single ⟨j, h⟩]
    · simp
    · intro b _ hb
      rw [ite_eq_right]
      intro hj
      apply hb
      ext
      exact hj.symm
    · intro hj; exact absurd (Finset.mem_univ _) hj
  · apply Finset.sum_eq_zero
    intro i _
    rw [ite_eq_right]
    intro hj
    exact h (hj ▸ i.2)
theorem

coeff_poly_fin

L59 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.coeff_poly_fin
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · statement
theorem coeff_poly_fin {n : ℕ} (c : Fin n → T) (i : Fin n) : (poly c).coeff i = c i
theorem

degree_poly_lt

L62 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.degree_poly_lt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · statement
theorem degree_poly_lt {n : ℕ} (c : Fin n → T) : (poly c).degree < n
theorem

poly_coeff_eq_of_degree_lt

L65 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.poly_coeff_eq_of_degree_lt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · full declaration
theorem poly_coeff_eq_of_degree_lt {n : ℕ} (p : T[X]) (hp : p.degree < n) :
    poly (fun i : Fin n => p.coeff i) = p := by
  ext j
  rw [coeff_poly]
  split_ifs with h
  · rfl
  · symm
    apply coeff_eq_zero_of_degree_lt
    exact lt_of_lt_of_le hp (by exact_mod_cast not_lt.mp h)
theorem

poly_map

L75 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.poly_map
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · full declaration
theorem poly_map {n : ℕ} (c : Fin n → T) {T' : Type*} [CommRing T'] (φ : T →+* T') :
    (poly c).map φ = poly (fun i => φ (c i)) := by
  unfold poly
  simp [Polynomial.map_sum]
theorem

poly_injective

L80 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.poly_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · statement
theorem poly_injective {n : ℕ} {c c' : Fin n → T} (h : poly c = poly c') : c = c'
theorem

eq_of_dvd_sub_of_degree_lt

L84 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.eq_of_dvd_sub_of_degree_lt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section poly
variable {T : Type*} [CommRing T]
Lean source · statement
theorem eq_of_dvd_sub_of_degree_lt {F p q : T[X]} (hF : F.Monic)
    (hp : p.degree < F.degree) (hq : q.degree < F.degree) (h : F ∣ p - q) : p = q
def

redQuot

L101 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.redQuot
Documentation

Reduction of an adjoined-root ring along the prescribed reduction of its defining polynomial.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section reduction
variable {B : Type*} [CommRing B] (J : Ideal B) (F : B[X]) (G : (B ⧸ J)[X])
  (hG : F.map (Ideal.Quotient.mk J) = G)
Lean source · statement
def redQuot : AdjoinRoot F →+* AdjoinRoot G
theorem

redQuot_mk

L107 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.redQuot_mk
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section reduction
variable {B : Type*} [CommRing B] (J : Ideal B) (F : B[X]) (G : (B ⧸ J)[X])
  (hG : F.map (Ideal.Quotient.mk J) = G)
include hG in
Lean source · statement
theorem redQuot_mk (p : B[X]) :
    redQuot J F G hG (AdjoinRoot.mk F p) = AdjoinRoot.mk G (p.map (Ideal.Quotient.mk J))
theorem

redQuot_surjective

L114 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.redQuot_surjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section reduction
variable {B : Type*} [CommRing B] (J : Ideal B) (F : B[X]) (G : (B ⧸ J)[X])
  (hG : F.map (Ideal.Quotient.mk J) = G)
Lean source · statement
theorem redQuot_surjective : Function.Surjective (redQuot J F G hG)
theorem

ker_redQuot_le

L120 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.ker_redQuot_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section reduction
variable {B : Type*} [CommRing B] (J : Ideal B) (F : B[X]) (G : (B ⧸ J)[X])
  (hG : F.map (Ideal.Quotient.mk J) = G)
Lean source · statement
theorem ker_redQuot_le :
    RingHom.ker (redQuot J F G hG) ≤ J.map (AdjoinRoot.of F)
theorem

isNilpotent_of_mem_ker_redQuot

L142 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.isNilpotent_of_mem_ker_redQuot
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section reduction
variable {B : Type*} [CommRing B] (J : Ideal B) (F : B[X]) (G : (B ⧸ J)[X])
  (hG : F.map (Ideal.Quotient.mk J) = G)
Lean source · statement
theorem isNilpotent_of_mem_ker_redQuot (hJ : J ^ 2 = ⊥) {x : AdjoinRoot F}
    (hx : x ∈ RingHom.ker (redQuot J F G hG)) : IsNilpotent x
abbrev

P

L157 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.P
Documentation

The polynomial ring of coefficients for representatives modulo the given polynomial.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
Lean source · statement
abbrev P : Type u
def

genericElem

L160 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.genericElem
Documentation

The generic polynomial of degree below the degree of the given polynomial.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
Lean source · statement
def genericElem : (P f)[X]
def

idemRem

L164 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.idemRem
Documentation

The remainder of the generic idempotence equation modulo the defining polynomial.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
Lean source · statement
def idemRem : (P f)[X]
def

idemIdeal

L169 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.idemIdeal
Documentation

The ideal of coefficient equations expressing generic idempotence modulo the defining polynomial.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
Lean source · statement
def idemIdeal : Ideal (P f)
theorem

idemIdeal_fg

L171 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.idemIdeal_fg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
Lean source · statement
theorem idemIdeal_fg : (idemIdeal f).FG
abbrev

E

L174 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.E
Documentation

The coefficient algebra cut out by the idempotence equations.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
Lean source · statement
abbrev E : Type u
def

elemOf

L183 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.elemOf
Documentation

The polynomial obtained by evaluating the generic coefficients under an algebra homomorphism.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
def elemOf (ψ : P f →ₐ[R] B) : B[X]
theorem

genericElem_map

L186 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.genericElem_map
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem genericElem_map (ψ : P f →ₐ[R] B) :
    (genericElem f).map (ψ : P f →+* B) = elemOf ψ
theorem

map_algebraMap_map

L192 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.map_algebraMap_map
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem map_algebraMap_map (ψ : P f →ₐ[R] B) :
    (f.map (algebraMap R (P f))).map (ψ : P f →+* B) = f.map (algebraMap R B)
theorem

idemRem_map

L196 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.idemRem_map
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem idemRem_map (hf : f.Monic) (ψ : P f →ₐ[R] B) :
    (idemRem f).map (ψ : P f →+* B) =
      (elemOf ψ * elemOf ψ - elemOf ψ) %ₘ (f.map (algebraMap R B))
theorem

forall_idemIdeal_iff

L203 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.forall_idemIdeal_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem forall_idemIdeal_iff (hf : f.Monic) (ψ : P f →ₐ[R] B) :
    (∀ a ∈ idemIdeal f, ψ a = 0) ↔
      IsIdempotentElem (AdjoinRoot.mk (f.map (algebraMap R B)) (elemOf ψ))
theorem

elemOf_comp

L227 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.elemOf_comp
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem elemOf_comp {B' : Type*} [CommRing B'] [Algebra R B'] (χ : B →ₐ[R] B')
    (ψ : P f →ₐ[R] B) :
    elemOf (χ.comp ψ) = (elemOf ψ).map (χ : B →+* B')
theorem

degree_elemOf_lt

L234 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.degree_elemOf_lt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem degree_elemOf_lt (ψ : P f →ₐ[R] B) : (elemOf ψ).degree < f.natDegree
theorem

degree_map_eq

L237 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.degree_map_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem degree_map_eq (hf : f.Monic) [Nontrivial B] :
    (f.map (algebraMap R B)).degree = f.natDegree
theorem

apply_X_eq_of_mk_eq

L241 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.apply_X_eq_of_mk_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem apply_X_eq_of_mk_eq (hf : f.Monic) {ψ₁ ψ₂ : P f →ₐ[R] B}
    (h : AdjoinRoot.mk (f.map (algebraMap R B)) (elemOf ψ₁) =
      AdjoinRoot.mk (f.map (algebraMap R B)) (elemOf ψ₂)) (i : Fin f.natDegree) :
    ψ₁ (MvPolynomial.X i) = ψ₂ (MvPolynomial.X i)
def

evalAt

L255 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.evalAt
Documentation

The algebra homomorphism evaluating coefficient variables at the chosen vector.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
def evalAt (c : Fin f.natDegree → B) : P f →ₐ[R] B
theorem

evalAt_X

L257 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.evalAt_X
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem evalAt_X (c : Fin f.natDegree → B) (i : Fin f.natDegree) :
    evalAt (f := f) c (MvPolynomial.X i) = c i
theorem

elemOf_evalAt

L261 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.elemOf_evalAt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem elemOf_evalAt (c : Fin f.natDegree → B) : elemOf (evalAt (f := f) c) = poly c
theorem

forall_idemIdeal_comp_mk

L267 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.forall_idemIdeal_comp_mk
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem forall_idemIdeal_comp_mk (ψ : E f →ₐ[R] B) :
    ∀ a ∈ idemIdeal f, (ψ.comp (Ideal.Quotient.mkₐ R (idemIdeal f))) a = 0
theorem

exists_algHom_of_isIdempotentElem

L272 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.exists_algHom_of_isIdempotentElem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
section points
variable {B : Type*} [CommRing B] [Algebra R B]
Lean source · statement
theorem exists_algHom_of_isIdempotentElem (hf : f.Monic)
    (x : AdjoinRoot (f.map (algebraMap R B))) (hx : IsIdempotentElem x) :
    ∃ ψ : E f →ₐ[R] B, AdjoinRoot.mk (f.map (algebraMap R B))
      (elemOf (ψ.comp (Ideal.Quotient.mkₐ R (idemIdeal f)))) = x
theorem

formallyEtale_E

L301 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.formallyEtale_E
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
Lean source · statement
theorem formallyEtale_E (hf : f.Monic) : Algebra.FormallyEtale R (E f)
theorem

etale_E

L350 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.etale_E
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section scheme
variable {R : Type u} [CommRing R] (f : R[X])
variable {f}
Lean source · statement
theorem etale_E (hf : f.Monic) : Algebra.Etale R (E f)
theorem

exists_dvd_and_map_residue_eq

L362 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.exists_dvd_and_map_residue_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section hensel
variable {R : Type u} [CommRing R] [HenselianLocalRing R]
open IsLocalRing
Lean source · statement
theorem exists_dvd_and_map_residue_eq {f : R[X]} (hf : f.Monic)
    (e₀ : (ResidueField R)[X]) (hdeg : e₀.degree < f.natDegree)
    (he₀ : f.map (residue R) ∣ e₀ * e₀ - e₀) :
    ∃ e : R[X], e.degree < f.natDegree ∧ f ∣ e * e - e ∧ e.map (residue R) = e₀
theorem

exists_isIdempotentElem_of_isArtinianRing

L402 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.exists_isIdempotentElem_of_isArtinianRing
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section finite
open IsLocalRing
variable {R : Type u} [CommRing R]
Lean source · statement
theorem exists_isIdempotentElem_of_isArtinianRing {C : Type*} [CommRing C] [IsArtinianRing C]
    (c : C) : ∃ (N : ℕ) (d : C), 1 ≤ N ∧ IsIdempotentElem (d * c ^ N) ∧ c ^ N = (d * c ^ N) * c ^ N
theorem

map_maximalIdeal_le_jacobson

L425 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.map_maximalIdeal_le_jacobson
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section finite
open IsLocalRing
variable {R : Type u} [CommRing R]
Lean source · statement
theorem map_maximalIdeal_le_jacobson [IsLocalRing R] {S : Type*} [CommRing S] [Algebra R S]
    [Module.Finite R S] :
    (maximalIdeal R).map (algebraMap R S) ≤ Ideal.jacobson ⊥
theorem

eq_of_sub_mem_jacobson

L435 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.eq_of_sub_mem_jacobson
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section finite
open IsLocalRing
variable {R : Type u} [CommRing R]
Lean source · statement
theorem eq_of_sub_mem_jacobson {S : Type*} [CommRing S] {e₁ e₂ : S}
    (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂) (h : e₁ - e₂ ∈ Ideal.jacobson (⊥ :
      Ideal S)) :
    e₁ = e₂
theorem

existsUnique_isIdempotentElem_mk_eq

L457 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite.HenselIdem.existsUnique_isIdempotentElem_mk_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
namespace HenselIdem
universe u
section finite
open IsLocalRing
variable {R : Type u} [CommRing R]
variable [HenselianLocalRing R]
Lean source · statement
theorem existsUnique_isIdempotentElem_mk_eq {S : Type*} [CommRing S] [Algebra R S]
    [Module.Finite R S]
    (ē : S ⧸ (maximalIdeal R).map (algebraMap R S)) (hē : IsIdempotentElem ē) :
    ∃! e : S, IsIdempotentElem e ∧
      Ideal.Quotient.mk ((maximalIdeal R).map (algebraMap R S)) e = ē
theorem

existsUnique_isIdempotentElem_mk_eq_of_moduleFinite

L542 ↗
HenselianLocalRing.existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
open Polynomial
universe u v
open HenselIdem in
Lean source · statement
theorem _root_.HenselianLocalRing.existsUnique_isIdempotentElem_mk_eq_of_moduleFinite
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S]
    (ē : S ⧸ (IsLocalRing.maximalIdeal R).map (algebraMap R S)) (hē : IsIdempotentElem ē) :
    ∃! e : S, IsIdempotentElem e ∧
      Ideal.Quotient.mk ((IsLocalRing.maximalIdeal R).map (algebraMap R S)) e = ē

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