Module

RingHomUniformizerCoefficient.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingHomUniformizerCoefficient

4 declarations indexed from sourceView source ↗

Module documentation

Coefficients of a mapped uniformizer

The coefficient in π * c = s(π) is constructed from the ring map and the element. Existence and nonzero-factor cancellation identify it with any actual unit ratio, without using a ramification character.

Imports2

Mathlib.Algebra.Ring.Hom.Defs
Mathlib.Algebra.GroupWithZero.Units.Basic

Imported by2

def

ringHomUniformizerCoefficient

L27 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.ringHomUniformizerCoefficient

Documentation

Extract the coefficient in the literal equation π * c = s(π) when it exists. This construction uses only the ring map and the chosen element; it does not use a character, residue action, or character evaluation.

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

def ringHomUniformizerCoefficient
    (R : Type u) [CommRing R] (s : R →+* R) (π : R) : R

theorem

ringHomUniformizerCoefficient_spec

L34 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.ringHomUniformizerCoefficient_spec

Documentation

An actual coefficient witness makes the extracted coefficient solve the prescribed equation.

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 ringHomUniformizerCoefficient_spec
    (R : Type u) [CommRing R] (s : R →+* R) (π : R)
    (h : ∃ c : R, π * c = s.toFun π) :
    π * ringHomUniformizerCoefficient R s π = s.toFun π

theorem

ringHomUniformizerCoefficient_eq_of_mul_eq

L45 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.ringHomUniformizerCoefficient_eq_of_mul_eq

Documentation

In a domain, the coefficient of a nonzero element is unique. In particular, any actual uniformizer-ratio witness gives this same coefficient.

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 ringHomUniformizerCoefficient_eq_of_mul_eq
    (R : Type u) [CommRing R] [IsDomain R]
    (s : R →+* R) (π : R) (hπ : π ≠ 0)
    (c : R) (hc : π * c = s.toFun π) :
    ringHomUniformizerCoefficient R s π = c

theorem

ringHomUniformizerCoefficient_unit_spec

L55 ↗

RamificationTheory.HilbertRamification.DiscreteValuationRing.ringHomUniformizerCoefficient_unit_spec

Documentation

A constructed unit ratio supplies both properties of the extracted coefficient, with no chosen character or comparison in its definition.

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 ringHomUniformizerCoefficient_unit_spec
    (R : Type u) [CommRing R] [IsDomain R]
    (s : R →+* R) (π : R) (hπ : π ≠ 0)
    (h : ∃ c : R, IsUnit c ∧ π * c = s.toFun π) :
    IsUnit (ringHomUniformizerCoefficient R s π) ∧
      π * ringHomUniformizerCoefficient R s π = s.toFun π

Module documentation

Coefficients of a mapped uniformizer

Declarations

ringHomUniformizerCoefficient

ringHomUniformizerCoefficient_spec

ringHomUniformizerCoefficient_eq_of_mul_eq

ringHomUniformizerCoefficient_unit_spec