Hilbert's Ramification Theory

In this file, we discuss the ramification theory in Galois extensions of number fields.

Main definitions and results

• isMaximal_conjugates : The Galois group Gal(K/L) acts transitively on the set of all maximal ideals.
• ramificationIdx_eq_of_isGalois : In the case of Galois extension, all the ramificationIdx are the same.
• inertiaDeg_eq_of_isGalois: In the case of Galois extension, all the inertiaDeg are the same.
• decompositionGroup is consisting of all elements of the Galois group L ≃ₐ[K] L such that keep P invariant.
• inertiaDeg_of_decompositionideal_over_bot_eq_oneThe : The residue class field corresponding to decompositionField p P is isomorphic toresidue class field corresponding to p.
• inertiaGroup is the subgorup of L ≃ₐ[K] L that consists of all the σ : L ≃ₐ[K] L that are identity modulo P.

References

• [J Neukirch, Algebraic Number Theory][Neukirch1992]

Preliminary

@[reducible, inline]

abbrev NumberField.idealUnder (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) : Ideal (NumberField.RingOfIntegers K)

The ideal obtained by intersecting 𝓞 K and P.

Equations

• NumberField.idealUnder K P = Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) P

theorem NumberField.idealUnder_def (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) : NumberField.idealUnder K P = Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) P

instance NumberField.idealUnder.IsPrime (K : Type u_1) [Field K] {L : Type u_2} [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsPrime] : (NumberField.idealUnder K P).IsPrime

Equations

• ⋯ = ⋯

class NumberField.ideal_lies_over {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) (p : Ideal (NumberField.RingOfIntegers K)) : Prop

We say P lies over p if p is the preimage of P under the algebraMap.

• over : p = Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) P

def NumberField.term_Lies_over_ : Lean.TrailingParserDescr

We say P lies over p if p is the preimage of P under the algebraMap.

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.over_idealUnder {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) : P lies_over NumberField.idealUnder K P

Equations

• ⋯ = ⋯

class NumberField.ideal_unique_lies_over {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) (p : Ideal (NumberField.RingOfIntegers K)) extends P lies_over p : Prop

• over : p = Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) P
• unique : ∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsMaximal] [inst : Q lies_over p], Q = P

def NumberField.term_Unique_lies_over_ : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.idealUnder.IsMaximal {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : (NumberField.idealUnder K P).IsMaximal

If P is a maximal ideal of 𝓞 L, then the intersection of P and 𝓞 K is also a maximal ideal.

Equations

• ⋯ = ⋯

instance NumberField.ideal_comap_int.IsMaximal {K : Type u_3} [Field K] [NumberField K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] : (Ideal.comap (algebraMap ℤ (NumberField.RingOfIntegers K)) p).IsMaximal

In particular, if p is a maximal ideal of ringOfIntegers, then the intersection of p and ℤ is also a maximal ideal.

Equations

• ⋯ = ⋯

theorem NumberField.exists_ideal_over_maximal_of_ringOfIntegers {K : Type u_3} [Field K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_5) [Field L] [NumberField L] [Algebra K L] : ∃ (P : Ideal (NumberField.RingOfIntegers L)), P.IsMaximal ∧ P lies_over p

For any maximal idela p in 𝓞 K, there exists a maximal ideal in 𝓞 L lying over p.

theorem NumberField.ne_bot_ofIsMaximal {K : Type u_3} [Field K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] [NumberField K] : p ≠ ⊥

Maximal Ideals in the ring of integers are non-zero.

theorem NumberField.map_isMaximal_ne_bot {K : Type u_3} [Field K] [NumberField K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_5) [Field L] [Algebra K L] : Ideal.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p ≠ ⊥

The image of a maximal ideal under the algebraMap between ring of integers is non-zero.

theorem NumberField.prime_iff_isMaximal {L : Type u_4} [Field L] [NumberField L] (P : Ideal (NumberField.RingOfIntegers L)) : Prime P ↔ P.IsMaximal

@[reducible, inline]

noncomputable abbrev NumberField.primes_over {K : Type u_5} [Field K] (p : Ideal (NumberField.RingOfIntegers K)) (L : Type u_6) [Field L] [NumberField L] [Algebra K L] : Finset (Ideal (NumberField.RingOfIntegers L))

The Finset consists of all primes lying over p : Ideal (𝓞 K).

Equations

• NumberField.primes_over p L = (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p)).toFinset

theorem NumberField.primes_over_mem {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] : P ∈ NumberField.primes_over p L ↔ P.IsMaximal ∧ P lies_over p

instance NumberField.primes_over_instIsMaximal {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (Q : { x : Ideal (NumberField.RingOfIntegers L) // x ∈ NumberField.primes_over p L }) : (↑Q).IsMaximal

Equations

• ⋯ = ⋯

instance NumberField.primes_over_inst_lies_over {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (Q : { x : Ideal (NumberField.RingOfIntegers L) // x ∈ NumberField.primes_over p L }) : ↑Q lies_over p

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev NumberField.primes_over.mk {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : { x : Ideal (NumberField.RingOfIntegers L) // x ∈ NumberField.primes_over p L }

Given a maximal ideal P lies_over p in 𝓞 L, primes_over.mk sends P to an element of the subset primes_over p L of Ideal (𝓞 L).

Equations

• NumberField.primes_over.mk p P = ⟨P, ⋯⟩

theorem NumberField.primes_over_card_ne_zero {K : Type u_5} [Field K] [NumberField K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_7) [Field L] [NumberField L] [Algebra K L] : (NumberField.primes_over p L).card ≠ 0

theorem NumberField.unique_primes_over_card_eq_one {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (P : Ideal (NumberField.RingOfIntegers L)) [hp : P unique_lies_over p] : (NumberField.primes_over p L).card = 1

Another form of the property unique_lies_over.

theorem NumberField.ideal_lies_over.trans {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] {E : Type u_9} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (NumberField.RingOfIntegers K)) (𝔓 : Ideal (NumberField.RingOfIntegers E)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : 𝔓 lies_over p] [hP : P lies_over 𝔓] : P lies_over p

theorem NumberField.ideal_lies_over_tower_bot {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] {E : Type u_9} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (NumberField.RingOfIntegers K)) (𝔓 : Ideal (NumberField.RingOfIntegers E)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : P lies_over p] [hP : P lies_over 𝔓] : 𝔓 lies_over p

theorem NumberField.ideal_unique_lies_over.trans {K : Type u_10} {L : Type u_11} [Field K] [Field L] [Algebra K L] {E : Type u_12} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (NumberField.RingOfIntegers K)) (𝔓 : Ideal (NumberField.RingOfIntegers E)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : 𝔓 unique_lies_over p] [hP : P unique_lies_over 𝔓] : P unique_lies_over p

theorem NumberField.ideal_unique_lies_over_tower_bot {K : Type u_10} {L : Type u_11} [Field K] [Field L] [NumberField L] [Algebra K L] {E : Type u_12} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (NumberField.RingOfIntegers K)) (𝔓 : Ideal (NumberField.RingOfIntegers E)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : P unique_lies_over p] [hP : P lies_over 𝔓] : 𝔓 unique_lies_over p

theorem NumberField.ideal_unique_lies_over_tower_top {K : Type u_10} {L : Type u_11} [Field K] [Field L] [NumberField L] [Algebra K L] {E : Type u_12} [Field E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (NumberField.RingOfIntegers K)) (𝔓 : Ideal (NumberField.RingOfIntegers E)) (P : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsMaximal] [hP : P unique_lies_over p] [𝔓 lies_over p] : P unique_lies_over 𝔓

instance NumberField.IntermediateField_ideal_lies_over {K : Type u_13} {L : Type u_14} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [P lies_over p] (E : IntermediateField K L) : NumberField.idealUnder (↥E) P lies_over p

Equations

• ⋯ = ⋯

theorem NumberField.ideal_comap_intermediateField {K : Type u_13} {L : Type u_14} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [P lies_over p] (E : IntermediateField K L) : p = NumberField.idealUnder K (NumberField.idealUnder (↥E) P)

instance NumberField.IntermediateField_ideal_unique_lies_over {K : Type u_15} {L : Type u_16} [Field K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [P unique_lies_over p] (E : IntermediateField K L) : NumberField.idealUnder (↥E) P unique_lies_over p

Equations

• ⋯ = ⋯

instance NumberField.instLiesOverRingOfIntegers_galoisRamification {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : P lies_over p] : P.LiesOver p

Equations

• ⋯ = ⋯

Galois group Gal(K/L) acts transitively on the set of all maximal ideals

theorem NumberField.mapAlgEquiv_toAlgHom_toRingHom_eq_mapRingHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) : (↑(NumberField.RingOfIntegers.mapAlgEquiv σ)).toRingHom = NumberField.RingOfIntegers.mapRingHom σ

theorem NumberField.mapRingHom_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : NumberField.RingOfIntegers.mapRingHom 1 = RingHom.id (NumberField.RingOfIntegers L)

theorem NumberField.mapRingHom_symm_comp_mapRingHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) : (NumberField.RingOfIntegers.mapRingHom σ.symm).comp (NumberField.RingOfIntegers.mapRingHom σ) = RingHom.id (NumberField.RingOfIntegers L)

theorem NumberField.mapRingHom_symm_apply_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) (x : NumberField.RingOfIntegers L) : (NumberField.RingOfIntegers.mapRingHom σ.symm) ((NumberField.RingOfIntegers.mapRingHom σ) x) = x

theorem NumberField.mapRingHom_comp_mapRingHom_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) : (NumberField.RingOfIntegers.mapRingHom σ).comp (NumberField.RingOfIntegers.mapRingHom σ.symm) = RingHom.id (NumberField.RingOfIntegers L)

theorem NumberField.mapRingHom_apply_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) (x : NumberField.RingOfIntegers L) : (NumberField.RingOfIntegers.mapRingHom σ) ((NumberField.RingOfIntegers.mapRingHom σ.symm) x) = x

theorem NumberField.mapRingEquiv_symm_apply_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) (x : NumberField.RingOfIntegers L) : (NumberField.RingOfIntegers.mapRingEquiv σ.symm) ((NumberField.RingOfIntegers.mapRingEquiv σ) x) = x

theorem NumberField.mapRingEquiv_apply_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) (x : NumberField.RingOfIntegers L) : (NumberField.RingOfIntegers.mapRingEquiv σ) ((NumberField.RingOfIntegers.mapRingEquiv σ.symm) x) = x

instance NumberField.mapRingHom_map.isMaximal {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [hpm : P.IsMaximal] (σ : L ≃ₐ[K] L) : (Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P).IsMaximal

The mapRingHom σ will send a maximal ideal to a maximal ideal.

Equations

• ⋯ = ⋯

theorem NumberField.isMaximal_conjugates {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [hpm : P.IsMaximal] [hp : P lies_over p] (Q : Ideal (NumberField.RingOfIntegers L)) [hqm : Q.IsMaximal] [hq : Q lies_over p] [IsGalois K L] : ∃ (σ : L ≃ₐ[K] L), Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P = Q

The Galois group Gal(K/L) acts transitively on the set of all maximal ideals P of 𝓞 L lying above p, i.e., these prime ideals are all conjugates of each other.

theorem NumberField.IsMaximal_conjugates' {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {P : Ideal (NumberField.RingOfIntegers L)} [P.IsMaximal] {Q : Ideal (NumberField.RingOfIntegers L)} [Q.IsMaximal] [IsGalois K L] (h : NumberField.idealUnder K P = NumberField.idealUnder K Q) : ∃ (σ : L ≃ₐ[K] L), Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P = Q

theorem NumberField.normalizedFactors_map_mapRingHom_commutes {K : Type u_3} {L : Type u_4} [Field K] [Field L] [NumberField L] [Algebra K L] {I : Ideal (NumberField.RingOfIntegers L)} (hI : I ≠ ⊥) (σ : L ≃ₐ[K] L) : UniqueFactorizationMonoid.normalizedFactors (Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) I) = Multiset.map (Ideal.map (NumberField.RingOfIntegers.mapRingHom σ)) (UniqueFactorizationMonoid.normalizedFactors I)

The function normalizedFactors commutes with the function map (mapRingHom σ).

theorem NumberField.ideal_map_invariant_under_mapRingHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (σ : L ≃ₐ[K] L) : Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) (Ideal.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p) = Ideal.map (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p

The image of an ideal under the algebraMap between ring of integers remains invariant under the action of mapRingHom σ.

theorem NumberField.mapRingHom_IdealMap.injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (σ : L ≃ₐ[K] L) : Function.Injective (Ideal.map (NumberField.RingOfIntegers.mapRingHom σ))

The map induced by mapRingHom σ on the ideals of 𝓞 L is injective.

theorem NumberField.ramificationIdx_eq_of_isGalois {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (Q : Ideal (NumberField.RingOfIntegers L)) [hqm : Q.IsMaximal] [Q lies_over p] [IsGalois K L] : Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p P = Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p Q

In the case of Galois extension, all the ramificationIdx are the same.

theorem NumberField.ramificationIdx_eq_of_isGalois' {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {P : Ideal (NumberField.RingOfIntegers L)} [P.IsMaximal] {Q : Ideal (NumberField.RingOfIntegers L)} [hqm : Q.IsMaximal] (h : NumberField.idealUnder K P = NumberField.idealUnder K Q) : Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (NumberField.idealUnder K P) P = Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (NumberField.idealUnder K Q) Q

theorem NumberField.idealUnder_invariant_under_mapRingHom {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : P lies_over p] (σ : L ≃ₐ[K] L) : p = NumberField.idealUnder K (Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P)

instance NumberField.mapRingHom_map_lies_over {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [hp : P lies_over p] (σ : L ≃ₐ[K] L) : Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P lies_over p

Equations

• ⋯ = ⋯

def NumberField.residueField_mapAlgEquiv {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] {P : Ideal (NumberField.RingOfIntegers L)} [P.IsMaximal] [P lies_over p] {Q : Ideal (NumberField.RingOfIntegers L)} [Q.IsMaximal] [Q lies_over p] {σ : L ≃ₐ[K] L} (hs : Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P = Q) : (NumberField.RingOfIntegers L ⧸ P) ≃ₐ[NumberField.RingOfIntegers K ⧸ p] NumberField.RingOfIntegers L ⧸ Q

The algebra equiv ((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ map (mapRingHom σ) P) induced by an algebra equiv σ : L ≃ₐ[K] L.

Equations

• NumberField.residueField_mapAlgEquiv p hs = { toEquiv := (P.quotientEquiv Q ↑(NumberField.RingOfIntegers.mapAlgEquiv σ) ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

theorem NumberField.inertiaDeg_eq_of_isGalois {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsMaximal] [Q lies_over p] [IsGalois K L] : Ideal.inertiaDeg (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p P = Ideal.inertiaDeg (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p Q

In the case of Galois extension, all the inertiaDeg are the same.

@[irreducible]

noncomputable def NumberField.ramificationIdx_of_isGalois {K : Type u_3} [Field K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_5) [Field L] [NumberField L] [Algebra K L] : ℕ

In the case of Galois extension, it can be seen from the Theorem ramificationIdx_eq_of_IsGalois that all ramificationIdx are the same, which we define as the ramificationIdx_of_isGalois.

Equations

• NumberField.ramificationIdx_of_isGalois p L = Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p (Classical.choose ⋯)

@[irreducible]

noncomputable def NumberField.inertiaDeg_of_isGalois {K : Type u_3} [Field K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_5) [Field L] [NumberField L] [Algebra K L] : ℕ

In the case of Galois extension, it can be seen from the Theorem inertiaDeg_eq_of_IsGalois that all inertiaDeg are the same, which we define as the inertiaDeg_of_isGalois.

Equations

• NumberField.inertiaDeg_of_isGalois p L = Ideal.inertiaDeg (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p (Classical.choose ⋯)

theorem NumberField.ramificationIdx_eq_ramificationIdx_of_isGalois {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p P = NumberField.ramificationIdx_of_isGalois p L

In the case of Galois extension, all ramification indices are equal to the ramificationIdx_of_isGalois. This completes the property mentioned in our previous definition.

theorem NumberField.inertiaDeg_eq_inertiaDeg_of_isGalois {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Ideal.inertiaDeg (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) p P = NumberField.inertiaDeg_of_isGalois p L

In the case of Galois extension, all inertia degrees are equal to the inertiaDeg_of_isGalois. This completes the property mentioned in our previous definition.

theorem NumberField.ramificationIdx_mul_inertiaDeg_of_isGalois {K : Type u_3} [Field K] [NumberField K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_5) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : (NumberField.primes_over p L).card * (NumberField.ramificationIdx_of_isGalois p L * NumberField.inertiaDeg_of_isGalois p L) = Module.finrank K L

The form of the fundamental identity in the case of Galois extension.

decomposition Group

instance NumberField.Gal_MulAction_primes {K : Type u_3} [Field K] [NumberField K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] (L : Type u_5) [Field L] [NumberField L] [Algebra K L] : MulAction (L ≃ₐ[K] L) { x : Ideal (NumberField.RingOfIntegers L) // x ∈ NumberField.primes_over p L }

The MulAction of the Galois group L ≃ₐ[K] L on the set primes_over p L, given by σ ↦ (P ↦ σ P).

Equations

• NumberField.Gal_MulAction_primes p L = MulAction.mk ⋯ ⋯

theorem NumberField.Gal_MulAction_primes_mk_coe {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (σ : L ≃ₐ[K] L) : ↑(σ • NumberField.primes_over.mk p P) = Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P

def NumberField.decompositionGroup {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : Subgroup (L ≃ₐ[K] L)

The decomposition group of P over K, is the stabilizer of primes_over.mk p P under the action Gal_MulAction_primes.

Equations

• NumberField.decompositionGroup p P = MulAction.stabilizer (L ≃ₐ[K] L) (NumberField.primes_over.mk p P)

theorem NumberField.decompositionGroup_mem {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (σ : L ≃ₐ[K] L) : σ ∈ NumberField.decompositionGroup p P ↔ Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P = P

The decompositionGroup is consisting of all elements of the Galois group L ≃ₐ[K] L such that keep P invariant.

def NumberField.decompositionField {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : IntermediateField K L

The decomposition field of P over K is the fixed field of decompositionGroup p P.

Equations

• NumberField.decompositionField p P = IntermediateField.fixedField (NumberField.decompositionGroup p P)

instance NumberField.decompositionField_NumberField {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : NumberField ↥(NumberField.decompositionField p P)

decompositionField is a Number Field.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev NumberField.decompositionIdeal {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : Ideal (NumberField.RingOfIntegers ↥(NumberField.decompositionField p P))

The ideal equal to the intersection of P and decompositionField p P.

Equations

• NumberField.decompositionIdeal p P = NumberField.idealUnder (↥(NumberField.decompositionField p P)) P

instance NumberField.decompositionIdeal.isMaximal {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : (NumberField.decompositionIdeal p P).IsMaximal

Equations

• ⋯ = ⋯

theorem NumberField.decompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Fintype.card ↥(NumberField.decompositionGroup p P) = NumberField.ramificationIdx_of_isGalois p L * NumberField.inertiaDeg_of_isGalois p L

theorem NumberField.finrank_over_decompositionField_eq_ramificationIdx_mul_inertiaDeg {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Module.finrank (↥(NumberField.decompositionField p P)) L = NumberField.ramificationIdx_of_isGalois p L * NumberField.inertiaDeg_of_isGalois p L

theorem NumberField.isMaximal_lies_over_decompositionideal_unique {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (Q : Ideal (NumberField.RingOfIntegers L)) [Q.IsMaximal] [Q lies_over NumberField.decompositionIdeal p P] [IsGalois K L] : Q = P

P is the unique ideal lying over decompositionIdeal p P.

instance NumberField.unique_lies_over_decompositionIdeal {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : P unique_lies_over NumberField.decompositionIdeal p P

The instance form of isMaximal_lies_over_decompositionideal_unique.

Equations

• ⋯ = ⋯

theorem NumberField.primes_over_decompositionideal_card_eq_one {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : (NumberField.primes_over (NumberField.decompositionIdeal p P) L).card = 1

An alternative statement of isMaximal_lies_over_decompositionideal_unique.

theorem NumberField.ramificationIdx_of_decompositionIdeal {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : NumberField.ramificationIdx_of_isGalois (NumberField.decompositionIdeal p P) L = NumberField.ramificationIdx_of_isGalois p L

theorem NumberField.inertiaDeg_of_decompositionIdeal {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : NumberField.inertiaDeg_of_isGalois (NumberField.decompositionIdeal p P) L = NumberField.inertiaDeg_of_isGalois p L

theorem NumberField.ramificationIdx_of_decompositionideal_over_bot_eq_one {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Ideal.ramificationIdx (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers ↥(NumberField.decompositionField p P))) p (NumberField.decompositionIdeal p P) = 1

theorem NumberField.inertiaDeg_of_decompositionideal_over_bot_eq_one {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Ideal.inertiaDeg (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers ↥(NumberField.decompositionField p P))) p (NumberField.decompositionIdeal p P) = 1

The residue class field corresponding to decompositionField p P is isomorphic to residue class field corresponding to p.

inertia Group

noncomputable instance NumberField.residue_field_instFintype {K : Type u_3} [Field K] [NumberField K] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] : Finite (NumberField.RingOfIntegers K ⧸ p)

The residue class field of a number field is a finite field.

Equations

• ⋯ = ⋯

instance NumberField.extension_of_residue_fields_instIsGalois {K : Type u_3} {L : Type u_4} [Field K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : IsGalois (NumberField.RingOfIntegers K ⧸ p) (NumberField.RingOfIntegers L ⧸ P)

The extension between residue class fields of number fields is a Galois extension.

Equations

• ⋯ = ⋯

def NumberField.inertiaGroup (K : Type u_5) {L : Type u_6} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) : Subgroup (L ≃ₐ[K] L)

The inertia group of P over K is the subgorup of L ≃ₐ[K] L that consists of all the σ : L ≃ₐ[K] L that are identity modulo P.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.inertiaGroup_le_decompositionGroup {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : NumberField.inertiaGroup K P ≤ NumberField.decompositionGroup p P

theorem NumberField.mapRingHom_map_eq_of_unique_lies_over {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] [hp : P unique_lies_over p] (σ : L ≃ₐ[K] L) : Ideal.map (NumberField.RingOfIntegers.mapRingHom σ) P = P

If P is the unique ideal lying over p, then P remains invariant under the action of σ.

def NumberField.residueGaloisHom {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : (L ≃ₐ[K] L) →* (NumberField.RingOfIntegers L ⧸ P) ≃ₐ[NumberField.RingOfIntegers K ⧸ p] NumberField.RingOfIntegers L ⧸ P

If P is the unique ideal lying over p, then the action of each element σ in L ≃ₐ[K] L on the residue class field is an an automorphism of (𝓞 L) ⧸ P fixing (𝓞 K) ⧸ p, inducing a homomorphism from L ≃ₐ[K] L to the Galois group ((𝓞 L) ⧸ P) ≃ₐ[(𝓞 K) ⧸ p] ((𝓞 L) ⧸ P).

Equations

• NumberField.residueGaloisHom p P = { toFun := fun (σ : L ≃ₐ[K] L) => NumberField.residueField_mapAlgEquiv p ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

noncomputable abbrev NumberField.powerBasis_of_residue {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : PowerBasis (NumberField.RingOfIntegers K ⧸ p) (NumberField.RingOfIntegers L ⧸ P)

Equations

• NumberField.powerBasis_of_residue p P = Field.powerBasisOfFiniteOfSeparable (NumberField.RingOfIntegers K ⧸ p) (NumberField.RingOfIntegers L ⧸ P)

theorem NumberField.residueGaloisHom_surjective {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [hn : Normal K L] : Function.Surjective ⇑(NumberField.residueGaloisHom p P)

theorem NumberField.inertiaGroup_eq_ker {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : NumberField.inertiaGroup K P = (NumberField.residueGaloisHom p P).ker

If P is the unique ideal lying over p, then the inertiaGroup is equal to the kernel of the homomorphism residueGaloisHom.

theorem NumberField.inertiaGroup_normal {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : (NumberField.inertiaGroup K P).Normal

If P is the unique ideal lying over p, then the inertiaGroup K P is a normal subgroup.

noncomputable def NumberField.aut_quoutient_inertiaGroup_equiv_residueField_aut {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [Normal K L] : (L ≃ₐ[K] L) ⧸ NumberField.inertiaGroup K P ≃* (NumberField.RingOfIntegers L ⧸ P) ≃ₐ[NumberField.RingOfIntegers K ⧸ p] NumberField.RingOfIntegers L ⧸ P

Equations

• One or more equations did not get rendered due to their size.

def NumberField.inertiaFieldAux (K : Type u_7) {L : Type u_8} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : IntermediateField K L

The intermediate field fixed by inertiaGroup K P.

Equations

• NumberField.inertiaFieldAux K P = IntermediateField.fixedField (NumberField.inertiaGroup K P)

instance NumberField.inertiaField_NumberField {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : NumberField ↥(NumberField.inertiaFieldAux K P)

inertiaFieldAux K P is a Number Field.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev NumberField.inertiaIdealAux (K : Type u_7) {L : Type u_8} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : Ideal (NumberField.RingOfIntegers ↥(NumberField.inertiaFieldAux K P))

The ideal equal to the intersection of P and inertiaFieldAux p P.

Equations

• NumberField.inertiaIdealAux K P = NumberField.idealUnder (↥(NumberField.inertiaFieldAux K P)) P

instance NumberField.inertiaideal_IsMaxiaml {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : (NumberField.inertiaIdealAux K P).IsMaximal

inertiaIdealAux p P is a maximal Ideal.

Equations

• ⋯ = ⋯

theorem NumberField.inertiaField_isGalois_of_unique {K : Type u_7} {L : Type u_8} [Field K] [Field L] [Algebra K L] [IsGalois K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P unique_lies_over p] : IsGalois K ↥(NumberField.inertiaFieldAux K P)

(inertiaFieldAux p P) / K is a Galois extension.

noncomputable def NumberField.inertiaField_aut_equiv_ResidueField_aut {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : (↥(NumberField.inertiaFieldAux K P) ≃ₐ[K] ↥(NumberField.inertiaFieldAux K P)) ≃* (NumberField.RingOfIntegers L ⧸ P) ≃ₐ[NumberField.RingOfIntegers K ⧸ p] NumberField.RingOfIntegers L ⧸ P

The Galois group Gal((inertiaFieldAux p P) / K) is isomorphic to the Galois group Gal((𝓞 L) ⧸ P) / (𝓞 K) ⧸ p).

Equations

• One or more equations did not get rendered due to their size.

def NumberField.inertiaField_aut_tower_top_equiv_inertiaGroup_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : (L ≃ₐ[↥(NumberField.inertiaFieldAux K P)] L) ≃* ↥(NumberField.inertiaGroup K P)

The Galois group Gal(L / (inertiaFieldAux p P)) is isomorphic to inertiaGroup K P.

Equations

• NumberField.inertiaField_aut_tower_top_equiv_inertiaGroup_of_unique P = IntermediateField.subgroup_equiv_aut (NumberField.inertiaGroup K P)

theorem NumberField.finrank_eq_ramificationIdx_mul_inertiaDeg {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) [p.IsMaximal] [IsGalois K L] (P : Ideal (NumberField.RingOfIntegers L)) [P unique_lies_over p] : Module.finrank K L = NumberField.ramificationIdx_of_isGalois p L * NumberField.inertiaDeg_of_isGalois p L

The extension degree [L : K] is equal to the product of the ramification index and the inertia degree of p in L.

theorem NumberField.finrank_bot_inertiaField_eq_inertiaDeg_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Module.finrank K ↥(NumberField.inertiaFieldAux K P) = NumberField.inertiaDeg_of_isGalois p L

The extension degree [inertiaFieldAux p P : K] is equal to the inertia degree of p in L.

theorem NumberField.finrank_inertiaField_top_eq_ramificationIdx_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Module.finrank (↥(NumberField.inertiaFieldAux K P)) L = NumberField.ramificationIdx_of_isGalois p L

The extension degree [L : inertiaFieldAux p P] is equal to the ramification index of p in L.

theorem NumberField.inertiaGroup_card_eq_ramificationIdx_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Fintype.card ↥(NumberField.inertiaGroup K P) = NumberField.ramificationIdx_of_isGalois p L

theorem NumberField.inertiaGroup_inertiaideal_top (K : Type u_7) {L : Type u_8} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] : NumberField.inertiaGroup (↥(NumberField.inertiaFieldAux K P)) P = ⊤

theorem NumberField.inertiaDeg_over_inertiaideal_eq_one_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [P.IsMaximal] [P unique_lies_over p] : NumberField.inertiaDeg_of_isGalois (NumberField.inertiaIdealAux K P) L = 1

theorem NumberField.ramificationIdx_over_inertiaideal_eq_ramificationIdx_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : NumberField.ramificationIdx_of_isGalois (NumberField.inertiaIdealAux K P) L = NumberField.ramificationIdx_of_isGalois p L

theorem NumberField.ramificationIdx_below_inertiaideal_eq_one_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : NumberField.ramificationIdx_of_isGalois p ↥(NumberField.inertiaFieldAux K P) = 1

theorem NumberField.inertiaDeg_below_inertiaideal_eq_inertiaDeg_of_unique {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : NumberField.inertiaDeg_of_isGalois p ↥(NumberField.inertiaFieldAux K P) = NumberField.inertiaDeg_of_isGalois p L

theorem NumberField.inertiaGroup_eq {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : Subgroup.map (IntermediateField.subgroup_equiv_aut (NumberField.decompositionGroup p P)).symm.toMonoidHom ((NumberField.inertiaGroup K P).subgroupOf (NumberField.decompositionGroup p P)) = NumberField.inertiaGroup (↥(NumberField.decompositionField p P)) P

def NumberField.inertiaGroup_equiv {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : ↥(NumberField.inertiaGroup (↥(NumberField.decompositionField p P)) P) ≃* ↥(NumberField.inertiaGroup K P)

Equations

• One or more equations did not get rendered due to their size.

def NumberField.inertiaField {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : IntermediateField (↥(NumberField.decompositionField p P)) L

The intertia field of P over K is the intermediate field of L / decompositionField p P fixed by the inertia group pf P over K.

Equations

• NumberField.inertiaField p P = IntermediateField.fixedField (NumberField.inertiaGroup (↥(NumberField.decompositionField p P)) P)

@[reducible, inline]

abbrev NumberField.inertiaIdeal {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : Ideal (NumberField.RingOfIntegers ↥(NumberField.inertiaField p P))

The ideal equal to the intersection of P and inertiaField p P.

Equations

• NumberField.inertiaIdeal p P = NumberField.idealUnder (↥(NumberField.inertiaField p P)) P

instance NumberField.inertiaField_isGalois {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : IsGalois ↥(NumberField.decompositionField p P) ↥(NumberField.inertiaField p P)

(inertiaField p P) / (decompositionField p P) is a Galois extension.

Equations

• ⋯ = ⋯

def NumberField.inertiaField_aut_tower_top_equiv_inertiaGroup {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : (L ≃ₐ[↥(NumberField.inertiaField p P)] L) ≃* ↥(NumberField.inertiaGroup K P)

The Galois group Gal(L / (inertiaField p P)) is isomorphic to inertiaGroup K P.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.finrank_bot_inertiaField_eq_inertiaDeg {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : Module.finrank ↥(NumberField.decompositionField p P) ↥(NumberField.inertiaField p P) = NumberField.inertiaDeg_of_isGalois p L

The extension degree [inertiaField p P : K] is equal to the inertia degree of p in L.

theorem NumberField.finrank_inertiaField_top_eq_ramificationIdx {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : Module.finrank (↥(NumberField.inertiaField p P)) L = NumberField.ramificationIdx_of_isGalois p L

The extension degree [L : inertiaField p P] is equal to the ramification index of p in L.

theorem NumberField.inertiaGroup_card_eq_ramificationIdx {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : Fintype.card ↥(NumberField.inertiaGroup K P) = NumberField.ramificationIdx_of_isGalois p L

theorem NumberField.inertiaDeg_over_inertiaideal_eq_one {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : NumberField.inertiaDeg_of_isGalois (NumberField.inertiaIdeal p P) L = 1

theorem NumberField.ramificationIdx_over_inertiaideal_eq_ramificationIdx {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : NumberField.ramificationIdx_of_isGalois (NumberField.inertiaIdeal p P) L = NumberField.ramificationIdx_of_isGalois p L

theorem NumberField.ramificationIdx_below_inertiaideal_eq_one {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : NumberField.ramificationIdx_of_isGalois (NumberField.decompositionIdeal p P) ↥(NumberField.inertiaField p P) = 1

theorem NumberField.inertiaDeg_below_inertiaideal_eq_inertiaDeg {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : NumberField.inertiaDeg_of_isGalois (NumberField.decompositionIdeal p P) ↥(NumberField.inertiaField p P) = NumberField.inertiaDeg_of_isGalois p L

noncomputable def NumberField.inertiaField_decompositionField_aut_equiv_ResidueField_aut {K : Type u_5} {L : Type u_6} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (NumberField.RingOfIntegers K)) (P : Ideal (NumberField.RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : (↥(NumberField.inertiaField p P) ≃ₐ[↥(NumberField.decompositionField p P)] ↥(NumberField.inertiaField p P)) ≃* (NumberField.RingOfIntegers L ⧸ P) ≃ₐ[NumberField.RingOfIntegers K ⧸ p] NumberField.RingOfIntegers L ⧸ P

Equations

• One or more equations did not get rendered due to their size.