Skip to content

Decomposition and inertia groups

9 fully proved

Subgroup

TheoremEqual cardinality of an intersection forces containment#✓fully proved

Let \(H\) and \(K\) be subgroups of a group \(G\) with \(H\) finite. If \(H \cap K\) has as many elements as \(H\), then \(H \le K\).

theorem le_of_card_subgroupOf_eq {G : Type*} [Group G] {H K : Subgroup G}
    [Finite H]
    (h : Nat.card (H.subgroupOf K) = Nat.card H) :
    H ≤ K
Used by 2
Used byRamification index one and the inertia group · Ramification index and inertia degree one and the decomposition group

Ideal

TheoremTower formula for inertia groups#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. For a subgroup \(S \le G\) write \(I_S(\mathfrak P)\) for the inertia group of \(\mathfrak P\) in \(S\), the set of \(\sigma \in S\) with \(\sigma(x) - x \in \mathfrak P\) for all \(x \in B\). Then \(e(\mathfrak P_E \mid \mathfrak p) \cdot |I_H(\mathfrak P)| = |I_G(\mathfrak P)|\), where \(e(\mathfrak P_E \mid \mathfrak p)\) is the ramification index of \(\mathfrak P_E\) over \(\mathfrak p\).

Ideal.card_inertia_tower_formula · 24 lines 
theorem card_inertia_tower_formula
    {K L : Type*} {B : Type*} [Field K] [Field L] [Algebra K L]
    [CommRing B] [MulSemiringAction (L ≃ₐ[K] L) B]
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    P_E.ramificationIdx A *
      Nat.card (P.inertia (↥E.fixingSubgroup)) =
    Nat.card (P.inertia (L ≃ₐ[K] L))
Used by 1
Used byTower formula for inertia groups, intersected with the fixing group

TheoremTower formula for inertia groups, intersected with the fixing group#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(I(\mathfrak P)\) be the inertia group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(x) - x \in \mathfrak P\) for all \(x \in B\). Then \(e(\mathfrak P_E \mid \mathfrak p) \cdot |I(\mathfrak P) \cap H| = |I(\mathfrak P)|\), where \(e(\mathfrak P_E \mid \mathfrak p)\) is the ramification index of \(\mathfrak P_E\) over \(\mathfrak p\).

Ideal.ramificationIdx_mul_card_inertia_subgroupOf · 24 lines 
theorem ramificationIdx_mul_card_inertia_subgroupOf
    {K L : Type*} {B : Type*} [Field K] [Field L] [Algebra K L]
    [CommRing B] [MulSemiringAction (L ≃ₐ[K] L) B]
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    P_E.ramificationIdx A *
      Nat.card ((P.inertia (L ≃ₐ[K] L)).subgroupOf E.fixingSubgroup) =
    Nat.card (P.inertia (L ≃ₐ[K] L))
Uses 1 · Used by 1
Proof usesTower formula for inertia groups
Used byRamification index one and the inertia group

TheoremRamification index one and the inertia group#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(I(\mathfrak P)\) be the inertia group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(x) - x \in \mathfrak P\) for all \(x \in B\). Then the ramification index \(e(\mathfrak P_E \mid \mathfrak p)\) of \(\mathfrak P_E\) over \(\mathfrak p\) equals \(1\) if and only if \(I(\mathfrak P) \le H\).

Ideal.ramificationIdx_eq_one_iff_inertia_le_fixingSubgroup · 21 lines 
theorem ramificationIdx_eq_one_iff_inertia_le_fixingSubgroup
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    P_E.ramificationIdx A = 1 ↔
      P.inertia (L ≃ₐ[K] L) ≤ E.fixingSubgroup
Uses 2 · Used by 1
Proof usesTower formula for inertia groups, intersected with the fixing group · Equal cardinality of an intersection forces containment
Used byRamification index one and the inertia field

TheoremRamification index one and the inertia field#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(I(\mathfrak P)\) be the inertia group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(x) - x \in \mathfrak P\) for all \(x \in B\), and let \(L^{I(\mathfrak P)}\) be its fixed field in \(L\). Then the ramification index \(e(\mathfrak P_E \mid \mathfrak p)\) of \(\mathfrak P_E\) over \(\mathfrak p\) equals \(1\) if and only if \(E \subseteq L^{I(\mathfrak P)}\).

Ideal.ramificationIdx_eq_one_iff_le_inertiaField · 21 lines 
theorem ramificationIdx_eq_one_iff_le_inertiaField
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    P_E.ramificationIdx A = 1 ↔
      E ≤ IntermediateField.fixedField (P.inertia (L ≃ₐ[K] L))
Uses 1 · Used by 1
Proof usesRamification index one and the inertia group
Used byFields below the inertia and decomposition fields

TheoremTower formula for decomposition groups#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(D(\mathfrak P)\) be the decomposition group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(\mathfrak P) = \mathfrak P\), and let \(e\) and \(f\) be the ramification index and the inertia degree of \(\mathfrak P_E\) over \(\mathfrak p\). Then \(e f \cdot |D(\mathfrak P) \cap H| = |D(\mathfrak P)|\).

Ideal.ramificationIdx_mul_inertiaDeg_mul_card_stabilizer_subgroupOf · 24 lines 
theorem ramificationIdx_mul_inertiaDeg_mul_card_stabilizer_subgroupOf
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    (P_E.ramificationIdx A * P_E.inertiaDeg A) *
      Nat.card ((@MulAction.stabilizer (L ≃ₐ[K] L) (Ideal B) _
        Ideal.pointwiseMulSemiringAction.toMulAction P).subgroupOf E.fixingSubgroup) =
    Nat.card (@MulAction.stabilizer (L ≃ₐ[K] L) (Ideal B) _
        Ideal.pointwiseMulSemiringAction.toMulAction P)
Used by 1
Used byRamification index and inertia degree one and the decomposition group

TheoremRamification index and inertia degree one and the decomposition group#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(D(\mathfrak P)\) be the decomposition group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(\mathfrak P) = \mathfrak P\), and let \(e\) and \(f\) be the ramification index and the inertia degree of \(\mathfrak P_E\) over \(\mathfrak p\). Then \(e = 1\) and \(f = 1\) if and only if \(D(\mathfrak P) \le H\).

Ideal.ramificationIdx_inertiaDeg_eq_one_iff_stabilizer_le_fixingSubgroup · 22 lines 
theorem ramificationIdx_inertiaDeg_eq_one_iff_stabilizer_le_fixingSubgroup
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    (P_E.ramificationIdx A = 1 ∧ P_E.inertiaDeg A = 1) ↔
      (@MulAction.stabilizer (L ≃ₐ[K] L) (Ideal B) _
        Ideal.pointwiseMulSemiringAction.toMulAction P) ≤ E.fixingSubgroup
Uses 2 · Used by 1
Proof usesTower formula for decomposition groups · Equal cardinality of an intersection forces containment
Used byRamification index and inertia degree one and the decomposition field

TheoremRamification index and inertia degree one and the decomposition field#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(D(\mathfrak P)\) be the decomposition group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(\mathfrak P) = \mathfrak P\), and let \(L^{D(\mathfrak P)}\) be its fixed field in \(L\). Let \(e\) and \(f\) be the ramification index and the inertia degree of \(\mathfrak P_E\) over \(\mathfrak p\). Then \(e = 1\) and \(f = 1\) if and only if \(E \subseteq L^{D(\mathfrak P)}\).

Ideal.ramificationIdx_inertiaDeg_eq_one_iff_le_decompositionField · 23 lines 
theorem ramificationIdx_inertiaDeg_eq_one_iff_le_decompositionField
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    (P_E.ramificationIdx A = 1 ∧ P_E.inertiaDeg A = 1) ↔
      E ≤ IntermediateField.fixedField
        (@MulAction.stabilizer (L ≃ₐ[K] L) (Ideal B) _
          Ideal.pointwiseMulSemiringAction.toMulAction P)
Uses 1 · Used by 1
Proof usesRamification index and inertia degree one and the decomposition group
Used byFields below the inertia and decomposition fields

TheoremFields below the inertia and decomposition fields#✓fully proved

Let \(L/K\) be a finite Galois extension with Galois group \(G\). Let \(A\) and \(B\) be Dedekind domains with \(B\) a finite torsion-free \(A\)-algebra, and let \(G\) act on \(B\) by ring automorphisms as a Galois group of \(B\) over \(A\): faithfully, fixing the image of \(A\), and with every element of \(B\) fixed by \(G\) in the image of \(A\). Let \(E\) be an intermediate field of \(L/K\) and \(H \le G\) the subgroup fixing \(E\) pointwise. Let \(C\) be a Dedekind domain and a torsion-free \(A\)-algebra, and give \(E\) an \(A\)-algebra structure and an injective ring map \(C \to E\) whose image is the set of elements of \(E\) integral over \(A\) (the composite \(A \to C \to E\) need not be the given map \(A \to E\)). Suppose \(B\) is also a finite torsion-free \(C\)-algebra, with \(A \to C \to B\) equal to \(A \to B\), and that \(H\), acting on \(B\) by restriction, is a Galois group of \(B\) over \(C\). Let \(\mathfrak p\), \(\mathfrak P_E\) and \(\mathfrak P\) be maximal ideals of \(A\), \(C\) and \(B\) such that \(\mathfrak P\) lies over \(\mathfrak p\) and over \(\mathfrak P_E\) and \(\mathfrak P_E\) lies over \(\mathfrak p\), and suppose that every prime of \(B\) over \(\mathfrak p\), and every prime of \(B\) over \(\mathfrak P_E\), has a separable residue field extension. Let \(I(\mathfrak P)\) be the inertia group of \(\mathfrak P\), the set of \(\sigma \in G\) with \(\sigma(x) - x \in \mathfrak P\) for all \(x \in B\), and \(D(\mathfrak P)\) its decomposition group, the set of \(\sigma \in G\) with \(\sigma(\mathfrak P) = \mathfrak P\); let \(L^{I(\mathfrak P)}\) and \(L^{D(\mathfrak P)}\) be their fixed fields in \(L\), and let \(e\) and \(f\) be the ramification index and the inertia degree of \(\mathfrak P_E\) over \(\mathfrak p\). Then \(e = 1\) if and only if \(E \subseteq L^{I(\mathfrak P)}\), and \(e = f = 1\) if and only if \(E \subseteq L^{D(\mathfrak P)}\).

Ideal.ramificationIdx_inertiaDeg_eq_one_iff_le_inertiaField_decompositionField · 25 lines 
theorem ramificationIdx_inertiaDeg_eq_one_iff_le_inertiaField_decompositionField
    [IsDedekindDomain B] [FaithfulSMul (L ≃ₐ[K] L) B]
    {A : Type*} [CommRing A] [IsDedekindDomain A] [Algebra A B]
    (P : Ideal B) [IsGalois K L] [FiniteDimensional K L] [P.IsMaximal]
    (p : Ideal A) [p.IsMaximal]
    (E : IntermediateField K L)
    (C_E : Type*) [CommRing C_E] [IsDedekindDomain C_E] [Algebra A C_E]
    [Algebra A ↥E] [Algebra C_E ↥E] [IsIntegralClosure C_E A ↥E]
    (P_E : Ideal C_E) [P_E.IsMaximal] [P_E.LiesOver p]
    [Algebra C_E B] [IsScalarTower A C_E B]
    [Module.Finite A B] [Module.IsTorsionFree A B]
    [Module.Finite C_E B] [Module.IsTorsionFree C_E B]
    [Module.IsTorsionFree A C_E]
    [P.LiesOver p] [P.LiesOver P_E]
    [Algebra.HasSeparableResidueFieldsAt A B p]
    [Algebra.HasSeparableResidueFieldsAt C_E B P_E]
    [IsGaloisGroup (L ≃ₐ[K] L) A B]
    [IsGaloisGroup (↥E.fixingSubgroup) C_E B]
    :
    (P_E.ramificationIdx A = 1 ↔
      E ≤ IntermediateField.fixedField (P.inertia (L ≃ₐ[K] L))) ∧
    ((P_E.ramificationIdx A = 1 ∧ P_E.inertiaDeg A = 1) ↔
      E ≤ IntermediateField.fixedField
        (@MulAction.stabilizer (L ≃ₐ[K] L) (Ideal B) _
          Ideal.pointwiseMulSemiringAction.toMulAction P))
Sources
  • ATLAS NumberTheoryI, Corollary 7.14.
Uses 2
Proof usesRamification index one and the inertia field · Ramification index and inertia degree one and the decomposition field

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.