Module

HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite

4 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring exists is Idempotent Elem map eq of module finite

Imports2

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_algHom_lift_of_etale

Imported by2

theorem

aeval_mul_one_sub_of_isIdempotentElem

L31 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite.F1aSol.aeval_mul_one_sub_of_isIdempotentElem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite
universe u v
open Polynomial IsLocalRing
namespace F1aSol

Lean source · statement

theorem aeval_mul_one_sub_of_isIdempotentElem {R A : Type*} [CommRing R] [CommRing A]
  [Algebra R A]
    (q : R[X]) {ε : A} (hε : IsIdempotentElem ε) :
    aeval ε q * (1 - ε) = algebraMap R A (q.coeff 0) * (1 - ε)

theorem

aeval_mul_self_of_isIdempotentElem

L43 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite.F1aSol.aeval_mul_self_of_isIdempotentElem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite
universe u v
open Polynomial IsLocalRing
namespace F1aSol

Lean source · statement

theorem aeval_mul_self_of_isIdempotentElem {R A : Type*} [CommRing R] [CommRing A] [Algebra
  R A]
    (q : R[X]) {ε : A} (hε : IsIdempotentElem ε) :
    aeval ε q * ε = algebraMap R A (q.eval 1) * ε

theorem

aeval_eq_zero_of_forall_coeff_mem

L51 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite.F1aSol.aeval_eq_zero_of_forall_coeff_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite
universe u v
open Polynomial IsLocalRing
namespace F1aSol

Lean source · statement

theorem aeval_eq_zero_of_forall_coeff_mem {R A : Type*} [CommRing R] [CommRing A] [Algebra
  R A]
    (I : Ideal R) (hI : ∀ r ∈ I, algebraMap R A r = 0) (q : R[X]) (hq : ∀ i, q.coeff i ∈ I) (x : A)
      :
    aeval x q = 0

theorem

exists_isIdempotentElem_map_eq_of_module_finite

L63 ↗

HenselianLocalRing.exists_isIdempotentElem_map_eq_of_module_finite

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_exists_isIdempotentElem_map_eq_of_module_finite
universe u v
open Polynomial IsLocalRing
open F1aSol in

Lean source · statement

theorem _root_.HenselianLocalRing.exists_isIdempotentElem_map_eq_of_module_finite
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {B : Type v} [CommRing B] [Algebra R B] [Module.Finite R B]
    (e₀ : B ⧸ Ideal.map (algebraMap R B) (IsLocalRing.maximalIdeal R)) (he₀ : IsIdempotentElem e₀) :
    ∃ e : B, IsIdempotentElem e ∧
      Ideal.Quotient.mk (Ideal.map (algebraMap R B) (IsLocalRing.maximalIdeal R)) e = e₀

Module documentation

Henselian Local Ring exists is Idempotent Elem map eq of module finite

Declarations

aeval_mul_one_sub_of_isIdempotentElem

aeval_mul_self_of_isIdempotentElem

aeval_eq_zero_of_forall_coeff_mem

exists_isIdempotentElem_map_eq_of_module_finite