Module

FreeProPProjective.lean

Nyll.ProCGroups.Cohomology.FreeProPProjective

2 declarations indexed from sourceView source ↗

Module documentation

Projectivity of finite-basis free pro-p groups

A finite-basis free pro-p group lifts continuously through every continuous surjection from a pro-p group. The section form is the projective input for the standard proof that its continuous degree-two cohomology vanishes.

Imports2

Imported by2

theorem

freeProP_exists_continuous_lift_of_surjective

L36 ↗

ClassFieldTower.ProP.freeProP_exists_continuous_lift_of_surjective

Documentation

A finite-basis free pro-p source lifts continuously through every continuous surjection whose source is pro-p.

Source context 7 commands

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

open scoped Topology
namespace ClassFieldTower.ProP
open ProCGroups
noncomputable section
universe u
variable {p d : ℕ} [Fact p.Prime]
variable
  (sourceData :
    FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
      (FiniteGroupClass.pGroup p))

Lean source · statement

theorem freeProP_exists_continuous_lift_of_surjective
    (hbasis : Cardinal.mk sourceData.basis = d)
    {E : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
    [CompactSpace E] [T2Space E] [TotallyDisconnectedSpace E]
    (hE : ProC.HasPGroupOpenNormalBasis p E)
    {Q : Type u} [Group Q] [TopologicalSpace Q] [T2Space Q]
    (q : E →ₜ* Q) (hq : Function.Surjective q)
    (f : sourceData.carrier →ₜ* Q) :
    ∃ s : sourceData.carrier →ₜ* E,
      q.comp s = f

theorem

freeProP_exists_continuous_section_of_surjective

L74 ↗

ClassFieldTower.ProP.freeProP_exists_continuous_section_of_surjective