OpenFiniteQuotients.lean

abbrev CompletedGroupAlgebraOpenIdeal
    (R : Type u) [CommRing R] [TopologicalSpace R] : Type u

theorem profiniteRing_eq_zero_of_forall_openIdeal_quotient_eq_zero
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R] {r : R}
    (hr : ∀ I : CompletedGroupAlgebraOpenIdeal R, Ideal.Quotient.mk I.1 r = 0) :
    r = 0

abbrev CompletedGroupAlgebraOpenQuotientIndex
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] : Type (max u v)

instance instNonemptyCompletedGroupAlgebraOpenIdeal
    (R : Type u) [CommRing R] [TopologicalSpace R] :
    Nonempty (CompletedGroupAlgebraOpenIdeal R)

theorem directed_completedGroupAlgebraOpenQuotientIndex
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] :
    Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => K := by
  intro K L
  rcases directed_openNormalSubgroupInClass
      (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          ProCGroups.FiniteGroupClass.allFinite_formation
      K.2 L.2 with
    ⟨W, hKW, hLW⟩
  let I : CompletedGroupAlgebraOpenIdeal R :=
    ⟨(OrderDual.ofDual K.1).1 ⊓ (OrderDual.ofDual L.1).1, by
      simpa using (OrderDual.ofDual K.1).2.inter (OrderDual.ofDual L.1).2⟩
  refine ⟨(OrderDual.toDual I, W), ?_, ?_⟩
  · constructor
    · change (I.1 : Ideal R) ≤ (OrderDual.ofDual K.1).1
      exact inf_le_left
    · exact hKW
  · constructor
    · change (I.1 : Ideal R) ≤ (OrderDual.ofDual L.1).1
      exact inf_le_right
    · exact hLW

abbrev CompletedGroupAlgebraOpenQuotientStage
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Type (max u v)

def groupAlgebraOpenFiniteQuotientMap
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    MonoidAlgebra R G →+* CompletedGroupAlgebraOpenQuotientStage R G K

def groupAlgebraOpenFiniteQuotientKernel
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ideal (MonoidAlgebra R G)

theorem mem_groupAlgebraOpenFiniteQuotientKernel_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    {K : CompletedGroupAlgebraOpenQuotientIndex R G} {x : MonoidAlgebra R G} :
    x ∈ groupAlgebraOpenFiniteQuotientKernel R G K ↔
      groupAlgebraOpenFiniteQuotientMap R G K x = 0

def completedGroupAlgebraOpenFiniteQuotientTransition
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
    CompletedGroupAlgebraOpenQuotientStage R G L →+*
      CompletedGroupAlgebraOpenQuotientStage R G K

theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp_map
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
    (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
        (groupAlgebraOpenFiniteQuotientMap R G L) =
      groupAlgebraOpenFiniteQuotientMap R G K

def completedGroupAlgebraOpenFiniteQuotientProjection
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraOpenQuotientStage R G K

theorem completedGroupAlgebraOpenFiniteQuotientProjection_toCompletedGroupAlgebra
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    (completedGroupAlgebraOpenFiniteQuotientProjection R G K).comp
        (toCompletedGroupAlgebraRingHom R G) =
      groupAlgebraOpenFiniteQuotientMap R G K

theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp_projection
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
    (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
        (completedGroupAlgebraOpenFiniteQuotientProjection R G L) =
      completedGroupAlgebraOpenFiniteQuotientProjection R G K

theorem groupAlgebraOpenFiniteQuotientKernel_antitone
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
    groupAlgebraOpenFiniteQuotientKernel R G L ≤
      groupAlgebraOpenFiniteQuotientKernel R G K

def completedGroupAlgebraOpenFiniteQuotientStageTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K)

theorem completedGroupAlgebraOpenFiniteQuotientStage_discrete
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G K) := by
  let : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  exact ⟨rfl⟩

theorem continuous_completedGroupAlgebraStageCoeffQuotientMap_openIdeal
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
      (completedGroupAlgebraSystem R G).topologicalSpace K.2
    letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    Continuous (completedGroupAlgebraStageCoeffQuotientMap R G
      ((OrderDual.ofDual K.1).1 : Ideal R) K.2) := by
  let Iopen : CompletedGroupAlgebraOpenIdeal R := OrderDual.ofDual K.1
  let Q := CompletedGroupAlgebraQuotient G K.2
  let : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
    (completedGroupAlgebraSystem R G).topologicalSpace K.2
  let : TopologicalSpace (R ⧸ (Iopen.1 : Ideal R)) := ⊥
  have : DiscreteTopology (R ⧸ (Iopen.1 : Ideal R)) := ⟨rfl⟩
  have hmk : Continuous (Ideal.Quotient.mk (Iopen.1 : Ideal R)) :=
    continuous_idealQuotient_mk_openIdeal_discrete
      (R := R) (I := Iopen.1) Iopen.2
  have hcont :
      letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
        finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
      Continuous (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2) := by
    dsimp [CompletedGroupAlgebraStage, CompletedGroupAlgebraCoeffQuotientStage, Q]
    exact finiteGroupAlgebra_mapRangeRingHom_continuous
      (R := R) (S := R ⧸ (Iopen.1 : Ideal R)) Q
      (Ideal.Quotient.mk (Iopen.1 : Ideal R)) hmk
  have hdisc :
      letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
        finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
      DiscreteTopology (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) := by
    dsimp [CompletedGroupAlgebraCoeffQuotientStage, Q]
    exact finiteGroupAlgebraTopology_discrete_of_discrete_coeff
      (S := R ⧸ (Iopen.1 : Ideal R)) Q
  let tfin : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
  let tdisc : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  have ht : tfin = tdisc := by
    dsimp [tfin, tdisc, completedGroupAlgebraOpenFiniteQuotientStageTopology]
    exact hdisc.eq_bot
  change @Continuous (CompletedGroupAlgebraStage R G K.2)
    (CompletedGroupAlgebraOpenQuotientStage R G K)
    ((completedGroupAlgebraSystem R G).topologicalSpace K.2) tdisc
    (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2)
  rw [← ht]
  exact hcont

theorem continuous_completedGroupAlgebraOpenFiniteQuotientProjection
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    Continuous (completedGroupAlgebraOpenFiniteQuotientProjection R G K) := by
  let : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
    (completedGroupAlgebraSystem R G).topologicalSpace K.2
  let : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  exact (continuous_completedGroupAlgebraStageCoeffQuotientMap_openIdeal
    (R := R) (G := G) K).comp ((completedGroupAlgebraSystem R G).continuous_projection K.2)

def groupAlgebraOpenFiniteQuotientProductMap
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →
      (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
        CompletedGroupAlgebraOpenQuotientStage R G K

def groupAlgebraOpenFiniteQuotientKernelTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    TopologicalSpace (MonoidAlgebra R G)

theorem continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
        TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    Continuous (groupAlgebraOpenFiniteQuotientProductMap R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  let : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
      TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  exact continuous_induced_dom

theorem continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    letI : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    Continuous (groupAlgebraOpenFiniteQuotientMap R G K) := by
  let : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  let : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
      TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  change Continuous fun x : MonoidAlgebra R G =>
    groupAlgebraOpenFiniteQuotientProductMap R G x K
  exact (continuous_apply K).comp
    (continuous_groupAlgebraOpenFiniteQuotientProductMap_kernelTopology R G)

theorem groupAlgebraOpenFiniteQuotientKernel_isOpen_kernelTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    IsOpen (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) := by
  let : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  let : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
  have : DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G K) :=
    completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K
  change IsOpen ((groupAlgebraOpenFiniteQuotientMap R G K) ⁻¹'
    ({0} : Set (CompletedGroupAlgebraOpenQuotientStage R G K)))
  exact (isOpen_discrete ({0} : Set (CompletedGroupAlgebraOpenQuotientStage R G K))).preimage
    (continuous_groupAlgebraOpenFiniteQuotientMap_kernelTopology R G K)

theorem groupAlgebraOpenFiniteQuotientKernel_mem_nhds_zero_kernelTopology
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    letI : TopologicalSpace (MonoidAlgebra R G) :=
      groupAlgebraOpenFiniteQuotientKernelTopology R G
    (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) ∈
      𝓝 (0 : MonoidAlgebra R G) := by
  let : TopologicalSpace (MonoidAlgebra R G) :=
    groupAlgebraOpenFiniteQuotientKernelTopology R G
  apply IsOpen.mem_nhds
    (groupAlgebraOpenFiniteQuotientKernel_isOpen_kernelTopology R G K)
  change (0 : MonoidAlgebra R G) ∈ groupAlgebraOpenFiniteQuotientKernel R G K
  rw [mem_groupAlgebraOpenFiniteQuotientKernel_iff]
  exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)

theorem completedGroupAlgebraOpenFiniteQuotientTransition_single
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L)
    (q : CompletedGroupAlgebraQuotient G L.2)
    (r : R ⧸ ((OrderDual.ofDual L.1).1 : Ideal R)) :
    completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
        (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
          (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) hKL.2) q)
        (Ideal.Quotient.factor
          (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
            ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1) r) := by
  exact completedGroupAlgebraFiniteQuotientTransition_single (R := R) (G := G)
    (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
      ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
    (hUV := hKL.2) q r

theorem completedGroupAlgebraOpenFiniteQuotientTransition_id
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    completedGroupAlgebraOpenFiniteQuotientTransition R G (le_rfl : K ≤ K) =
      RingHom.id (CompletedGroupAlgebraOpenQuotientStage R G K)

theorem completedGroupAlgebraOpenFiniteQuotientTransition_comp
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    {K L M : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) (hLM : L ≤ M) :
    (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
        (completedGroupAlgebraOpenFiniteQuotientTransition R G hLM) =
      completedGroupAlgebraOpenFiniteQuotientTransition R G (hKL.trans hLM)

theorem completedGroupAlgebraOpenFiniteQuotientTransition_surjective
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
    Function.Surjective (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)