NYLL
Module

RingRestrictedInertiaDVRTransition.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingRestrictedInertiaDVRTransition
6 declarations indexed from sourceView source ↗

Module documentation

Uniformizer-ratio identities across DVR maps

Proves ratio and residue-coefficient identities for compatible ring maps and group actions across a DVR tower. The exponents are identified with the additive valuation and ramification index of a mapped uniformizer.

Imports8
Imported by2

Declarations

theorem

uniformizerRatioCoefficient_tower_of_ringHom

L34 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioCoefficient_tower_of_ringHom
Documentation

The coefficient calculation depends only on the two actual ring maps and their ratio equations. Group actions are not data of this calculation.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w z
Lean source · statement
theorem uniformizerRatioCoefficient_tower_of_ringHom
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsDomain B]
    (f : A →+* B) (s : A →+* A) (t : B →+* B)
    (π : A) (ρ : B) (hρ : ρ ≠ 0) (r : ℕ) (u : Bˣ)
    (hfactor : f π = ρ ^ r * (u : B)) (c : A) (d : B)
    (hc : π * c = s π) (hd : ρ * d = t ρ)
    (hcomm : f.comp s = t.comp f) :
    f c * (u : B) = d ^ r * t (u : B)
theorem

uniformizerResidueCoefficient_tower_of_ringHom

L52 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerResidueCoefficient_tower_of_ringHom
Documentation

Residue fixing of the upper coefficient map removes the unit correction from the same ring-map ratio calculation.

Source context 4 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w z
Lean source · statement
theorem uniformizerResidueCoefficient_tower_of_ringHom
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [IsDomain B]
    [IsLocalRing B]
    (f : A →+* B) (s : A →+* A) (t : B →+* B)
    (π : A) (ρ : B) (hρ : ρ ≠ 0) (r : ℕ) (u : Bˣ)
    (hfactor : f π = ρ ^ r * (u : B)) (c : A) (d : B)
    (hc : π * c = s π) (hd : ρ * d = t ρ)
    (hcomm : f.comp s = t.comp f)
    (hfixed : (residue B).comp t = residue B) :
    residue B (f c) = residue B d ^ r
theorem

uniformizerRatioCoefficient_tower_of_compatible

L78 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerRatioCoefficient_tower_of_compatible
Documentation

The coefficient ratio calculation for two actual compatible automorphisms. Only the lower group acts on the lower DVR; no pulled-back action is installed.

Source context 9 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w z
variable (A : Type u) (B : Type v)
variable [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
variable [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
variable (G : Type w) (H : Type z) [Group G] [Group H]
variable [MulSemiringAction H A] [MulSemiringAction G B]
Lean source · statement
theorem uniformizerRatioCoefficient_tower_of_compatible
    (f : A →+* B) (π : A) (hπ : Irreducible π) (ρ : B) (hρ : Irreducible ρ)
    (r : ℕ) (u : Bˣ) (hfactor : f π = ρ ^ r * (u : B))
    (g : G) (h : H) (hcomm : ∀ x : A, f (h • x) = g • f x) :
    f (uniformizerRatioUnit A H π hπ h : A) * (u : B) =
      (uniformizerRatioUnit B G ρ hρ g : B) ^ r * (g • (u : B))
theorem

uniformizerResidueCoefficient_tower_of_compatible

L93 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerResidueCoefficient_tower_of_compatible
Documentation

Upper ideal inertia removes the constructed unit correction. The result is in the upper residue field, so it requires no lower residue structure.

Source context 9 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w z
variable (A : Type u) (B : Type v)
variable [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
variable [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
variable (G : Type w) (H : Type z) [Group G] [Group H]
variable [MulSemiringAction H A] [MulSemiringAction G B]
Lean source · statement
theorem uniformizerResidueCoefficient_tower_of_compatible
    (f : A →+* B) (π : A) (hπ : Irreducible π) (ρ : B) (hρ : Irreducible ρ)
    (r : ℕ) (u : Bˣ) (hfactor : f π = ρ ^ r * (u : B))
    (g : G) (h : H) (hcomm : ∀ x : A, f (h • x) = g • f x)
    (hg : g ∈ (maximalIdeal B).inertia G) :
    residue B (f (uniformizerRatioUnit A H π hπ h : A)) =
      residue B (uniformizerRatioUnit B G ρ hρ g : B) ^ r
theorem

uniformizerResidueCoefficient_tower_addVal_of_actionHom

L112 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerResidueCoefficient_tower_addVal_of_actionHom
Documentation

An injective coefficient map and an actual compatible group restriction produce the raw residue-character relation at the native DVR order.

Source context 9 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w z
variable (A : Type u) (B : Type v)
variable [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
variable [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
variable (G : Type w) (H : Type z) [Group G] [Group H]
variable [MulSemiringAction H A] [MulSemiringAction G B]
Lean source · statement
theorem uniformizerResidueCoefficient_tower_addVal_of_actionHom
    (f : A →+* B) (hinj : Function.Injective f)
    (φ : G →* H) (hcomm : ∀ (g : G) (x : A), f ((φ g) • x) = g • f x)
    (π : A) (hπ : Irreducible π) (ρ : B) (hρ : Irreducible ρ)
    (g : G) (hg : g ∈ (maximalIdeal B).inertia G) :
    residue B (f (uniformizerRatioUnit A H π hπ (φ g) : A)) =
      residue B (uniformizerRatioUnit B G ρ hρ g : B) ^
        (IsDiscreteValuationRing.addVal B (f π)).toNat
theorem

uniformizerResidueCoefficient_tower_ramificationIdx_of_actionHom

L127 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerResidueCoefficient_tower_ramificationIdx_of_actionHom
Documentation

The same actual different-group relation at the actual local ramification index, with the entire unit factor supplied by the native DVR owner.

Source context 9 commands

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

noncomputable section
namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
open IsLocalRing
universe u v w z
variable (A : Type u) (B : Type v)
variable [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
variable [CommRing B] [IsDomain B] [IsDiscreteValuationRing B]
variable (G : Type w) (H : Type z) [Group G] [Group H]
variable [MulSemiringAction H A] [MulSemiringAction G B]
Lean source · statement
theorem uniformizerResidueCoefficient_tower_ramificationIdx_of_actionHom
    [Algebra A B] [(maximalIdeal B).LiesOver (maximalIdeal A)]
    (hinj : Function.Injective (algebraMap A B))
    (φ : G →* H)
    (hcomm : ∀ (g : G) (x : A), algebraMap A B ((φ g) • x) = g • algebraMap A B x)
    (π : A) (hπ : Irreducible π) (ρ : B) (hρ : Irreducible ρ)
    (g : G) (hg : g ∈ (maximalIdeal B).inertia G) :
    residue B (algebraMap A B (uniformizerRatioUnit A H π hπ (φ g) : A)) =
      residue B (uniformizerRatioUnit B G ρ hρ g : B) ^
        (maximalIdeal B).ramificationIdx A

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