Module

HenselianCyclicIdempotent.lean

Nyll.SchemeTheory.RingTheory.HenselianCyclicIdempotent

1 declaration indexed from sourceView source ↗

Module documentation

Lifting a cyclic quotient idempotent over a Henselian pair

The determinant trick gives an annihilator reducing to (X - 1) * X ^ d. Hensel's lemma lifts the simple root 1. Dividing out this root and evaluating the remaining factor constructs the desired idempotent in the finite algebra.

Imports10

Nyll.SchemeTheory.RingTheory.CyclicIdempotentAnnihilator
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Polynomial.Derivative
Mathlib.Algebra.Polynomial.Div
Mathlib.Algebra.Polynomial.Monic
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Jacobson.Ideal
Mathlib.Tactic.Ring

Imported by2

theorem

exists_idempotent_lift_of_cyclic_quotient

L38 ↗

Algebra.exists_idempotent_lift_of_cyclic_quotient

Documentation

A quotient idempotent whose factor is cyclic over the base lifts to an idempotent in a finite algebra over a Henselian pair.

Source context 4 commands

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

@[expose] public section
open Polynomial
universe u v
namespace Algebra

Lean source · statement

theorem exists_idempotent_lift_of_cyclic_quotient
    {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    [Module.Finite R B] (I : Ideal R) [HenselianRing R I] (b : B)
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R B)) b))
    (hcyc : ∀ x : B ⧸ I.map (algebraMap R B), ∃ r : R,
      Ideal.Quotient.mk (I.map (algebraMap R B)) b * x =
        r • Ideal.Quotient.mk (I.map (algebraMap R B)) b) :
    ∃ e : B, IsIdempotentElem e ∧
      Ideal.Quotient.mk (I.map (algebraMap R B)) e =
        Ideal.Quotient.mk (I.map (algebraMap R B)) b

Module documentation

Lifting a cyclic quotient idempotent over a Henselian pair

Declarations

exists_idempotent_lift_of_cyclic_quotient