Module

HenselianFinite.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianFinite

17 declarations indexed from sourceView source ↗

Module documentation

Finite algebra consequences of Henselian pairs

This file keeps the Nakayama and finite-module completion consequences away from the lightweight HenselianDVF core.

Imports6

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Henselian
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.AdicPower
Mathlib.Algebra.Module.Shrink
Mathlib.RingTheory.AdicCompletion.AsTensorProduct
Mathlib.RingTheory.AdicCompletion.Noetherian
Mathlib.RingTheory.Nakayama

Imported by10

theorem

ideal_smul_top_le_module_jacobson_of_le_jacobson_bot

L31 ↗

ValuationTheory.DiscreteValuationField.ideal_smul_top_le_module_jacobson_of_le_jacobson_bot

Documentation

If an ideal lies in the Jacobson radical of the base ring, then its action on any module lands in the module Jacobson radical.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem ideal_smul_top_le_module_jacobson_of_le_jacobson_bot
    {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    {I : Ideal R} (hI : I ≤ Ideal.jacobson (⊥ : Ideal R)) :
    I • (⊤ : Submodule R M) ≤ Module.jacobson R M

theorem

ideal_smul_top_le_module_jacobson_of_henselianRing

L41 ↗

ValuationTheory.DiscreteValuationField.ideal_smul_top_le_module_jacobson_of_henselianRing

Documentation

The jac field of HenselianRing gives the Nakayama/module-Jacobson component needed after applying the Henselian ideal to any module.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem ideal_smul_top_le_module_jacobson_of_henselianRing
    {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
    {I : Ideal R} [HenselianRing R I] :
    I • (⊤ : Submodule R M) ≤ Module.jacobson R M

theorem

ideal_map_restrictScalars_le_module_jacobson_of_henselianRing

L50 ↗

ValuationTheory.DiscreteValuationField.ideal_map_restrictScalars_le_module_jacobson_of_henselianRing

Documentation

Algebra form of ideal_smul_top_le_module_jacobson_of_henselianRing: the base Henselian ideal mapped into an algebra lies in the module Jacobson radical after restricting scalars to the base.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem ideal_map_restrictScalars_le_module_jacobson_of_henselianRing
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    {I : Ideal R} [HenselianRing R I] :
    (I.map (algebraMap R S)).restrictScalars R ≤ Module.jacobson R S

theorem

ideal_map_le_jacobson_bot_of_le_jacobson_bot_of_moduleFinite

L61 ↗

ValuationTheory.DiscreteValuationField.ideal_map_le_jacobson_bot_of_le_jacobson_bot_of_moduleFinite

Documentation

Finite algebra form of the Jacobson/Nakayama component: if an ideal lies in the Jacobson radical of the base, then its extension to a finite algebra lies in the Jacobson radical upstairs.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem ideal_map_le_jacobson_bot_of_le_jacobson_bot_of_moduleFinite
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S] {I : Ideal R}
    (hI : I ≤ Ideal.jacobson (⊥ : Ideal R)) :
    I.map (algebraMap R S) ≤ Ideal.jacobson (⊥ : Ideal S)

theorem

ideal_map_le_jacobson_bot_of_henselianRing_of_moduleFinite

L103 ↗

ValuationTheory.DiscreteValuationField.ideal_map_le_jacobson_bot_of_henselianRing_of_moduleFinite

Documentation

Henselian-ring version of ideal_map_le_jacobson_bot_of_le_jacobson_bot_of_moduleFinite.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem ideal_map_le_jacobson_bot_of_henselianRing_of_moduleFinite
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S] {I : Ideal R} [HenselianRing R I] :
    I.map (algebraMap R S) ≤ Ideal.jacobson (⊥ : Ideal S)

theorem

isHausdorff_map_algebraMap_of_henselianRing_of_moduleFinite

L112 ↗

ValuationTheory.DiscreteValuationField.isHausdorff_map_algebraMap_of_henselianRing_of_moduleFinite

Documentation

In a Noetherian finite algebra over a Henselian pair, the extended Henselian ideal is adically Hausdorff.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isHausdorff_map_algebraMap_of_henselianRing_of_moduleFinite
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S] [IsNoetherianRing S]
    {I : Ideal R} [HenselianRing R I] :
    IsHausdorff (I.map (algebraMap R S)) S

theorem

linearEquiv_comap_pow_smul_top

L124 ↗

ValuationTheory.DiscreteValuationField.linearEquiv_comap_pow_smul_top

Documentation

Pulling back an adic power submodule along a linear equivalence gives the corresponding adic power submodule on the source.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem linearEquiv_comap_pow_smul_top
    {R M N : Type*} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N) (n : ℕ) :
    ((I ^ n • ⊤ : Submodule R N).comap (e : M →ₗ[R] N)) =
      (I ^ n • ⊤ : Submodule R M)

theorem

linearEquiv_map_pow_smul_top

L138 ↗

ValuationTheory.DiscreteValuationField.linearEquiv_map_pow_smul_top

Documentation

Mapping an adic power submodule along a linear equivalence gives the corresponding adic power submodule on the target.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem linearEquiv_map_pow_smul_top
    {R M N : Type*} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N) (n : ℕ) :
    ((I ^ n • ⊤ : Submodule R M).map (e : M →ₗ[R] N)) =
      (I ^ n • ⊤ : Submodule R N)

theorem

isHausdorff_of_linearEquiv

L150 ↗

ValuationTheory.DiscreteValuationField.isHausdorff_of_linearEquiv

Documentation

Adic Hausdorffness is preserved by linear equivalence of modules.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isHausdorff_of_linearEquiv
    {R M N : Type*} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N)
    [IsHausdorff I M] : IsHausdorff I N

theorem

isPrecomplete_of_linearEquiv

L170 ↗

ValuationTheory.DiscreteValuationField.isPrecomplete_of_linearEquiv

Documentation

Adic precompleteness is preserved by linear equivalence of modules.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isPrecomplete_of_linearEquiv
    {R M N : Type*} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N)
    [IsPrecomplete I M] : IsPrecomplete I N

theorem

isHausdorff_linearEquiv_iff

L197 ↗

ValuationTheory.DiscreteValuationField.isHausdorff_linearEquiv_iff

Documentation

Hausdorffness for an ideal is invariant under a linear equivalence.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isHausdorff_linearEquiv_iff
    {R M N : Type*} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N) :
    IsHausdorff I N ↔ IsHausdorff I M

theorem

isPrecomplete_linearEquiv_iff

L212 ↗

ValuationTheory.DiscreteValuationField.isPrecomplete_linearEquiv_iff

Documentation

Precompleteness for an ideal is invariant under a linear equivalence.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isPrecomplete_linearEquiv_iff
    {R M N : Type*} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N) :
    IsPrecomplete I N ↔ IsPrecomplete I M

theorem

isAdicComplete_of_moduleFinite_sameUniverse

L228 ↗

ValuationTheory.DiscreteValuationField.isAdicComplete_of_moduleFinite_sameUniverse

Documentation

Same-universe finite modules over a Noetherian adically complete ring are adically complete.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isAdicComplete_of_moduleFinite_sameUniverse
    {R M : Type u} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] [Module.Finite R M]
    [IsAdicComplete I R] :
    IsAdicComplete I M

theorem

isAdicComplete_of_moduleFinite

L263 ↗

ValuationTheory.DiscreteValuationField.isAdicComplete_of_moduleFinite

Documentation

A finite module over a Noetherian adically complete ring is adically complete.

This is a universe-polymorphic wrapper around mathlib's tensor-product finite-module completion theorem.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem isAdicComplete_of_moduleFinite
    {R : Type u} {M : Type v} [CommRing R] (I : Ideal R)
    [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] [Module.Finite R M]
    [IsAdicComplete I R] :
    IsAdicComplete I M

theorem

henselianRing_map_algebraMap_of_moduleFinite_of_isAdicComplete

L281 ↗

ValuationTheory.DiscreteValuationField.henselianRing_map_algebraMap_of_moduleFinite_of_isAdicComplete

Documentation

A finite algebra over a Noetherian I-adically complete base is Henselian along the ideal generated by I.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField

Lean source · statement

theorem henselianRing_map_algebraMap_of_moduleFinite_of_isAdicComplete
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    {I : Ideal R} [IsNoetherianRing R] [Module.Finite R S]
    [IsAdicComplete I R] :
    HenselianRing S (I.map (algebraMap R S))

theorem

isHausdorff_maximalIdeal

L301 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.isHausdorff_maximalIdeal

Documentation

The maximal-ideal topology on a Henselian DVF valuation ring is separated.

The proof uses only the Henselian Jacobson condition together with the Noetherian DVR structure of the valuation ring.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

theorem isHausdorff_maximalIdeal (F : HenselianDVF.{u, v} K) :
    IsHausdorff F.maximalIdeal F.valuationSubring

theorem

isAdicComplete_maximalIdeal_of_isPrecomplete

L315 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.isAdicComplete_maximalIdeal_of_isPrecomplete

Documentation

A precomplete Henselian DVF valuation ring is adically complete at its maximal ideal, since separatedness is automatic.

Source context 6 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · full declaration

theorem isAdicComplete_maximalIdeal_of_isPrecomplete
    (F : HenselianDVF.{u, v} K)
    [IsPrecomplete F.maximalIdeal F.valuationSubring] :
    IsAdicComplete F.maximalIdeal F.valuationSubring where
  toIsHausdorff := F.isHausdorff_maximalIdeal
  toIsPrecomplete := inferInstance

Module documentation

Finite algebra consequences of Henselian pairs

Declarations