CrowellExactSequence.freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis
The bifiltered coefficient maps form an additive identity-quotient kernel neighbourhood basis.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open FoxDifferential
open ProCGroups.ProC
open ProCGroups.Completion
open ProCGroups.InverseSystems
universe u v
variable {G H : Type u}
variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]Lean source · full declaration
theorem freeProCZCBifilteredAllFiniteQuotientStageCoeffMap_additive_basis
{C : ProCGroups.FiniteGroupClass.{u}} (hForm : ProCGroups.FiniteGroupClass.Formation C)
{X H : Type u}
[Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : X → H)
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
HasAdditiveIdentityQuotientKernelNeighbourhoodBasis
(A := ZCCompletedGroupAlgebra C H)
(fun j : ZCCompletedGroupAlgebraIndex C H =>
(freeProCZCBifilteredAllFiniteQuotientStageCoeffMap
(C := C) (X := X) (H := H) φ hφgen j).toAddMonoidHom) := by
classical
let : ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C :=
hForm.containsTrivialQuotients
let : Nonempty (ZCCompletedGroupAlgebraIndex C H) :=
⟨(ProCIntegerIndex.terminal (C := C) inferInstance,
zcCompletedGroupAlgebraTopIndex C H)⟩
let S := zcCompletedGroupAlgebraSystem C H
have hdir :
Directed (· ≤ ·) (id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) :=
directed_zcCompletedGroupAlgebraIndex_of_formation
(C := C) (H := H) hForm
intro U hU hUzero
rcases S.exists_projection_preimage_subset hdir hU hUzero with
⟨j, V, _hVopen, hzeroV, hpre⟩
refine ⟨j, ?_⟩
intro z hz
apply hpre
change zcCompletedGroupAlgebraProjection C H j z ∈ V
let :
∀ j : ZCCompletedGroupAlgebraIndex C H,
DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H C j.2) :=
fun j =>
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
have hqmap_inj :
Function.Injective
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j) := by
exact
freeProCFiniteQuotientStageQMapFamily_injective
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j
have hstage_inj :
Function.Injective
(zcCompletedGroupAlgebraStageToFoxAlgebraicStage
(C := C) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) j)
j.1.modulus j dvd_rfl
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j)) := by
exact
zcCompletedGroupAlgebraStageToFoxAlgebraicStage_self_injective
(C := C) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) j)
j
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j)
hqmap_inj
have hzstage :
zcCompletedGroupAlgebraProjection C H j z = 0 := by
let stageMap :=
zcCompletedGroupAlgebraStageToFoxAlgebraicStage
(C := C) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) j)
j.1.modulus j dvd_rfl
(freeProCFiniteQuotientStageQMapFamily
(C := C) φ
(id : ZCCompletedGroupAlgebraIndex C H →
ZCCompletedGroupAlgebraIndex C H) hφgen j)
have hstage_inj' : Function.Injective stageMap := hstage_inj
have hzmap := hz
simp only [freeProCZCBifilteredAllFiniteQuotientStageCoeffMap,
freeProCZCBifilteredFiniteQuotientStageCoeffMap,
zcCompletedGroupAlgebraBifilteredStageCoeffMap,
zcCompletedGroupAlgebraFoxAlgebraicStageCoeffMap] at hzmap
change
stageMap (zcCompletedGroupAlgebraProjection C H j z) = 0 at hzmap
apply hstage_inj'
rw [hzmap, map_zero]
rw [hzstage]
exact hzeroV