NYLL
Module

TowerInvariants.lean

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

Module documentation

Hilbert ramification theory: ramification and inertia in towers

This file records the tower identities for ramification indices and inertia degrees used in the prime-decomposition tower identity.

Imports1
Imported by2

Declarations

theorem

ramificationIdx_tower

L30 ↗
HilbertRamification.Dedekind.ramificationIdx_tower
Documentation

The prime-decomposition tower identity: ramification indices multiply in a tower.

Source context 7 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
variable {A B C : Type*}
variable [CommRing A] [CommRing B] [CommRing C]
variable [Algebra A B] [Algebra B C] [Algebra A C]
variable [IsScalarTower A B C]
Lean source · statement
theorem ramificationIdx_tower
    [IsDedekindDomain B] [IsDedekindDomain C]
    {p : Ideal A} {P : Ideal B} {Q : Ideal C}
    [P.IsPrime] [Q.IsPrime]
    (hP : Ideal.map (algebraMap B C) P ≠ ⊥)
    (hp : Ideal.map (algebraMap A C) p ≠ ⊥)
    (hPQ : Ideal.map (algebraMap B C) P ≤ Q) :
    Ideal.ramificationIdx' p Q =
      Ideal.ramificationIdx' p P *
        Ideal.ramificationIdx' P Q
theorem

dedekindTower_inertiaDeg_tower

L44 ↗
HilbertRamification.Dedekind.dedekindTower_inertiaDeg_tower
Documentation

The prime-decomposition tower identity: inertia degrees multiply in a tower.

Source context 7 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
variable {A B C : Type*}
variable [CommRing A] [CommRing B] [CommRing C]
variable [Algebra A B] [Algebra B C] [Algebra A C]
variable [IsScalarTower A B C]
Lean source · statement
theorem dedekindTower_inertiaDeg_tower
    (p : Ideal A) [p.IsMaximal]
    (P : Ideal B) [P.IsMaximal] [P.LiesOver p]
    (Q : Ideal C) [Q.LiesOver P] :
    Q.inertiaDeg A =
      P.inertiaDeg A * Q.inertiaDeg B
theorem

dedekindTower_tower_invariants_of_top_product

L57 ↗
HilbertRamification.Dedekind.dedekindTower_tower_invariants_of_top_product
Documentation

The prime-decomposition tower arithmetic identity: if the top layer of a tower already accounts for the full product e * f, while ramification indices and inertia degrees multiply in the tower, then the lower layer is unramified with residue degree one, and the top layer has the original invariants.

Source context 7 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
variable {A B C : Type*}
variable [CommRing A] [CommRing B] [CommRing C]
variable [Algebra A B] [Algebra B C] [Algebra A C]
variable [IsScalarTower A B C]
Lean source · statement
theorem dedekindTower_tower_invariants_of_top_product
    {e f eBase fBase eTop fTop : ℕ}
    (heTop : eTop ≠ 0) (hfTop : fTop ≠ 0)
    (he : e = eBase * eTop)
    (hf : f = fBase * fTop)
    (hprod : eTop * fTop = e * f) :
    eBase = 1 ∧ fBase = 1 ∧ eTop = e ∧ fTop = f
theorem

dedekindTower_ideal_tower_invariants_of_top_product

L87 ↗
HilbertRamification.Dedekind.dedekindTower_ideal_tower_invariants_of_top_product
Documentation

The prime-decomposition tower identity: the ideal-theoretic tower form of the preceding arithmetic cancellation. The hypothesis hprod is exactly the equality supplied in the prime-decomposition tower identity by the nonsplitting of the top prime and the fixed-field degree computation [L : Z_P] = e * f.

Source context 7 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
variable {A B C : Type*}
variable [CommRing A] [CommRing B] [CommRing C]
variable [Algebra A B] [Algebra B C] [Algebra A C]
variable [IsScalarTower A B C]
Lean source · statement
theorem dedekindTower_ideal_tower_invariants_of_top_product
    [IsDedekindDomain B] [IsDedekindDomain C] [Module.Finite B C]
    {p : Ideal A} [p.IsMaximal]
    {P : Ideal B} [P.IsPrime] [P.IsMaximal] [P.LiesOver p]
    {Q : Ideal C} [Q.IsPrime] [Q.LiesOver P]
    (hP : Ideal.map (algebraMap B C) P ≠ ⊥)
    (hp : Ideal.map (algebraMap A C) p ≠ ⊥)
    (hPQ : Ideal.map (algebraMap B C) P ≤ Q)
    (hprod :
      Ideal.ramificationIdx' P Q * Q.inertiaDeg B =
        Ideal.ramificationIdx' p Q * Q.inertiaDeg A) :
    Ideal.ramificationIdx' p P = 1 ∧
      P.inertiaDeg A = 1 ∧
      Ideal.ramificationIdx' P Q =
        Ideal.ramificationIdx' p Q ∧
      Q.inertiaDeg B = Q.inertiaDeg A
theorem

dedekindRamification_tower_middle_invariants_of_top_invariants

L120 ↗
HilbertRamification.Dedekind.dedekindRamification_tower_middle_invariants_of_top_invariants
Documentation

A prime-decomposition arithmetic consequence: if the top layer of a tower has the full ramification index and residue degree one, then the middle layer has ramification index one and the full residue degree.

Source context 7 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
variable {A B C : Type*}
variable [CommRing A] [CommRing B] [CommRing C]
variable [Algebra A B] [Algebra B C] [Algebra A C]
variable [IsScalarTower A B C]
Lean source · statement
theorem dedekindRamification_tower_middle_invariants_of_top_invariants
    {e f eBase fBase eTop fTop : ℕ}
    (heTop : eTop ≠ 0)
    (he : e = eBase * eTop)
    (hf : f = fBase * fTop)
    (heTop_eq : eTop = e)
    (hfTop_eq : fTop = 1) :
    eBase = 1 ∧ fBase = f
theorem

dedekindRamification_ideal_tower_middle_invariants_of_top_invariants

L143 ↗
HilbertRamification.Dedekind.dedekindRamification_ideal_tower_middle_invariants_of_top_invariants
Documentation

A prime-decomposition consequence: the ideal-theoretic tower form of the preceding arithmetic cancellation. This is the step from the already-proved P/P_T invariants to the P_T/P_Z invariants in the diagram Z_P -> T_P -> L.

Source context 7 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
variable {A B C : Type*}
variable [CommRing A] [CommRing B] [CommRing C]
variable [Algebra A B] [Algebra B C] [Algebra A C]
variable [IsScalarTower A B C]
Lean source · statement
theorem dedekindRamification_ideal_tower_middle_invariants_of_top_invariants
    [IsDedekindDomain B] [IsDedekindDomain C]
    {p : Ideal A} [p.IsMaximal]
    {P : Ideal B} [P.IsPrime] [P.IsMaximal] [P.LiesOver p]
    {Q : Ideal C} [Q.IsPrime] [Q.LiesOver P]
    (hP : Ideal.map (algebraMap B C) P ≠ ⊥)
    (hp : Ideal.map (algebraMap A C) p ≠ ⊥)
    (hPQ : Ideal.map (algebraMap B C) P ≤ Q)
    (heTop :
      Ideal.ramificationIdx' P Q =
        Ideal.ramificationIdx' p Q)
    (hfTop : Q.inertiaDeg B = 1) :
    Ideal.ramificationIdx' p P = 1 ∧
      P.inertiaDeg A = Q.inertiaDeg A

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