LeanPool.Neukirch.HilbertRamificationTheory

Imported Lean Pool material for LeanPool.Neukirch.HilbertRamificationTheory.

def IntermediateField.subgroupEquivAut {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (H : Subgroup Gal(L/K)) : Gal(L/↥(fixedField H)) ≃* ↥H

If H is a subgroup of Gal(L/K), then Gal(L / fixedField H) is isomorphic to H.

Equations

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

noncomputable def AlgHom.fieldRangeToAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (σ : ↥E →ₐ[K] L) : ↥E ≃ₐ[K] ↥σ.fieldRange

The AlgEquiv induced by an AlgHom from the domain of definition to the fieldRange.

Equations

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

theorem AlgEquiv.liftNormal_intermediateField_commutes {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [Normal K L] {E F : IntermediateField K L} (σ : ↥E ≃ₐ[K] ↥F) (x : ↥E) : (σ.liftNormal L) ↑x = ↑(σ x)

noncomputable def IsGalois.normalAutEquivQuotientSymm {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] (H : Subgroup Gal(L/K)) [H.Normal] : Gal(↥(IntermediateField.fixedField H)/K) ≃* Gal(L/K) ⧸ H

If H is a normal Subgroup of Gal(L/K), then Gal(fixedField H/K) is isomorphic to Gal(L/K)⧸H.

Equations

• IsGalois.normalAutEquivQuotientSymm H = (IsGalois.normalAutEquivQuotient H).symm

theorem Polynomial.isIntegralClosure_root_eq_ofMonic {R : Type u_1} (S : Type u_2) (L : Type u_3) [CommRing R] [CommRing S] [IsDomain S] [CommRing L] [IsDomain L] [Algebra R L] [Algebra S L] [Algebra R S] [IsScalarTower R S L] [IsIntegralClosure S R L] {p : Polynomial R} (hp : p.Monic) : Multiset.map (⇑(algebraMap S L)) (map (algebraMap R S) p).roots = (map (algebraMap R L) p).roots

If L be an extension of R, then for a monic polynomial p : R[X], the roots of p in L are equal to the roots of p in the integral closure of R in L.

theorem Polynomial.isIntegralClosure_root_card_eq_ofMonic {R : Type u_1} (S : Type u_2) (L : Type u_3) [CommRing R] [CommRing S] [IsDomain S] [CommRing L] [IsDomain L] [Algebra R L] [Algebra S L] [Algebra R S] [IsScalarTower R S L] [IsIntegralClosure S R L] {p : Polynomial R} (hp : p.Monic) : (map (algebraMap R S) p).roots.card = (map (algebraMap R L) p).roots.card

If L be an extension of R, then for a monic polynomial p : R[X], the number of roots of p in L is equal to the number of roots of p in the integral closure of R in L.

theorem Polynomial.roots_map_of_card_eq_natDegree {A : Type u_4} {B : Type u_5} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] {p : Polynomial A} {f : A →+* B} (h : map f p ≠ 0) (hroots : p.roots.card = p.natDegree) : Multiset.map (⇑f) p.roots = (map f p).roots

A variant of the theorem roots_map_of_injective_of_card_eq_natDegree that replaces the injectivity condition with the condition Polynomial.map f p ≠ 0.

theorem Ideal.IsPrime.prod_mem {R : Type u_1} {ι : Type u_2} [CommSemiring R] {p : Ideal R} [hp : p.IsPrime] {s : Finset ι} {x : ι → R} (h : ∏ i ∈ s, x i ∈ p) : ∃ (i : ↥s), x ↑i ∈ p

If the product of a finite number of elements in the commutative semiring R lies in the prime ideal p, then at least one of those elements is in p.

instance Ideal.instIsScalarTowerQuotientComapRingHomAlgebraMap_leanPool {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal S) : IsScalarTower R (R ⧸ comap (algebraMap R S) p) (S ⧸ p)

instance Ideal.quotient_finite_quotient_comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] (p : Ideal S) : Module.Finite (R ⧸ comap (algebraMap R S) p) (S ⧸ p)

If S is a finite R-module, then S ⧸ p is a finite R ⧸ comap (algebraMap R S) p-module.

@[reducible]

noncomputable def Int.Quotient.FintypeOfNeBot {p : Ideal ℤ} (hp : p ≠ ⊥) : Fintype (ℤ ⧸ p)

If p is a non-zero ideal of the ℤ, then ℤ ⧸ p is finite.

Equations

• Int.Quotient.FintypeOfNeBot hp = Fintype.ofEquiv (ZMod (Submodule.IsPrincipal.generator p).natAbs) ↑(⋯.mp (Submodule.IsPrincipal.generator p).quotientSpanEquivZMod).symm

@[implicit_reducible]

noncomputable instance Int.Quotient.FintypeOfIsMaximal (p : Ideal ℤ) [hpm : p.IsMaximal] : Fintype (ℤ ⧸ p)

In particular, if p is a maximal ideal of the ℤ, then ℤ ⧸ p is a finite field.

Equations

• Int.Quotient.FintypeOfIsMaximal p = Int.Quotient.FintypeOfNeBot ⋯

theorem NumberField.of_finite_extension (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [FiniteDimensional K L] : NumberField L

A finite extension of a number field is a number field.

instance NumberField.Extension_FiniteDimensional (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [Algebra K L] [NumberField L] : FiniteDimensional K L

Any extension of a Number Field is a finite extension.

instance NumberField.of_IntermediateField {K : Type u_3} {L : Type u_4} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (E : IntermediateField K L) : NumberField ↥E

instance NumberField.instIsScalarTowerRingOfIntegers_leanPool (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] : IsScalarTower (RingOfIntegers K) (RingOfIntegers L) L

theorem NumberField.ringOfIntegers_algebra_isIntegral (K : Type u_5) [Field K] : Algebra.IsIntegral ℤ (RingOfIntegers K)

theorem NumberField.isIntegral_tower {K : Type u_5} {L : Type u_6} [Field K] [Field L] [Algebra K L] (x : L) (hx : IsIntegral (RingOfIntegers K) x) : IsIntegral ℤ x

instance NumberField.extension_ringOfIntegers_isIntegralClosure (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [NumberField L] : IsIntegralClosure (RingOfIntegers L) (RingOfIntegers K) L

The instance form of theorem ringOfIntegers_eq_integralClosure.

instance NumberField.extension_ringOfIntegers_isIntegral (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [NumberField L] : Algebra.IsIntegral (RingOfIntegers K) (RingOfIntegers L)

Any Extension between ring of integers is integral.

instance NumberField.extension_ringOfIntegers_isNoetherian (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] : IsNoetherian (RingOfIntegers K) (RingOfIntegers L)

In particular, any Extension between ring of integers is noetherian.

theorem NumberField.algebraMap_ker_eq_bot (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] : RingHom.ker (algebraMap (RingOfIntegers K) (RingOfIntegers L)) = ⊥

The kernel of the algebraMap between ring of integers is ⊥.

theorem NumberField.algebraMap_injective_of_ringOfIntegers (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] : Function.Injective ⇑(algebraMap (RingOfIntegers K) (RingOfIntegers L))

The algebraMap between ring of integers is injective.

instance NumberField.instIsScalarTower_IntermediateField_ringOfIntegers (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) : IsScalarTower (RingOfIntegers K) (RingOfIntegers ↥E) (RingOfIntegers L)

instance NumberField.instIsScalarTower_ringOfIntegers (K : Type u_3) [Field K] (E : Type u_5) (L : Type u_6) [Field E] [NumberField E] [Field L] [NumberField L] [Algebra K E] [Algebra E L] [Algebra K L] [IsScalarTower K E L] : IsScalarTower (RingOfIntegers K) (RingOfIntegers E) (RingOfIntegers L)

@[reducible, inline]

abbrev NumberField.IdealBelow (K : Type u_3) [Field K] {L : Type u_5} [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : Ideal (RingOfIntegers K)

The ideal obtained by intersecting 𝓞 K and P.

Equations

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

theorem NumberField.IdealBelow_def (K : Type u_3) [Field K] {L : Type u_5} [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : IdealBelow K P = Ideal.comap (algebraMap (RingOfIntegers K) (RingOfIntegers L)) P

instance NumberField.IdealBelow_IsPrime (K : Type u_3) [Field K] {L : Type u_5} [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) [P.IsPrime] : (IdealBelow K P).IsPrime

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

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

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

def NumberField.term_Lies_over_ : Lean.TrailingParserDescr

P lies_over p means the prime p is the preimage of P under the canonical algebra map.

Equations

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

instance NumberField.over_IdealBelow {K : Type u_6} {L : Type u_7} [Field K] [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : P lies_over IdealBelow K P

theorem NumberField.over_def {K : Type u_6} {L : Type u_7} [Field K] [Field L] [Algebra K L] {p : Ideal (RingOfIntegers K)} {P : Ideal (RingOfIntegers L)} (h : p = IdealBelow K P) : P lies_over p

@[instance 100]

instance NumberField.instLiesOverRingOfIntegersOfIdeal_lies_over {K : Type u_8} {L : Type u_9} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [h : P lies_over p] : P.LiesOver p

Bridge the bespoke lies_over relation to Mathlib's Ideal.LiesOver, so that the Mathlib ramification/inertia API applies.

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

P is the unique maximal ideal lying over p: it lies over p and is equal to every maximal ideal lying over p.

• liesOver_eq : p = Ideal.comap (algebraMap (RingOfIntegers K) (RingOfIntegers L)) P
• unique (Q : Ideal (RingOfIntegers L)) [Q.IsMaximal] [Q lies_over p] : Q = P

  Every maximal ideal lying over p is equal to P.

def NumberField.term_Unique_lies_over_ : Lean.TrailingParserDescr

P unique_lies_over p means P is the unique maximal ideal lying over p.

Equations

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

instance NumberField.IdealBelow_IsMaximal {K : Type u_6} {L : Type u_7} [Field K] [Field L] [Algebra K L] [NumberField L] (P : Ideal (RingOfIntegers L)) [P.IsMaximal] : (IdealBelow K P).IsMaximal

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

instance NumberField.Ideal_comap_int_IsMaximal {K : Type u_6} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] : (Ideal.comap (algebraMap ℤ (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.

theorem NumberField.exists_ideal_over_maximal_of_ringOfIntegers {K : Type u_6} [Field K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_8) [Field L] [NumberField L] [Algebra K L] : ∃ (P : Ideal (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_6} [Field K] (p : Ideal (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_6} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_8) [Field L] [Algebra K L] : Ideal.map (algebraMap (RingOfIntegers K) (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_7} [Field L] [NumberField L] (P : Ideal (RingOfIntegers L)) : Prime P ↔ P.IsMaximal

@[reducible, inline]

noncomputable abbrev NumberField.primesOver {K : Type u_8} [Field K] (p : Ideal (RingOfIntegers K)) (L : Type u_9) [Field L] [NumberField L] [Algebra K L] : Finset (Ideal (RingOfIntegers L))

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

Equations

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

theorem NumberField.primesOver_mem {K : Type u_8} {L : Type u_9} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] : P ∈ primesOver p L ↔ P.IsMaximal ∧ P lies_over p

instance NumberField.primesOver_instIsMaximal {K : Type u_8} {L : Type u_9} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (Q : ↥(primesOver p L)) : (↑Q).IsMaximal

instance NumberField.primesOver_inst_lies_over {K : Type u_8} {L : Type u_9} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (Q : ↥(primesOver p L)) : ↑Q lies_over p

@[reducible, inline]

abbrev NumberField.primesOverMk {K : Type u_8} {L : Type u_9} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : ↥(primesOver p L)

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

Equations

• NumberField.primesOverMk p P = ⟨P, ⋯⟩

theorem NumberField.primesOver_card_ne_zero {K : Type u_8} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_10) [Field L] [NumberField L] [Algebra K L] : (primesOver p L).card ≠ 0

@[reducible, inline]

noncomputable abbrev NumberField.primesSameBleow {K : Type u_8} {L : Type u_9} [Field K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : Finset (Ideal (RingOfIntegers L))

The Finset consists of all primes lying over IdealBelow K P, i.e., all the primes Q such that IdealBelow K Q = IdealBelow K P.

Equations

• NumberField.primesSameBleow P = NumberField.primesOver (NumberField.IdealBelow K P) L

theorem NumberField.Nonsplit_iff_primesOver_card_eq_one {K : Type u_8} {L : Type u_9} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] : Ideal.Nonsplit (algebraMap (RingOfIntegers K) (RingOfIntegers L)) p ↔ (primesOver p L).card = 1

theorem NumberField.unique_lies_over_Nonsplit {K : Type u_10} {L : Type u_11} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [hp : P unique_lies_over p] : Ideal.Nonsplit (algebraMap (RingOfIntegers K) (RingOfIntegers L)) p

theorem NumberField.unique_primesOver_card_eq_one {K : Type u_8} {L : Type u_9} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (P : Ideal (RingOfIntegers L)) [P unique_lies_over p] : (primesOver p L).card = 1

Another form of the property unique_lies_over.

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

theorem NumberField.ideal_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] [NumberField E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (RingOfIntegers K)) (𝔓 : Ideal (RingOfIntegers E)) (P : Ideal (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] [NumberField L] [Algebra K L] {E : Type u_12} [Field E] [NumberField E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (RingOfIntegers K)) (𝔓 : Ideal (RingOfIntegers E)) (P : Ideal (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] [NumberField E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (RingOfIntegers K)) (𝔓 : Ideal (RingOfIntegers E)) (P : Ideal (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] [NumberField E] [Algebra K E] [Algebra E L] [IsScalarTower K E L] (p : Ideal (RingOfIntegers K)) (𝔓 : Ideal (RingOfIntegers E)) (P : Ideal (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] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [P lies_over p] (E : IntermediateField K L) : IdealBelow (↥E) P lies_over p

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

instance NumberField.IntermediateField_ideal_unique_lies_over {K : Type u_13} {L : Type u_14} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P unique_lies_over p] (E : IntermediateField K L) : IdealBelow (↥E) P unique_lies_over p

@[implicit_reducible]

instance NumberField.residueFieldInstAlgebra {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [hp : P lies_over p] : Algebra (RingOfIntegers K ⧸ p) (RingOfIntegers L ⧸ P)

If P lies over p, then the residue class field of p has a canonical map to the residue class field of P.

Equations

• NumberField.residueFieldInstAlgebra p P = Ideal.Quotient.algebraQuotientOfLEComap ⋯

instance NumberField.instIsScalarTowerRingOfIntegersQuotientIdeal_leanPool {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [hp : P lies_over p] : IsScalarTower (RingOfIntegers K) (RingOfIntegers K ⧸ p) (RingOfIntegers L ⧸ P)

instance NumberField.residue_field_instFiniteDimensional {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : FiniteDimensional (RingOfIntegers K ⧸ p) (RingOfIntegers L ⧸ P)

The extension between residue class fields is finite.

theorem NumberField.inertiaDeg_pos {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : p.inertiaDeg P > 0

def NumberField.mapRingHomOfClass {K : Type u_17} {L : Type u_18} {F : Type u_19} [Field K] [Field L] [FunLike F K L] [RingHomClass F K L] (f : F) : RingOfIntegers K →+* RingOfIntegers L

The ring homomorphism (𝓞 K) →+* (𝓞 L) induced by restricting any ring homomorphism f : K → L (given through a RingHomClass) to the rings of integers.

Equations

• NumberField.mapRingHomOfClass f = { toFun := fun (k : NumberField.RingOfIntegers K) => ⟨f ↑k, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def NumberField.mapAlgHomOfClass {k : Type u_17} {K : Type u_18} {L : Type u_19} {F : Type u_20} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [FunLike F K L] [AlgHomClass F k K L] (f : F) : RingOfIntegers K →ₐ[RingOfIntegers k] RingOfIntegers L

The algebra homomorphism (𝓞 K) →ₐ[𝓞 k] (𝓞 L) induced by restricting any algebra homomorphism f : K → L (given through an AlgHomClass) to the rings of integers.

Equations

• NumberField.mapAlgHomOfClass f = { toRingHom := NumberField.mapRingHomOfClass f, commutes' := ⋯ }

def NumberField.GalAlgEquiv {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : RingOfIntegers L ≃ₐ[RingOfIntegers K] RingOfIntegers L

The AlgEquiv of elements of Galois group Gal(K/L) restricted to 𝓞 L.

Equations

• NumberField.GalAlgEquiv σ = AlgEquiv.ofAlgHom (NumberField.mapAlgHomOfClass σ) (NumberField.mapAlgHomOfClass σ.symm) ⋯ ⋯

theorem NumberField.GalAlgEquiv_apply {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (x : RingOfIntegers L) : ↑((GalAlgEquiv σ) x) = σ ↑x

def NumberField.GalRingHom {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : RingOfIntegers L →+* RingOfIntegers L

Consider GalAlgEquiv σ as a ring homomorphism.

Equations

• NumberField.GalRingHom σ = (↑(NumberField.GalAlgEquiv σ)).toRingHom

theorem NumberField.GalAlgEquiv_toAlgHom_toRingHom_eq_GalRingHom {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : (↑(GalAlgEquiv σ)).toRingHom = GalRingHom σ

theorem NumberField.GalRingHom_mul {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ τ : Gal(L/K)) : (GalRingHom σ).comp (GalRingHom τ) = GalRingHom (σ * τ)

theorem NumberField.GalRingHom_one {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] : GalRingHom 1 = RingHom.id (RingOfIntegers L)

theorem NumberField.GalRingHom_inv_mul_cancel {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : (GalRingHom σ⁻¹).comp (GalRingHom σ) = RingHom.id (RingOfIntegers L)

theorem NumberField.GalRingHom_inv_mul_cancel_mem {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (x : RingOfIntegers L) : (GalRingHom σ⁻¹) ((GalRingHom σ) x) = x

theorem NumberField.GalRingHom_mul_inv_cancel {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : (GalRingHom σ).comp (GalRingHom σ⁻¹) = RingHom.id (RingOfIntegers L)

theorem NumberField.GalRingHom_mul_inv_cancel_mem {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) (x : RingOfIntegers L) : (GalRingHom σ) ((GalRingHom σ⁻¹) x) = x

instance NumberField.GalRingHom_map_isMaximal {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) [hpm : P.IsMaximal] (σ : Gal(L/K)) : (Ideal.map (GalRingHom σ) P).IsMaximal

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

theorem NumberField.IsMaximal_conjugates {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [hpm : P.IsMaximal] [hp : P lies_over p] (Q : Ideal (RingOfIntegers L)) [hqm : Q.IsMaximal] [hq : Q lies_over p] [IsGalois K L] : ∃ (σ : Gal(L/K)), Ideal.map (GalRingHom σ) 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_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] {P : Ideal (RingOfIntegers L)} [P.IsMaximal] {Q : Ideal (RingOfIntegers L)} [Q.IsMaximal] [IsGalois K L] (h : IdealBelow K P = IdealBelow K Q) : ∃ (σ : Gal(L/K)), Ideal.map (GalRingHom σ) P = Q

theorem NumberField.normalizedFactors_map_GalRingHom_commutes {K : Type u_17} {L : Type u_18} [Field K] [Field L] [NumberField L] [Algebra K L] {I : Ideal (RingOfIntegers L)} (hI : I ≠ ⊥) (σ : Gal(L/K)) : UniqueFactorizationMonoid.normalizedFactors (Ideal.map (GalRingHom σ) I) = Multiset.map (Ideal.map (GalRingHom σ)) (UniqueFactorizationMonoid.normalizedFactors I)

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

theorem NumberField.Ideal_map_invariant_under_GalRingHom {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (σ : Gal(L/K)) : Ideal.map (GalRingHom σ) (Ideal.map (algebraMap (RingOfIntegers K) (RingOfIntegers L)) p) = Ideal.map (algebraMap (RingOfIntegers K) (RingOfIntegers L)) p

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

theorem NumberField.GalRingHom_IdealMap_injective {K : Type u_15} {L : Type u_16} [Field K] [Field L] [Algebra K L] (σ : Gal(L/K)) : Function.Injective (Ideal.map (GalRingHom σ))

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

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

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

theorem NumberField.ramificationIdx_eq_of_isGalois' {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] {P : Ideal (RingOfIntegers L)} [P.IsMaximal] {Q : Ideal (RingOfIntegers L)} [hqm : Q.IsMaximal] (h : IdealBelow K P = IdealBelow K Q) : (IdealBelow K P).ramificationIdx P = (IdealBelow K Q).ramificationIdx Q

theorem NumberField.IdealBelow_invariant_under_GalRingHom {K : Type u_19} {L : Type u_20} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [hp : P lies_over p] (σ : Gal(L/K)) : p = IdealBelow K (Ideal.map (GalRingHom σ) P)

instance NumberField.GalRingHom_map_lies_over {K : Type u_17} {L : Type u_18} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [hp : P lies_over p] (σ : Gal(L/K)) : Ideal.map (GalRingHom σ) P lies_over p

def NumberField.residueFieldGalAlgEquiv {K : Type u_17} {L : Type u_18} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) {P : Ideal (RingOfIntegers L)} [P lies_over p] {Q : Ideal (RingOfIntegers L)} [Q lies_over p] {σ : Gal(L/K)} (hs : Ideal.map (GalRingHom σ) P = Q) : (RingOfIntegers L ⧸ P) ≃ₐ[RingOfIntegers K ⧸ p] RingOfIntegers L ⧸ Q

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

Equations

• NumberField.residueFieldGalAlgEquiv p hs = { toEquiv := (P.quotientEquiv Q (NumberField.GalAlgEquiv σ).toRingEquiv ⋯).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

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

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

noncomputable def NumberField.ramificationIdxOfIsGalois {K : Type u_17} [Field K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_19) [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 ramificationIdxOfIsGalois.

Equations

• NumberField.ramificationIdxOfIsGalois p L = p.ramificationIdx (Classical.choose ⋯)

noncomputable def NumberField.inertiaDegOfIsGalois {K : Type u_17} [Field K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_19) [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 inertiaDegOfIsGalois.

Equations

• NumberField.inertiaDegOfIsGalois p L = p.inertiaDeg (Classical.choose ⋯)

theorem NumberField.ramificationIdx_eq_ramificationIdxOfIsGalois {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : p.ramificationIdx P = ramificationIdxOfIsGalois p L

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

theorem NumberField.inertiaDeg_eq_inertiaDegOfIsGalois {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : p.inertiaDeg P = inertiaDegOfIsGalois p L

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

theorem NumberField.ramificationIdx_mul_inertiaDegOfIsGalois {K : Type u_17} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_19) [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : (primesOver p L).card * (ramificationIdxOfIsGalois p L * inertiaDegOfIsGalois p L) = Module.finrank K L

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

@[implicit_reducible]

instance NumberField.GalMulActionPrimes {K : Type u_17} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] (L : Type u_19) [Field L] [NumberField L] [Algebra K L] : MulAction Gal(L/K) ↥(primesOver p L)

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

Equations

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

theorem NumberField.GalMulActionPrimes_mk_coe {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (σ : Gal(L/K)) : ↑(σ • primesOverMk p P) = Ideal.map (GalRingHom σ) P

def NumberField.DecompositionGroup {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : Subgroup Gal(L/K)

The decomposition group of P over K, is the stabilizer of primesOverMk p P under the action GalMulActionPrimes.

Equations

• NumberField.DecompositionGroup p P = MulAction.stabilizer Gal(L/K) (NumberField.primesOverMk p P)

theorem NumberField.DecompositionGroup_mem {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (σ : Gal(L/K)) : σ ∈ DecompositionGroup p P ↔ Ideal.map (GalRingHom σ) 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_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (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_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : NumberField ↥(DecompositionField p P)

DecompositionField is a Number Field.

@[reducible, inline]

abbrev NumberField.DecompositionIdeal {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : Ideal (RingOfIntegers ↥(DecompositionField p P))

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

Equations

• NumberField.DecompositionIdeal p P = NumberField.IdealBelow (↥(NumberField.DecompositionField p P)) P

instance NumberField.DecompositionIdeal_isMaximal {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : (DecompositionIdeal p P).IsMaximal

theorem NumberField.DecompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Fintype.card ↥(DecompositionGroup p P) = ramificationIdxOfIsGalois p L * inertiaDegOfIsGalois p L

theorem NumberField.Extension_degree_over_DecompositionField_eq_ramificationIdx_mul_inertiaDeg {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Module.finrank (↥(DecompositionField p P)) L = ramificationIdxOfIsGalois p L * inertiaDegOfIsGalois p L

theorem NumberField.isMaximal_lies_over_DecompositionIdeal_unique {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] (Q : Ideal (RingOfIntegers L)) [Q.IsMaximal] [Q lies_over 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_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : P unique_lies_over DecompositionIdeal p P

The instance form of isMaximal_lies_over_DecompositionIdeal_unique.

instance NumberField.DecompositionIdeal_Nonsplit {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : Ideal.Nonsplit (algebraMap (RingOfIntegers ↥(DecompositionField p P)) (RingOfIntegers L)) (DecompositionIdeal p P)

theorem NumberField.primesOver_DecompositionIdeal_card_eq_one {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : (primesOver (DecompositionIdeal p P) L).card = 1

An alternative statement of isMaximal_lies_over_DecompositionIdeal_unique.

theorem NumberField.ramificationIdx_and_inertiaDeg_of_DecompositionIdeal {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : ramificationIdxOfIsGalois (DecompositionIdeal p P) L = ramificationIdxOfIsGalois p L ∧ inertiaDegOfIsGalois (DecompositionIdeal p P) L = inertiaDegOfIsGalois p L

theorem NumberField.ramificationIdx_of_DecompositionIdeal {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : ramificationIdxOfIsGalois (DecompositionIdeal p P) L = ramificationIdxOfIsGalois p L

theorem NumberField.inertiaDeg_of_DecompositionIdeal {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : inertiaDegOfIsGalois (DecompositionIdeal p P) L = inertiaDegOfIsGalois p L

theorem NumberField.ramificationIdx_of_DecompositionIdeal_over_bot_eq_one {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : p.ramificationIdx (DecompositionIdeal p P) = 1

theorem NumberField.inertiaDeg_of_DecompositionIdeal_over_bot_eq_one {K : Type u_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] [IsGalois K L] : p.inertiaDeg (DecompositionIdeal p P) = 1

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

instance NumberField.instFiniteQuotientIntIdealComapRingOfIntegersRingHomAlgebraMap_leanPool {K : Type u_17} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) : Module.Finite (ℤ ⧸ Ideal.comap (algebraMap ℤ (RingOfIntegers K)) p) (RingOfIntegers K ⧸ p)

@[implicit_reducible]

noncomputable instance NumberField.residueFieldInstFintype {K : Type u_17} [Field K] [NumberField K] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] : Fintype (RingOfIntegers K ⧸ p)

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

Equations

• NumberField.residueFieldInstFintype p = Fintype.ofFinite (NumberField.RingOfIntegers K ⧸ p)

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

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

def NumberField.InertiaGroup (K : Type u_19) {L : Type u_20} [Field K] [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : Subgroup Gal(L/K)

The inertia group of P over K is the subgroup 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_17} {L : Type u_18} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P lies_over p] : InertiaGroup K P ≤ DecompositionGroup p P

theorem NumberField.GalRingHom_map_eq_of_unique_lies_over {K : Type u_21} {L : Type u_22} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [P.IsMaximal] [hp : P unique_lies_over p] (σ : Gal(L/K)) : Ideal.map (GalRingHom σ) 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_19} {L : Type u_20} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [P.IsMaximal] [hp : P unique_lies_over p] : Gal(L/K) →* (RingOfIntegers L ⧸ P) ≃ₐ[RingOfIntegers K ⧸ p] 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 (σ : Gal(L/K)) => NumberField.residueFieldGalAlgEquiv p ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def NumberField.powerBasisOfResidue {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : PowerBasis (RingOfIntegers K ⧸ p) (RingOfIntegers L ⧸ P)

A power basis of the residue field extension ((𝓞 L) ⧸ P) / ((𝓞 K) ⧸ p), obtained because this extension is finite and separable.

Equations

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

theorem NumberField.ResidueGaloisHom_surjective {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [hn : Normal K L] : Function.Surjective ⇑(ResidueGaloisHom p P)

theorem NumberField.InertiaGroup_eq_ker {K : Type u_21} {L : Type u_22} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : InertiaGroup K P = (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_21} {L : Type u_22} [Field K] [Field L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] : (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.autQuoutientInertiaGroupEquivResidueFieldAut {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [Normal K L] : Gal(L/K) ⧸ InertiaGroup K P ≃* (RingOfIntegers L ⧸ P) ≃ₐ[RingOfIntegers K ⧸ p] RingOfIntegers L ⧸ P

The quotient of the Galois group by the inertia group is isomorphic to the Galois group of the residue field extension.

Equations

• NumberField.autQuoutientInertiaGroupEquivResidueFieldAut p P = (QuotientGroup.quotientMulEquivOfEq ⋯).trans (QuotientGroup.quotientKerEquivOfSurjective (NumberField.ResidueGaloisHom p P) ⋯)

def NumberField.InertiaField' (K : Type u_21) {L : Type u_22} [Field K] [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : IntermediateField K L

The intermediate field fixed by InertiaGroup K P.

Equations

• NumberField.InertiaField' K P = IntermediateField.fixedField (NumberField.InertiaGroup K P)

instance NumberField.InertiaField_NumberField {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : NumberField ↥(InertiaField' K P)

InertiaField' K P is a Number Field.

@[reducible, inline]

abbrev NumberField.InertiaIdeal' (K : Type u_21) {L : Type u_22} [Field K] [Field L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : Ideal (RingOfIntegers ↥(InertiaField' K P))

The ideal equal to the intersection of P and InertiaField' p P.

Equations

• NumberField.InertiaIdeal' K P = NumberField.IdealBelow (↥(NumberField.InertiaField' K P)) P

instance NumberField.InertiaIdeal_IsMaxiaml {K : Type u_19} {L : Type u_20} [Field K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (RingOfIntegers L)) [P.IsMaximal] : (InertiaIdeal' K P).IsMaximal

InertiaIdeal' p P is a maximal Ideal.

theorem NumberField.InertiaField_isGalois_of_unique {K : Type u_21} {L : Type u_22} [Field K] [Field L] [Algebra K L] [IsGalois K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P unique_lies_over p] : IsGalois K ↥(InertiaField' K P)

(InertiaField' p P) / K is a Galois extension.

noncomputable def NumberField.InertiaFieldAutEquivResidueFieldAut {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Gal(↥(InertiaField' K P)/K) ≃* (RingOfIntegers L ⧸ P) ≃ₐ[RingOfIntegers K ⧸ p] RingOfIntegers L ⧸ P

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

Equations

• NumberField.InertiaFieldAutEquivResidueFieldAut p P = (IsGalois.normalAutEquivQuotientSymm (NumberField.InertiaGroup K P)).trans (NumberField.autQuoutientInertiaGroupEquivResidueFieldAut p P)

def NumberField.InertiaFieldAutTowerTopEquivInertiaGroupOfUnique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (RingOfIntegers L)) : Gal(L/↥(InertiaField' K P)) ≃* ↥(InertiaGroup K P)

The Galois group Gal(L / (InertiaField' p P)) is isomorphic to InertiaGroup K P.

Equations

• NumberField.InertiaFieldAutTowerTopEquivInertiaGroupOfUnique P = IntermediateField.subgroupEquivAut (NumberField.InertiaGroup K P)

theorem NumberField.finrank_eq_ramificationIdx_mul_inertiaDeg {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) [p.IsMaximal] [IsGalois K L] (P : Ideal (RingOfIntegers L)) [P.IsMaximal] [P unique_lies_over p] : Module.finrank K L = ramificationIdxOfIsGalois p L * inertiaDegOfIsGalois 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_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Module.finrank K ↥(InertiaField' K P) = inertiaDegOfIsGalois 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_of_unique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Module.finrank (↥(InertiaField' K P)) L = ramificationIdxOfIsGalois 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_of_unique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : Fintype.card ↥(InertiaGroup K P) = ramificationIdxOfIsGalois p L

theorem NumberField.InertiaGroup_InertiaIdeal_top (K : Type u_21) {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (P : Ideal (RingOfIntegers L)) [P.IsMaximal] : InertiaGroup (↥(InertiaField' K P)) P = ⊤

theorem NumberField.inertiaDeg_over_InertiaIdeal_eq_one_of_unique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [P.IsMaximal] [P unique_lies_over p] : inertiaDegOfIsGalois (InertiaIdeal' K P) L = 1

theorem NumberField.ramificationIdx_over_InertiaIdeal_eq_ramificationIdx_of_unique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : ramificationIdxOfIsGalois (InertiaIdeal' K P) L = ramificationIdxOfIsGalois p L

theorem NumberField.ramificationIdx_below_InertiaIdeal_eq_one_of_unique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : ramificationIdxOfIsGalois p ↥(InertiaField' K P) = 1

theorem NumberField.InertiaDeg_below_InertiaIdeal_eq_inertiaDeg_of_unique {K : Type u_19} {L : Type u_20} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [hp : P unique_lies_over p] [IsGalois K L] : inertiaDegOfIsGalois p ↥(InertiaField' K P) = inertiaDegOfIsGalois p L

theorem NumberField.InertiaGroup_eq {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : Subgroup.map (IntermediateField.subgroupEquivAut (DecompositionGroup p P)).symm.toMonoidHom ((InertiaGroup K P).subgroupOf (DecompositionGroup p P)) = InertiaGroup (↥(DecompositionField p P)) P

def NumberField.InertiaGroupEquiv {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : ↥(InertiaGroup (↥(DecompositionField p P)) P) ≃* ↥(InertiaGroup K P)

The inertia group of P over the decomposition field is isomorphic to the inertia group of P over K.

Equations

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

def NumberField.InertiaField {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : IntermediateField (↥(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_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : Ideal (RingOfIntegers ↥(InertiaField p P))

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

Equations

• NumberField.InertiaIdeal p P = NumberField.IdealBelow (↥(NumberField.InertiaField p P)) P

instance NumberField.InertiaField_isGalois {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : IsGalois ↥(DecompositionField p P) ↥(InertiaField p P)

(InertiaField p P) / (DecompositionField p P) is a Galois extension.

def NumberField.InertiaFieldAutTowerTopEquivInertiaGroup {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] : Gal(L/↥(InertiaField p P)) ≃* ↥(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_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : Module.finrank ↥(DecompositionField p P) ↥(InertiaField p P) = inertiaDegOfIsGalois 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_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : Module.finrank (↥(InertiaField p P)) L = ramificationIdxOfIsGalois 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_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : Fintype.card ↥(InertiaGroup K P) = ramificationIdxOfIsGalois p L

theorem NumberField.inertiaDeg_over_InertiaIdeal_eq_one {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : inertiaDegOfIsGalois (InertiaIdeal p P) L = 1

theorem NumberField.ramificationIdx_over_InertiaIdeal_eq_ramificationIdx {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : ramificationIdxOfIsGalois (InertiaIdeal p P) L = ramificationIdxOfIsGalois p L

theorem NumberField.ramificationIdx_below_InertiaIdeal_eq_one {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : ramificationIdxOfIsGalois (DecompositionIdeal p P) ↥(InertiaField p P) = 1

theorem NumberField.InertiaDeg_below_InertiaIdeal_eq_inertiaDeg {K : Type u_21} {L : Type u_22} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (p : Ideal (RingOfIntegers K)) (P : Ideal (RingOfIntegers L)) [p.IsMaximal] [P.IsMaximal] [P lies_over p] [IsGalois K L] : inertiaDegOfIsGalois (DecompositionIdeal p P) ↥(InertiaField p P) = inertiaDegOfIsGalois p L