NYLL
Module

PrincipalUnitActionComparison.lean

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

Module documentation

Actual principal-unit multipliers and field-unit quotients

The intrinsic ring predicate used by the DVR character kernel is equivalent to the field-unit predicate used by Hilbert ramification. The proof constructs the required units and uses the valuation alternative, without any fraction field scalar dictionaries or a supplied subgroup comparison.

Imports3
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.Algebra.Group.Units.Equiv
Imported by2

Declarations

theorem

mem_principalUnitGroup_iff_exists_principal_unit

L26 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.mem_principalUnitGroup_iff_exists_principal_unit
Source context 3 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u
Lean source · statement
theorem mem_principalUnitGroup_iff_exists_principal_unit
    {L : Type u} [Field L] (V : _root_.ValuationSubring L) (q : Lˣ) :
    q ∈ V.principalUnitGroup ↔
      ∃ a : Vˣ, ((a : V) : L) = (q : L) ∧
        (a : V) - 1 ∈ IsLocalRing.maximalIdeal V
theorem

principalUnitMultipliers_iff_unitQuotients

L48 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.principalUnitMultipliers_iff_unitQuotients
Documentation

A compatible actual field endomorphism acts by principal-unit multipliers on every valuation-ring element exactly when all its field-unit quotients are principal units.

Source context 3 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u
Lean source · statement
theorem principalUnitMultipliers_iff_unitQuotients
    {L : Type u} [Field L] (V : _root_.ValuationSubring L)
    (σ : L →+* L) (τ : V →+* V)
    (hcompat : V.subtype.comp τ = σ.comp V.subtype) :
    (∀ x : V, ∃ a : Vˣ,
      τ x = x * (a : V) ∧ (a : V) - 1 ∈ IsLocalRing.maximalIdeal V) ↔
      ∀ x : Lˣ, Units.map σ.toMonoidHom x / x ∈ V.principalUnitGroup

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