Nyll.GaloisCohomology.ProP.ClosedKernelFiniteGeneration

theorem

linearIndependent_of_triangular_evaluation

ClassFieldTower.ProP.linearIndependent_of_triangular_evaluation

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations ClassFieldTower.Cohomology
noncomputable section
universe u v

Lean source · statement

theorem linearIndependent_of_triangular_evaluation
    {k : Type v} [Field k] {X : Type u} {n : ℕ}
    (v : Fin n → X → k) (x : Fin n → X)
    (hdiag : ∀ i, v i (x i) ≠ 0)
    (htri : ∀ i j, j < i → v i (x j) = 0) : LinearIndependent k v

theorem

exists_closedNormal_generating_family_le_finrank_h2

L68 ↗

ClassFieldTower.ProP.exists_closedNormal_generating_family_le_finrank_h2

Documentation

A closed normal subgroup in the Frattini subgroup is generated, as a closed normal subgroup, by at most dim H²(F/R, ZMod p) actual relators.

Source context 5 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups ProCGroups.ProC ProCGroups.Presentations ClassFieldTower.Cohomology
noncomputable section
universe u v

Lean source · full declaration

theorem exists_closedNormal_generating_family_le_finrank_h2
    {p : ℕ} [Fact p.Prime]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (hF : HasPGroupOpenNormalBasis p F)
    (R : ClosedSubgroup F) [R.Normal]
    (hR : (R : Subgroup F) ≤ closedPowerCommutator p F)
    [FiniteDimensional (ZMod p)
      (continuousCohomologyZModPLifted p (F ⧸ (R : Subgroup F)) 2)] :
    ∃ r ≤ Module.finrank (ZMod p)
        (continuousCohomologyZModPLifted p (F ⧸ (R : Subgroup F)) 2),
      ∃ ρ : Fin r → R,
        closedNormalClosure (Set.range (fun i ↦ (ρ i : F))) = (R : Subgroup F) := by
  classical
  let d : ℕ := Module.finrank (ZMod p)
    (continuousCohomologyZModPLifted p (F ⧸ (R : Subgroup F)) 2)
  by_contra hnone
  have hnot (n : ℕ) (hn : n ≤ d) (ρ : Fin n → R) :
      closedNormalClosure (Set.range (fun i ↦ (ρ i : F))) ≠ (R : Subgroup F) := by
    intro heq
    exact hnone ⟨n, hn, ρ, heq⟩
  have hbuild (n : ℕ) (hn : n ≤ d + 1) :
      ∃ ρ : Fin n → R, ∃ χ : Fin n → R →ₜ* Multiplicative (ZMod p),
        (∀ (i : Fin n) (f : F) (r : R), χ i (MulAut.conjNormal f r) = χ i r) ∧
        (∀ i : Fin n, χ i (ρ i) ≠ 1) ∧
        ∀ i j : Fin n, j < i → χ i (ρ j) = 1 := by
    induction n with
    | zero =>
      refine ⟨Fin.elim0, Fin.elim0, ?_, ?_, ?_⟩
      · intro i
        exact Fin.elim0 i
      · intro i
        exact Fin.elim0 i
      · intro i
        exact Fin.elim0 i
    | succ n ih =>
      obtain ⟨ρ, χ, hχinv, hdiag, htri⟩ := ih (Nat.le_trans (Nat.le_succ n) hn)
      let K : ClosedSubgroup F :=
        { toSubgroup := closedNormalClosure (Set.range (fun i ↦ (ρ i : F)))
          isClosed' := closedNormalClosure_isClosed (Set.range (fun i ↦ (ρ i : F))) }
      let : K.Normal :=
        inferInstanceAs (closedNormalClosure (Set.range (fun i ↦ (ρ i : F)))).Normal
      have hKR : K ≤ R := by
        apply closedNormalClosure_le_closed_normal R.isClosed'
        rintro r ⟨i, rfl⟩
        exact (ρ i).2
      have hKne : K ≠ R := by
        intro heq
        exact hnot n (Nat.le_of_succ_le_succ hn) ρ
          (congrArg (fun L : ClosedSubgroup F ↦ (L : Subgroup F)) heq)
      have hstrict : K < R := lt_of_le_of_ne hKR hKne
      obtain ⟨χnew, hnew, hkill, hnewInv⟩ := relativeNakayama_character hF K R hstrict
      obtain ⟨r, hr⟩ : ∃ r : R, χnew r ≠ 1 := by
        by_contra hall
        apply hnew
        apply ContinuousMonoidHom.ext
        intro r
        exact not_not.mp (fun hr ↦ hall ⟨r, hr⟩)
      refine ⟨Fin.snoc ρ r, Fin.snoc χ χnew, ?_, ?_, ?_⟩
      · intro i
        refine Fin.lastCases ?_ (fun j ↦ ?_) i
        · simpa only [Fin.snoc_last] using hnewInv
        · simpa only [Fin.snoc_castSucc] using hχinv j
      · intro i
        refine Fin.lastCases ?_ (fun j ↦ ?_) i
        · simpa only [Fin.snoc_last] using hr
        · simpa only [Fin.snoc_castSucc] using hdiag j
      · intro i
        refine Fin.lastCases ?_ (fun i ↦ ?_) i
        · intro j
          refine Fin.lastCases ?_ (fun j ↦ ?_) j
          · intro hlt
            exact (lt_irrefl (Fin.last n) hlt).elim
          · intro _hlt
            have hjK : (ρ j : F) ∈ K :=
              subset_closedNormalClosure (Set.range (fun i ↦ (ρ i : F))) ⟨j, rfl⟩
            simpa only [Fin.snoc_last, Fin.snoc_castSucc] using hkill ⟨(ρ j : F), hjK⟩
        · intro j
          refine Fin.lastCases ?_ (fun j ↦ ?_) j
          · intro hlt
            exact (Nat.not_lt_of_ge (Nat.le_of_lt i.isLt) hlt).elim
          · intro hlt
            simpa only [Fin.snoc_castSucc] using htri i j hlt
  obtain ⟨ρ, χ, hχinv, hdiag, htri⟩ := hbuild (d + 1) le_rfl
  have hχind : LinearIndependent (ZMod p) (fun i ↦ fun r : R ↦ (χ i r).toAdd) := by
    apply linearIndependent_of_triangular_evaluation (x := ρ)
    · intro i heq
      exact hdiag i (congrArg Multiplicative.ofAdd heq)
    · intro i j hji
      exact congrArg Multiplicative.toAdd (htri i j hji)
  have hbound := invariant_character_family_card_le_finrank_h2 hF R hR χ hχinv hχind
  have hbad : d + 1 ≤ d := by simpa only [Fintype.card_fin] using hbound
  exact Nat.not_succ_le_self d hbad

ClosedKernelFiniteGeneration.lean

Module documentation

Finite normal generation from finite-dimensional H²

linearIndependent_of_triangular_evaluation

exists_closedNormal_generating_family_le_finrank_h2

Module documentation

Finite normal generation from finite-dimensional H²

Declarations

linearIndependent_of_triangular_evaluation

exists_closedNormal_generating_family_le_finrank_h2