GroupLike.lean

def completedGroupAlgebraOfInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (g : G) : CompletedGroupAlgebraInClass C R G

theorem completedGroupAlgebraProjectionInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) (g : G) :
    completedGroupAlgebraProjectionInClass C R G U
        (completedGroupAlgebraOfInClass C R G g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

theorem completedGroupAlgebraOfInClass_one
    (C : ProCGroups.FiniteGroupClass.{v}) :
    completedGroupAlgebraOfInClass C R G 1 =
      (1 : CompletedGroupAlgebraInClass C R G)

theorem completedGroupAlgebraOfInClass_mul
    (C : ProCGroups.FiniteGroupClass.{v})
    (g h : G) :
    completedGroupAlgebraOfInClass C R G (g * h) =
      completedGroupAlgebraOfInClass C R G g *
        completedGroupAlgebraOfInClass C R G h

theorem continuous_completedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
      (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
    Continuous fun g : G => completedGroupAlgebraStageMapInClass C R G U
      (MonoidAlgebra.of R G g) := by
  let : Finite (CompletedGroupAlgebraQuotientInClass G C U) :=
    finite_completedGroupAlgebraQuotientInClass G C U
  let : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
    (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
  let : DiscreteTopology (CompletedGroupAlgebraQuotientInClass G C U) :=
    QuotientGroup.discreteTopology
      (ProCGroups.openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 :
          OpenNormalSubgroup G))
  have hbasis :
      @Continuous (CompletedGroupAlgebraQuotientInClass G C U)
        (CompletedGroupAlgebraStageInClass C R G U) inferInstance
        ((completedGroupAlgebraSystemInClass C R G).topologicalSpace U)
        (fun q => MonoidAlgebra.single q (1 : R)) :=
    continuous_of_discreteTopology
  have hproj :
      Continuous fun g : G => openNormalSubgroupInClassProj (C := C) (G := G) U g := by
    change Continuous
      (QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
    exact continuous_quotient_mk'
  have hcont := hbasis.comp hproj
  change @Continuous G (CompletedGroupAlgebraStageInClass C R G U) (‹TopologicalSpace G›)
    ((completedGroupAlgebraSystemInClass C R G).topologicalSpace U)
    (fun g => MonoidAlgebra.single
      (openNormalSubgroupInClassProj (C := C) (G := G) U g) (1 : R)) at hcont
  convert hcont using 1
  funext g
  exact completedGroupAlgebraStageMapInClass_of (R := R) (G := G) C U g

theorem continuous_completedGroupAlgebraOfInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Continuous (completedGroupAlgebraOfInClass C R G)