Maps.lean

def completedGroupAlgebraMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ) :
    CompletedGroupAlgebraInClass C R G →+* CompletedGroupAlgebraInClass C R H where
  toFun x :=
    (completedGroupAlgebraInClassCompatibleFamilyEquiv
      (R := R) (G := H) C).symm
      ((completedGroupAlgebraSystemInClass C R H).inverseLimitLift
        (fun V x =>
          completedGroupAlgebraFunctorialStageMapInClass
            (G := G) (H := H) C hHer (R := R) φ hφ V
            (completedGroupAlgebraProjectionInClass C R G
              (completedGroupAlgebraComapIndexInClass
                (G := G) (H := H) C hHer φ hφ V) x))
        (by
          intro V W hVW
          funext x
          have hcomp := congrFun
            (congrArg DFunLike.coe
              (completedGroupAlgebraFunctorialStageMapInClass_transition
                (R := R) (G := G) (H := H) C hHer φ hφ hVW))
            (completedGroupAlgebraProjectionInClass C R G
              (completedGroupAlgebraComapIndexInClass
                (G := G) (H := H) C hHer φ hφ W) x)
          rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
          simp only
          rw [← completedGroupAlgebraProjectionInClass_compatible
            (R := R) (G := G) C
            (completedGroupAlgebraComapIndexInClass_mono
              (G := G) (H := H) C hHer φ hφ hVW) x]
          exact hcomp) x)
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_zero (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_one (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_add (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    exact map_mul (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)
      (completedGroupAlgebraProjectionInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) y)

theorem completedGroupAlgebraProjectionInClass_map
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndexInClass H C) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraProjectionInClass C R H V
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) =
      completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V
        (completedGroupAlgebraProjectionInClass C R G
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) x)

def completedGroupAlgebraMapAlgHomInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ) :
    CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraInClass C R H where
  toRingHom := completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
  commutes' := by
    intro r
    apply completedGroupAlgebraInClass_ext (R := R) (G := H) C
    intro V
    change completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V
        (algebraMap R
          (CompletedGroupAlgebraStageInClass C R G
            (completedGroupAlgebraComapIndexInClass
              (G := G) (H := H) C hHer φ hφ V)) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r
    exact completedGroupAlgebraFunctorialStageMapInClass_algebraMap
      (R := R) (G := G) (H := H) C hHer φ hφ V r

theorem completedGroupAlgebraMapAlgHomInClass_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ x =
      completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x

theorem continuous_completedGroupAlgebraMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    Continuous (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)

theorem completedGroupAlgebraMapInClass_comp_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      (toCompletedGroupAlgebraInClassRingHom C R H).comp
        (MonoidAlgebra.mapDomainRingHom R φ)

theorem completedGroupAlgebraMapInClass_surjective_of_surjective
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
    Function.Surjective
      (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)

theorem completedGroupAlgebraInClassRingHom_ext_of_comp_toCompleted
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G)
    {f g : CompletedGroupAlgebraInClass C R G →+*
      CompletedGroupAlgebraInClass C R H}
    (hf : Continuous f) (hg : Continuous g)
    (hfg : f.comp (toCompletedGroupAlgebraInClassRingHom C R G) =
      g.comp (toCompletedGroupAlgebraInClassRingHom C R G)) :
    f = g

theorem completedGroupAlgebraMapInClass_id
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) :
    completedGroupAlgebraMapInClass (G := G) (H := G) C hHer R
        (MonoidHom.id G) continuous_id =
      RingHom.id (CompletedGroupAlgebraInClass C R G)

theorem completedGroupAlgebraMapAlgHomInClass_id
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G) :
    completedGroupAlgebraMapAlgHomInClass (G := G) (H := G) C hHer R
        (MonoidHom.id G) continuous_id =
      AlgHom.id R (CompletedGroupAlgebraInClass C R G)

theorem completedGroupAlgebraMapInClass_comp
    {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G)
    (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
    (completedGroupAlgebraMapInClass (G := H) (H := K) C hHer R ψ hψ).comp
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) =
      completedGroupAlgebraMapInClass (G := G) (H := K) C hHer R
        (ψ.comp φ) (hψ.comp hφ)

theorem completedGroupAlgebraMapAlgHomInClass_comp
    {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hG : HasOpenNormalBasisInClass C G)
    (φ : G →* H) (hφ : Continuous φ) (ψ : H →* K) (hψ : Continuous ψ) :
    (completedGroupAlgebraMapAlgHomInClass (G := H) (H := K) C hHer R ψ hψ).comp
        (completedGroupAlgebraMapAlgHomInClass (G := G) (H := H) C hHer R φ hφ) =
      completedGroupAlgebraMapAlgHomInClass (G := G) (H := K) C hHer R
        (ψ.comp φ) (hψ.comp hφ)

theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g)) =
      toCompletedGroupAlgebraInClass C R H (MonoidAlgebra.of R H (φ g))

theorem completedGroupAlgebraMapInClass_toCompletedGroupAlgebraInClass_sub_one_of
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ
        (toCompletedGroupAlgebraInClass C R G (MonoidAlgebra.of R G g) - 1) =
      toCompletedGroupAlgebraInClass C R H (MonoidAlgebra.of R H (φ g)) - 1