Module

FiniteQuotientLifts.lean

Nyll.ProCGroups.Completion.FiniteQuotientLifts

2 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Completion / Finite Quotient Lifts

This module proves that unique lifting against finite discrete \(C\)-quotients, together with density, implies the full pro-\(C\) completion universal property.

Imports3

Imported by3

def

lift_to_inverseLimit_of_compatible_finite_lifts

L28 ↗

ProCGroups.Completion.lift_to_inverseLimit_of_compatible_finite_lifts

Documentation

A compatible family of continuous homomorphisms to finite stages assembles to a continuous homomorphism to the inverse limit.

Source context 3 commands

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

open scoped Topology
namespace ProCGroups.Completion
universe u

Lean source · full declaration

def lift_to_inverseLimit_of_compatible_finite_lifts
    {I : Type u} [Preorder I]
    (S : ProCGroups.InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
    {A : Type u} [Group A] [TopologicalSpace A]
    (φ : ∀ i, A →ₜ* S.X i)
    (hcompat : S.CompatibleMaps (fun i => φ i)) :
    A →ₜ* S.inverseLimit :=
  { toMonoidHom :=
      { toFun := S.inverseLimitLift (fun i => φ i) hcompat
        map_one' := by
          apply S.ext
          intro i
          calc
            S.projection i (S.inverseLimitLift (fun i => φ i) hcompat 1) = φ i 1 := by
              exact S.projection_inverseLimitLift_apply (fun i => φ i) hcompat i (1 : A)
            _ = 1 := by simp only [map_one]
        map_mul' := by
          intro x y
          apply S.ext
          intro i
          calc
            S.projection i (S.inverseLimitLift (fun i => φ i) hcompat (x * y)) = φ i (x * y) := by
              exact S.projection_inverseLimitLift_apply (fun i => φ i) hcompat i (x * y)
            _ = φ i x * φ i y := by simp only [map_mul]
            _ =
                S.projection i (S.inverseLimitLift (fun i => φ i) hcompat x) *
                  S.projection i (S.inverseLimitLift (fun i => φ i) hcompat y) := by
              have hx :
                  S.projection i (S.inverseLimitLift (fun i => φ i) hcompat x) = φ i x := by
                exact S.projection_inverseLimitLift_apply (fun i => φ i) hcompat i x
              have hy :
                  S.projection i (S.inverseLimitLift (fun i => φ i) hcompat y) = φ i y := by
                exact S.projection_inverseLimitLift_apply (fun i => φ i) hcompat i y
              rw [← hx, ← hy] }
    continuous_toFun := S.continuous_inverseLimitLift (fun i => φ i) (fun i => (φ
        i).continuous_toFun)
      hcompat }

theorem

isProCCompletion_of_finiteQuotientLifts

L71 ↗

ProCGroups.Completion.isProCCompletion_of_finiteQuotientLifts