NYLL
Module

RingPrincipalInertiaCriterion.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingPrincipalInertiaCriterion
2 declarations indexed from sourceView source ↗

Module documentation

A maximal-ideal criterion for principal-unit inertia

Expresses membership in principal-unit inertia by requiring each multiplier minus one to lie in the maximal ideal.

Imports2
Imported by3

Declarations

theorem

residue_eq_one_iff_sub_one_mem

L23 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.residue_eq_one_iff_sub_one_mem
Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
Lean source · statement
theorem residue_eq_one_iff_sub_one_mem
    {R : Type u} [CommRing R] [IsLocalRing R] (x : R) :
    residue R x = 1 ↔ x - 1 ∈ maximalIdeal R
theorem

mem_principalUnitInertia_iff_sub_one_mem

L30 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.mem_principalUnitInertia_iff_sub_one_mem
Documentation

Membership in the same actual principal-unit inertia is expressed without opening the residue field at downstream comparison boundaries.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v
Lean source · statement
theorem mem_principalUnitInertia_iff_sub_one_mem
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (G : Type v) [Group G] [MulSemiringAction G R]
    (σ : (maximalIdeal R).inertia G) :
    σ ∈ principalUnitInertia R G ↔
      ∀ x : R, ∃ a : Rˣ,
        (σ : G) • x = x * (a : R) ∧ (a : R) - 1 ∈ maximalIdeal R

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