NYLL
Module

RingAmbientCoefficientTower.lean

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

Module documentation

Uniformizer-ratio coefficients in a common field

Transports the uniformizer-ratio tower identity to a common field where the upper action fixes the coefficient map. This removes the unit correction and gives the relation at the additive valuation of the mapped uniformizer.

Imports3
Imported by2

Declarations

theorem

uniformizerAmbientCoefficient_tower_of_ringHom

L26 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerAmbientCoefficient_tower_of_ringHom
Documentation

Push the existing literal coefficient-ratio calculation directly to a common field. Fixing that field removes the unit correction; no intermediate residue field or local-homomorphism instance is needed.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v w
Lean source · statement
theorem uniformizerAmbientCoefficient_tower_of_ringHom
    (A : Type u) (B : Type v) (k : Type w)
    [CommRing A] [CommRing B] [IsDomain B] [Field k]
    (f : A →+* B) (s : A →+* A) (t : B →+* B)
    (iA : A →+* k) (iB : B →+* k)
    (hi : iB.comp f = iA) (hfixed : iB.comp t = iB)
    (π : A) (ρ : B) (hρ : ρ ≠ 0) (r : ℕ) (u : Bˣ)
    (hfactor : f.toFun π = ρ ^ r * u.val)
    (c : A) (d : B) (hc : π * c = s.toFun π) (hd : ρ * d = t.toFun ρ)
    (hcomm : f.comp s = t.comp f) :
    iA.toFun c = iB.toFun d ^ r
theorem

uniformizerAmbientCoefficient_tower_addVal_of_ringHom

L57 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.uniformizerAmbientCoefficient_tower_addVal_of_ringHom
Documentation

The common-field raw relation at the actual DVR order. Both the unit factorization and the coefficient-ratio identity come from their existing owners; only the ambient scalar calculation is performed here.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v w
Lean source · statement
theorem uniformizerAmbientCoefficient_tower_addVal_of_ringHom
    (A : Type u) (B : Type v) (k : Type w)
    [CommRing A]
    [CommRing B] [IsDomain B] [IsDiscreteValuationRing B] [Field k]
    (f : A →+* B) (hinj : Function.Injective f.toFun)
    (s : A →+* A) (t : B →+* B)
    (hcomm : f.comp s = t.comp f)
    (iA : A →+* k) (iB : B →+* k)
    (hi : iB.comp f = iA) (hfixed : iB.comp t = iB)
    (π : A) (hπ : Irreducible π) (ρ : B) (hρ : Irreducible ρ)
    (c : A) (d : B) (hc : π * c = s.toFun π) (hd : ρ * d = t.toFun ρ) :
    iA.toFun c = iB.toFun d ^
      (IsDiscreteValuationRing.addVal B (f.toFun π)).toNat

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