Module

HenselianLocalRing_exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite.lean

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite

9 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring exists complete Orthogonal Idempotents forall is Local Ring quotient

of module Finite

Imports1

Nyll.SchemeTheory.RingTheory.HenselianLocalRing_existsUnique_isIdempotentElem_mk_eq_of_moduleFinite

Imported by4

theorem

hensSplit_comap_map_mk

L30 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_comap_map_mk

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_comap_map_mk {S : Type v} [CommRing S] {K m : Ideal S} (hK : K ≤ m) :
    (m.map (Ideal.Quotient.mk K)).comap (Ideal.Quotient.mk K) = m

theorem

hensSplit_isMaximal_map_mk

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_isMaximal_map_mk

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_isMaximal_map_mk {S : Type v} [CommRing S] {K m : Ideal S} (hm : m.IsMaximal)
    (hK : K ≤ m) : (m.map (Ideal.Quotient.mk K)).IsMaximal

theorem

hensSplit_map_maximalIdeal_le

L45 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_map_maximalIdeal_le

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_map_maximalIdeal_le {R : Type u} [CommRing R] [IsLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] (m : Ideal S) (hm : m.IsMaximal) :
    (maximalIdeal R).map (algebraMap R S) ≤ m

theorem

hensSplit_isArtinianRing_fibre

L54 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_isArtinianRing_fibre

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_isArtinianRing_fibre {R : Type u} [CommRing R] [IsLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] :
    IsArtinianRing (S ⧸ (maximalIdeal R).map (algebraMap R S))

theorem

hensSplit_finite_maximalSpectrum

L70 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_finite_maximalSpectrum

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_finite_maximalSpectrum {R : Type u} [CommRing R] [IsLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] : Finite (MaximalSpectrum S)

theorem

hensSplit_isIdempotentElem_eq_zero_or_one

L88 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_isIdempotentElem_eq_zero_or_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_isIdempotentElem_eq_zero_or_one {R : Type u} [CommRing R] [IsLocalRing R] {a : R}
    (ha : IsIdempotentElem a) : a = 0 ∨ a = 1

theorem

hensSplit_isIdempotentElem_eq_of_mk_eq

L97 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_isIdempotentElem_eq_of_mk_eq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_isIdempotentElem_eq_of_mk_eq {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] {a b : S}
    (ha : IsIdempotentElem a) (hb : IsIdempotentElem b)
    (h : Ideal.Quotient.mk ((maximalIdeal R).map (algebraMap R S)) a =
      Ideal.Quotient.mk ((maximalIdeal R).map (algebraMap R S)) b) : a = b

theorem

hensSplit_isLocalRing_quotient

L105 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents.hensSplit_isLocalRing_quotient

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v
section hensSplitHelpers
open IsLocalRing

Lean source · statement

theorem hensSplit_isLocalRing_quotient {S : Type v} [CommRing S] (e : S) (m : Ideal S) (hm :
  m.IsMaximal)
    (h1 : 1 - e ∈ m) (h2 : ∀ m' : Ideal S, m'.IsMaximal → m' ≠ m → e ∈ m') :
    IsLocalRing (S ⧸ Ideal.span {1 - e})

theorem

exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite

L140 ↗

HenselianLocalRing.exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite

Source context 4 commands

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

section ProofImplementation
namespace HenselianLocalRing
open _root_.AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianOrthogonalIdempotents
universe u v

Lean source · statement

theorem exists_completeOrthogonalIdempotents_forall_isLocalRing_quotient_of_moduleFinite
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Module.Finite R S] :
    ∃ (_ : Fintype (MaximalSpectrum S)) (e : MaximalSpectrum S → S),
      CompleteOrthogonalIdempotents e ∧
      (∀ m : MaximalSpectrum S, e m ∉ m.asIdeal) ∧
      (∀ m m' : MaximalSpectrum S, m ≠ m' → e m ∈ m'.asIdeal) ∧
      (∀ m : MaximalSpectrum S, IsLocalRing (S ⧸ Ideal.span {1 - e m}))

Module documentation

Henselian Local Ring exists complete Orthogonal Idempotents forall is Local Ring quotient

Declarations