NYLL
Module

HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
6 declarations indexed from sourceView source ↗

Module documentation

Henselian Local Ring module Finite localization at Prime of quasi Finite At

Imports1
Imported by4

Declarations

theorem

exists_isIdempotentElem_notMem_iff

L28 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt.HenselFiniteAt.exists_isIdempotentElem_notMem_iff
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
namespace HenselFiniteAt
open IsLocalRing
Lean source · statement
theorem exists_isIdempotentElem_notMem_iff {C : Type*} [CommRing C] [IsArtinianRing C]
    (T : Set (Ideal C)) :
    ∃ e : C, IsIdempotentElem e ∧ ∀ 𝔫 : Ideal C, 𝔫.IsMaximal → (e ∉ 𝔫 ↔ 𝔫 ∈ T)
theorem

map_maximalIdeal_le_of_isMaximal

L68 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt.HenselFiniteAt.map_maximalIdeal_le_of_isMaximal
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
namespace HenselFiniteAt
open IsLocalRing
section finiteAlg
Lean source · statement
theorem map_maximalIdeal_le_of_isMaximal {R : Type*} [CommRing R] [IsLocalRing R]
    {A : Type*} [CommRing A] [Algebra R A] [Module.Finite R A] (𝔑 : Ideal A) [𝔑.IsMaximal] :
    (maximalIdeal R).map (algebraMap R A) ≤ 𝔑
theorem

exists_isIdempotentElem_notMem_iff_of_moduleFinite

L76 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt.HenselFiniteAt.exists_isIdempotentElem_notMem_iff_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_moduleFinite_localization_atPrime_of_quasiFiniteAt
namespace HenselFiniteAt
open IsLocalRing
section finiteAlg
Lean source · statement
theorem exists_isIdempotentElem_notMem_iff_of_moduleFinite (R : Type*) [CommRing R]
  [HenselianLocalRing R]
    {A : Type*} [CommRing A] [Algebra R A] [Module.Finite R A] (T : Set (Ideal A)) :
    ∃ ε : A, IsIdempotentElem ε ∧ ∀ 𝔑 : Ideal A, 𝔑.IsMaximal → (ε ∉ 𝔑 ↔ 𝔑 ∈ T)
theorem

exists_isIdempotentElem_moduleFinite_quotient_notMem

L118 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt.HenselFiniteAt.exists_isIdempotentElem_moduleFinite_quotient_notMem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
namespace HenselFiniteAt
open IsLocalRing
section finiteAt
variable {R : Type*} [CommRing R] [HenselianLocalRing R]
variable {S : Type*} [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
Lean source · statement
theorem exists_isIdempotentElem_moduleFinite_quotient_notMem
    (q : Ideal S) [q.IsPrime] (hq : q.comap (algebraMap R S) = maximalIdeal R)
      [Algebra.QuasiFiniteAt R q] :
    ∃ e : S, IsIdempotentElem e ∧ Module.Finite R (S ⧸ Ideal.span ({1 - e} : Set S)) ∧ e ∉ q
theorem

moduleFinite_localization

L219 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt.HenselFiniteAt.moduleFinite_localization
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
namespace HenselFiniteAt
open IsLocalRing
section finiteAt
variable {R : Type*} [CommRing R] [HenselianLocalRing R]
variable {S : Type*} [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
Lean source · statement
theorem moduleFinite_localization
    (q : Ideal S) [q.IsPrime] (hq : q.comap (algebraMap R S) = maximalIdeal R)
      [Algebra.QuasiFiniteAt R q] :
    Module.Finite R (Localization.AtPrime q)
theorem

moduleFinite_localization_atPrime_of_quasiFiniteAt

L366 ↗
HenselianLocalRing.moduleFinite_localization_atPrime_of_quasiFiniteAt
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace HenselianLocalRing_moduleFinite_localization_atPrime_of_quasiFiniteAt
universe u v
Lean source · statement
theorem _root_.HenselianLocalRing.moduleFinite_localization_atPrime_of_quasiFiniteAt
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type v} [CommRing S] [Algebra R S] [Algebra.FiniteType R S]
    (q : Ideal S) [q.IsPrime] (hq : q.comap (algebraMap R S) = IsLocalRing.maximalIdeal R)
    [Algebra.QuasiFiniteAt R q] :
    Module.Finite R (Localization.AtPrime q)

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