in K / L / k, [L : k] = index of fixing subgroup of L

Stream: Is there code for X?

[Jz Pan]

Seems that there are missing APIs for infinite Galois theory. If K / k is an infinite Galois extension, then docs#InfiniteGalois.isOpen_iff_finite says that the fixing subgroup of L is open if and only if L / k is finite. I think that in this case the [L : k] should equal to the index of the fixing subgroup of L (is this true mathematically?). But this result is missing. We only have docs#IsGalois.card_fixingSubgroup_eq_finrank which concerns [K : L] for finite Galois extension.

[Kevin Buzzard]

Yes this is true mathematically. You can probably deduce it mathematically from the finite case applied to the Galois closure of L/k plus third isomorphism theorem although this might be a painful way to formalise it

[Kevin Buzzard]

A useful result is that a finite index open subgroup contains a finite index open normal subgroup (take the intersection of the conjugates)

[Jz Pan]

Thank you, let me try. Is it the standard textbook proof?

[Jz Pan]

And seems that no stacks tags are attached to the theorems for infinite Galois theory yet.

[Kevin Buzzard]

I don't know what's in the textbooks or in stacks unfortunately, this is an area I picked up by osmosis 35 years ago

[Jz Pan]

There are some interesting facts on https://stacks.math.columbia.edu/tag/0BMI, for example the universal property of Krull topology...

[Jz Pan]

Kevin Buzzard said:

Yes this is true mathematically. You can probably deduce it mathematically from the finite case applied to the Galois closure of L/k plus third isomorphism theorem although this might be a painful way to formalise it

It works (probably without importing infinite Galois file):

import Mathlib

-- TODO: move to suitable file
theorem _root_.IntermediateField.map_fixingSubgroup
    {k E : Type*} (K : Type*)
    [Field k] [Field E] [Field K] [Algebra k E] [Algebra k K] [Algebra E K] [IsScalarTower k E K]
    [Normal k E] (L : IntermediateField k E) :
    (L.map (IsScalarTower.toAlgHom k E K)).fixingSubgroup =
      L.fixingSubgroup.comap (AlgEquiv.restrictNormalHom (F := k) (K₁ := K) E) := by
  ext f
  simp only [Subgroup.mem_comap, IntermediateField.mem_fixingSubgroup_iff]
  constructor
  · rintro h x hx
    change f.restrictNormal E x = x
    apply_fun _ using (algebraMap E K).injective
    rw [AlgEquiv.restrictNormal_commutes]
    exact h _ ⟨x, hx, rfl⟩
  · rintro h _ ⟨x, hx, rfl⟩
    replace h := congr(algebraMap E K $(show f.restrictNormal E x = x from h x hx))
    rwa [AlgEquiv.restrictNormal_commutes] at h

-- TODO: move to suitable file
theorem _root_.IntermediateField.map_fixingSubgroup_index
    {k E : Type*} (K : Type*)
    [Field k] [Field E] [Field K] [Algebra k E] [Algebra k K] [Algebra E K] [IsScalarTower k E K]
    [Normal k E] [Normal k K] (L : IntermediateField k E) :
    (L.map (IsScalarTower.toAlgHom k E K)).fixingSubgroup.index = L.fixingSubgroup.index := by
  rw [L.map_fixingSubgroup K, L.fixingSubgroup.index_comap_of_surjective
    (AlgEquiv.restrictNormalHom_surjective _)]

-- TODO: move to suitable file
theorem _root_.IsGalois.finrank_eq_index_of_finite
    {k K : Type*} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K)
    [IsGalois k K] [FiniteDimensional k L] :
    Module.finrank k L = L.fixingSubgroup.index := by
  let E := IntermediateField.normalClosure k L K
  have hle : L ≤ E := by
    simpa only [IntermediateField.fieldRange_val] using L.val.fieldRange_le_normalClosure
  let L' := IntermediateField.restrict hle
  have h := Module.finrank_mul_finrank k ↥L' ↥E
  classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  nth_rw 2 [Fintype.card_eq_nat_card] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.card_eq_fintype_card,
    Nat.mul_left_inj Fintype.card_ne_zero] at h
  rw [(IntermediateField.restrict_algEquiv hle).toLinearEquiv.finrank_eq, h,
    ← L'.map_fixingSubgroup_index K]
  congr 2
  exact IntermediateField.lift_restrict hle

[Jz Pan]

Module.finrank k L = L.fixingSubgroup.index should be true without requiring FiniteDimensional k L, though. In that case both sides should be zero. But I don't know how to prove that L.fixingSubgroup is of infinite index if [L : k] is not finite.

[Jz Pan]

I think I have a solution. If L / k is infinite but algebraic, then there are finite extensions L' with arbitrary large degree inside L / k. We should have L.fixingSubgroup ≤ L'.fixingSubgroup but L'.fixingSubgroup.index can be arbitrary large. So L.fixingSubgroup must be of infinite index.

[Jz Pan]

Done!

-- ... same as above

-- TODO: move to suitable file
theorem _root_.IsGalois.finrank_eq_index
    {k K : Type*} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] :
    Module.finrank k L = L.fixingSubgroup.index := by
  wlog hnfd : FiniteDimensional k L generalizing L
  · rw [Module.finrank_of_infinite_dimensional hnfd]
    by_contra! h
    replace h : L.fixingSubgroup.FiniteIndex := ⟨h.symm⟩
    obtain ⟨L', hfd, hL'⟩ :=
      IntermediateField.exists_lt_finrank_of_infinite_dimensional hnfd L.fixingSubgroup.index
    let i := (IntermediateField.liftAlgEquiv L').toLinearEquiv
    replace hfd := i.finiteDimensional
    rw [i.finrank_eq, this _ hfd] at hL'
    exact (Subgroup.index_antitone <| IntermediateField.fixingSubgroup.antimono <|
      IntermediateField.lift_le L').not_lt hL'
  let E := IntermediateField.normalClosure k L K
  have hle : L ≤ E := by
    simpa only [IntermediateField.fieldRange_val] using L.val.fieldRange_le_normalClosure
  let L' := IntermediateField.restrict hle
  have h := Module.finrank_mul_finrank k ↥L' ↥E
  classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  nth_rw 2 [Fintype.card_eq_nat_card] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.card_eq_fintype_card,
    Nat.mul_left_inj Fintype.card_ne_zero] at h
  rw [(IntermediateField.restrict_algEquiv hle).toLinearEquiv.finrank_eq, h,
    ← L'.map_fixingSubgroup_index K]
  congr 2
  exact IntermediateField.lift_restrict hle

[Jz Pan]

#find_home cannot find a suitable place for IntermediateField.map_fixingSubgroup...

[Jz Pan]

Found it: Mathlib.FieldTheory.KrullTopology

[Jz Pan]

PR created as #23693.