NYLL
Module

FiniteAbstractFixedField.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteAbstractFixedField
20 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: finite abstract fields inside a separable closure

The abstract fields to which the class field axiom is applied are the open closed subgroups of the absolute Galois group. This file turns the explicit finite-index witness from the abstract class-formation data into the corresponding finite fixed field. It is the field-theoretic input needed before the local class-field-axiom theorem can be applied.

Imports4
Imported by12

Declarations

abbrev

abstractFixedField

L34 ↗
LocalClassFieldTheory.abstractFixedField
Documentation

The concrete fixed field represented by an abstract closed subgroup.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
abbrev abstractFixedField (H : ClosedSubgroup (Gal(Ω/k))) :
    IntermediateField k Ω
theorem

closedFixingSubgroup_abstractFixedField_eq

L40 ↗
LocalClassFieldTheory.closedFixingSubgroup_abstractFixedField_eq
Documentation

Passing from an abstract field to its concrete fixed field and back recovers the original closed subgroup.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem closedFixingSubgroup_abstractFixedField_eq
    (H : ClosedSubgroup (Gal(Ω/k))) :
    closedFixingSubgroup k Ω (abstractFixedField k Ω H) = H
theorem

ambientQuotientFiniteOfAbstractFinite

L51 ↗
LocalClassFieldTheory.ambientQuotientFiniteOfAbstractFinite
Documentation

Absolute finiteness in the abstract class-formation quotient presentation gives a finite quotient of the ambient absolute Galois group by the same subgroup.

Source context 6 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
omit [IsGalois k Ω] in
Lean source · statement
theorem ambientQuotientFiniteOfAbstractFinite
    (H : ClosedSubgroup (Gal(Ω/k)))
    (hfinite : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) H (le_baseField H))) :
    Finite (Gal(Ω/k) ⧸ H.toSubgroup)
theorem

abstractFiniteClosedSubgroup_isOpen

L69 ↗
LocalClassFieldTheory.abstractFiniteClosedSubgroup_isOpen
Documentation

An abstract field finite over the distinguished base is represented by an open subgroup of the absolute Galois group.

Source context 6 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
omit [IsGalois k Ω] in
Lean source · statement
theorem abstractFiniteClosedSubgroup_isOpen
    (H : ClosedSubgroup (Gal(Ω/k)))
    (hfinite : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) H (le_baseField H))) :
    IsOpen H.carrier
theorem

abstractFixedField_finiteDimensional

L82 ↗
LocalClassFieldTheory.abstractFixedField_finiteDimensional
Documentation

The fixed field of an abstract field finite over the distinguished base is an actual finite field extension.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem abstractFixedField_finiteDimensional
    (H : ClosedSubgroup (Gal(Ω/k)))
    (hfinite : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) H (le_baseField H))) :
    FiniteDimensional k (abstractFixedField k Ω H)
theorem

abstractFixedField_le

L95 ↗
LocalClassFieldTheory.abstractFixedField_le
Documentation

Inclusion of abstract subgroups reverses to inclusion of their concrete fixed fields.

Source context 6 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
omit [IsGalois k Ω] in
Lean source · statement
theorem abstractFixedField_le {K L : ClosedSubgroup (Gal(Ω/k))}
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    abstractFixedField k Ω K ≤ abstractFixedField k Ω L
def

abstractSubgroupEquivGaloisGroup

L102 ↗
LocalClassFieldTheory.abstractSubgroupEquivGaloisGroup
Documentation

The abstract subgroup representing a fixed field is canonically the absolute Galois group of the ambient extension over that fixed field.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
def abstractSubgroupEquivGaloisGroup
    (H : ClosedSubgroup (Gal(Ω/k))) :
    H.toSubgroup ≃* Gal(Ω/abstractFixedField k Ω H)
theorem

abstractSubgroupEquivGaloisGroup_apply

L111 ↗
LocalClassFieldTheory.abstractSubgroupEquivGaloisGroup_apply
Documentation

States the theorem abstractSubgroupEquivGaloisGroup_apply.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem abstractSubgroupEquivGaloisGroup_apply
    (H : ClosedSubgroup (Gal(Ω/k))) (σ : H.toSubgroup) (x : Ω) :
    abstractSubgroupEquivGaloisGroup k Ω H σ x = σ.1 x
abbrev

abstractRelativeFixedField

L118 ↗
LocalClassFieldTheory.abstractRelativeFixedField
Documentation

The upper fixed field, regarded as an intermediate field over the lower fixed field in a relative abstract extension.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
abbrev abstractRelativeFixedField
    {K L : ClosedSubgroup (Gal(Ω/k))}
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    IntermediateField (abstractFixedField k Ω K) Ω
theorem

map_extensionSubgroup_abstractSubgroupEquiv

L126 ↗
LocalClassFieldTheory.map_extensionSubgroup_abstractSubgroupEquiv
Documentation

Under the preceding Galois-group equivalence, the relative class-formation subgroup is exactly the subgroup fixing the upper concrete field.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem map_extensionSubgroup_abstractSubgroupEquiv
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    (extensionSubgroup K L hLK).map
        (abstractSubgroupEquivGaloisGroup k Ω K).toMonoidHom =
      (abstractRelativeFixedField k Ω hLK).fixingSubgroup
theorem

abstractRelativeFixingSubgroup_normal

L170 ↗
LocalClassFieldTheory.abstractRelativeFixingSubgroup_normal
Documentation

Relative normality in the abstract class-formation framework is the actual normality of the subgroup fixing the upper field inside the lower field's absolute Galois group.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem abstractRelativeFixingSubgroup_normal
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    (abstractRelativeFixedField k Ω hLK).fixingSubgroup.Normal
theorem

abstractRelativeFixedField_isGalois

L184 ↗
LocalClassFieldTheory.abstractRelativeFixedField_isGalois
Documentation

The concrete relative fixed field is Galois precisely from the normality witness occurring in the abstract cyclic extension.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem abstractRelativeFixedField_isGalois
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    IsGalois (abstractFixedField k Ω K)
      (abstractRelativeFixedField k Ω hLK)
def

abstractRelativeToAmbientQuotient

L196 ↗
LocalClassFieldTheory.abstractRelativeToAmbientQuotient
Documentation

Restriction through the lower fixed field, followed by quotienting by the upper fixing subgroup.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · full declaration
def abstractRelativeToAmbientQuotient
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    letI := abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
    K.toSubgroup →*
      Gal(Ω/abstractFixedField k Ω K) ⧸
        (abstractRelativeFixedField k Ω hLK).fixingSubgroup := by
  letI : (abstractRelativeFixedField k Ω hLK).fixingSubgroup.Normal :=
    abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
  exact (QuotientGroup.mk'
    (abstractRelativeFixedField k Ω hLK).fixingSubgroup).comp
      (abstractSubgroupEquivGaloisGroup k Ω K).toMonoidHom
theorem

abstractRelativeToAmbientQuotient_ker

L212 ↗
LocalClassFieldTheory.abstractRelativeToAmbientQuotient_ker
Documentation

The kernel of the preceding quotient map is the exact abstract class-formation relative subgroup.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · full declaration
theorem abstractRelativeToAmbientQuotient_ker
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    letI := abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
    (abstractRelativeToAmbientQuotient k Ω K L hLK hnormal).ker =
      extensionSubgroup K L hLK := by
  let : (abstractRelativeFixedField k Ω hLK).fixingSubgroup.Normal :=
    abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
  ext σ
  change
    QuotientGroup.mk' (abstractRelativeFixedField k Ω hLK).fixingSubgroup
        (abstractSubgroupEquivGaloisGroup k Ω K σ) = 1 ↔
      σ ∈ extensionSubgroup K L hLK
  rw [QuotientGroup.mk'_apply, QuotientGroup.eq_one_iff]
  rw [← map_extensionSubgroup_abstractSubgroupEquiv k Ω K L hLK]
  constructor
  · rintro ⟨τ, hτ, hτσ⟩
    have : τ = σ :=
      (abstractSubgroupEquivGaloisGroup k Ω K).injective hτσ
    simpa [this] using hτ
  · intro hσ
    exact ⟨σ, hσ, rfl⟩
theorem

abstractRelativeToAmbientQuotient_surjective

L237 ↗
LocalClassFieldTheory.abstractRelativeToAmbientQuotient_surjective
Documentation

The quotient map from the abstract lower subgroup is surjective.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · full declaration
theorem abstractRelativeToAmbientQuotient_surjective
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    letI := abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
    Function.Surjective
      (abstractRelativeToAmbientQuotient k Ω K L hLK hnormal) := by
  let : (abstractRelativeFixedField k Ω hLK).fixingSubgroup.Normal :=
    abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
  intro q
  refine Quotient.inductionOn' q ?_
  intro τ
  refine ⟨(abstractSubgroupEquivGaloisGroup k Ω K).symm τ, ?_⟩
  change QuotientGroup.mk
    (abstractSubgroupEquivGaloisGroup k Ω K
      ((abstractSubgroupEquivGaloisGroup k Ω K).symm τ)) =
      QuotientGroup.mk τ
  rw [(abstractSubgroupEquivGaloisGroup k Ω K).apply_symm_apply]
def

abstractExtensionQuotientEquivAmbient

L259 ↗
LocalClassFieldTheory.abstractExtensionQuotientEquivAmbient
Documentation

The exact abstract class-formation quotient of a relative normal extension is the ordinary quotient of the lower absolute Galois group by the upper fixing subgroup.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · full declaration
def abstractExtensionQuotientEquivAmbient
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    letI := hnormal
    letI := abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
    K.toSubgroup ⧸ extensionSubgroup K L hLK ≃*
      Gal(Ω/abstractFixedField k Ω K) ⧸
        (abstractRelativeFixedField k Ω hLK).fixingSubgroup := by
  letI := hnormal
  letI : (abstractRelativeFixedField k Ω hLK).fixingSubgroup.Normal :=
    abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
  exact (QuotientGroup.quotientMulEquivOfEq
      (abstractRelativeToAmbientQuotient_ker
        k Ω K L hLK hnormal).symm).trans
    (QuotientGroup.quotientKerEquivOfSurjective
      (abstractRelativeToAmbientQuotient k Ω K L hLK hnormal)
      (abstractRelativeToAmbientQuotient_surjective
        k Ω K L hLK hnormal))
def

abstractExtensionQuotientEquivGaloisGroup

L281 ↗
LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
Documentation

The quotient group appearing in the abstract class-field-axiom predicate is canonically the actual Galois group of the two concrete fixed fields.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · full declaration
def abstractExtensionQuotientEquivGaloisGroup
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal) :
    letI := hnormal
    K.toSubgroup ⧸ extensionSubgroup K L hLK ≃*
      Gal(abstractRelativeFixedField k Ω hLK/abstractFixedField k Ω K) := by
  letI := hnormal
  letI : (abstractRelativeFixedField k Ω hLK).fixingSubgroup.Normal :=
    abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
  let H : ClosedSubgroup (Gal(Ω/abstractFixedField k Ω K)) :=
    closedFixingSubgroup (abstractFixedField k Ω K) Ω
      (abstractRelativeFixedField k Ω hLK)
  letI : H.toSubgroup.Normal := by
    exact abstractRelativeFixingSubgroup_normal k Ω K L hLK hnormal
  exact (abstractExtensionQuotientEquivAmbient
      k Ω K L hLK hnormal).trans
    ((InfiniteGalois.normalAutEquivQuotient H).trans
      (AlgEquiv.autCongr
        (IntermediateField.equivOfEq
          (InfiniteGalois.fixedField_fixingSubgroup
            (abstractRelativeFixedField k Ω hLK)))))
theorem

abstractFixedField_relativeFiniteDimensional

L306 ↗
LocalClassFieldTheory.abstractFixedField_relativeFiniteDimensional
Documentation

In a finite abstract tower L / K / k, the concrete upper fixed field is finite over the concrete lower fixed field.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · full declaration
theorem abstractFixedField_relativeFiniteDimensional
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hKfinite : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) K (le_baseField K)))
    (hLKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)) :
    letI : Algebra (abstractFixedField k Ω K) (abstractFixedField k Ω L) :=
      RingHom.toAlgebra
        (IntermediateField.inclusion (abstractFixedField_le k Ω hLK))
    FiniteDimensional (abstractFixedField k Ω K)
      (abstractFixedField k Ω L) := by
  let : Algebra (abstractFixedField k Ω K) (abstractFixedField k Ω L) :=
    RingHom.toAlgebra
      (IntermediateField.inclusion (abstractFixedField_le k Ω hLK))
  let : IsScalarTower k (abstractFixedField k Ω K)
      (abstractFixedField k Ω L) :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) K (le_baseField K)) :=
    hKfinite
  let : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK) := hLKfinite
  let : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) L (le_baseField L)) :=
    FiniteGaloisSubextension.finite_extension_trans hLK (le_baseField K)
  let : FiniteDimensional k (abstractFixedField k Ω L) :=
    abstractFixedField_finiteDimensional k Ω L inferInstance
  exact FiniteDimensional.right k
    (abstractFixedField k Ω K) (abstractFixedField k Ω L)
theorem

abstractRelativeFixedField_finiteDimensional

L339 ↗
LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
Documentation

The same relative finiteness statement in the scalar-extended intermediate-field presentation used by infinite Galois theory.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem abstractRelativeFixedField_finiteDimensional
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hKfinite : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) K (le_baseField K)))
    (hLKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)) :
    FiniteDimensional (abstractFixedField k Ω K)
      (abstractRelativeFixedField k Ω hLK)
theorem

finiteAbstractExtension_degree_eq_finrank

L367 ↗
LocalClassFieldTheory.finiteAbstractExtension_degree_eq_finrank
Documentation

The abstract extension degree is the ordinary degree of the concrete finite Galois extension represented by the same pair of fixed fields.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (k Ω : Type) [Field k] [Field Ω] [Algebra k Ω] [IsGalois k Ω]
Lean source · statement
theorem finiteAbstractExtension_degree_eq_finrank
    (K L : ClosedSubgroup (Gal(Ω/k)))
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (hnormal : (extensionSubgroup K L hLK).Normal)
    (hKfinite : Finite ((baseField (Gal(Ω/k))).toSubgroup ⧸
      extensionSubgroup (baseField (Gal(Ω/k))) K (le_baseField K)))
    (hLKfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L hLK)) :
    ((DegreeData.FiniteAbstractExtension.ofInclusion L K hLK).degree : ℕ) =
      Module.finrank (abstractFixedField k Ω K)
        (abstractRelativeFixedField k Ω hLK)

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