ProCInteger.lean

structure ProCIntegerIndex (C : FiniteGroupClass.{u}) where
  /-- The positive integer defining the coefficient ring `ZMod modulus` at this level. -/
  modulus : ℕ
  /-- The modulus is nonzero, as required for the finite cyclic coefficient group. -/
  positive : 0 < modulus
  /--
  The multiplicative presentation of the additive cyclic group `ZMod modulus` belongs to `C`,
  using universe-independent membership.
  -/
  cyclic_mem : C.MemAcrossUniverses (Multiplicative (ZMod modulus))

theorem memAcrossUniverses_of_ulift_mem
    {C : FiniteGroupClass.{u}} {G : Type} [Group G]
    (hG : C (ULift.{u} G)) : C.MemAcrossUniverses G

theorem ulift_mem_of_memAcrossUniverses
    {C : FiniteGroupClass.{u}} {G : Type} [Group G]
    (hG : C.MemAcrossUniverses G) : C (ULift.{u} G)

instance instLEProCIntegerIndex (C : FiniteGroupClass.{u}) : LE (ProCIntegerIndex C) where
  le i j := i.modulus ∣ j.modulus

instance instPreorderProCIntegerIndex (C : FiniteGroupClass.{u}) : Preorder (ProCIntegerIndex C)
    where
  le := (· ≤ ·)
  le_refl i := dvd_rfl
  le_trans _ _ _ hij hjk := dvd_trans hij hjk

def ofModulus {C : FiniteGroupClass.{u}} (n : ℕ) (hn : 0 < n)
    (hC : C.MemAcrossUniverses (Multiplicative (ZMod n))) : ProCIntegerIndex C where
  modulus := n
  positive := hn
  cyclic_mem := hC

theorem positiveFact {C : FiniteGroupClass.{u}} (i : ProCIntegerIndex C) :
    Fact (0 < i.modulus)

def terminal {C : FiniteGroupClass.{u}} (htriv : FiniteGroupClass.ContainsTrivialQuotients C) :
    ProCIntegerIndex C where
  modulus := 1
  positive := Nat.zero_lt_one
  cyclic_mem := memAcrossUniverses_of_ulift_mem (htriv.of_subsingleton inferInstance)

def ofAllFiniteModulus (n : ℕ) (hn : 0 < n) :
    ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}) where
  modulus := n
  positive := hn
  cyclic_mem := memAcrossUniverses_of_ulift_mem (by
    have : NeZero n := ⟨Nat.ne_of_gt hn⟩
    exact Finite.of_equiv (ZMod n) (Multiplicative.ofAdd.trans Equiv.ulift.symm))

theorem modulus_ofAllFiniteModulus (n : ℕ) (hn : 0 < n) :
    (ofAllFiniteModulus n hn).modulus = n

def ofElementOrder {C : FiniteGroupClass.{u}}
    (hHer : FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [Finite K] (hK : C K) (k : K) :
    ProCIntegerIndex C

theorem directed_of_formation {C : FiniteGroupClass.{u}} (hForm : FiniteGroupClass.Formation C) :
    Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)

theorem exists_index_orderOf_dvd_of_finite_mem {C : FiniteGroupClass.{u}}
    (hForm : FiniteGroupClass.Formation C)
    (hHer : FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [Finite K] (hK : C K) :
    ∃ i : ProCIntegerIndex C, ∀ k : K, orderOf k ∣ i.modulus

theorem exists_index_kills_finite_group_of_mem {C : FiniteGroupClass.{u}}
    (hForm : FiniteGroupClass.Formation C)
    (hHer : FiniteGroupClass.Hereditary C)
    {K : Type u} [Group K] [Finite K] (hK : C K) :
    ∃ i : ProCIntegerIndex C, ∀ k : K, k ^ i.modulus = 1

abbrev ProCIntegerStage (i : ProCIntegerIndex C) : Type

def proCIntegerTransition {i j : ProCIntegerIndex C} (hij : i ≤ j) :
    ProCIntegerStage C j →+* ProCIntegerStage C i

def proCIntegerSystem : ProCGroups.InverseSystems.InverseSystem (I := ProCIntegerIndex C) where
  X := ProCIntegerStage C
  topologicalSpace := fun _ => inferInstance
  map := fun {i j} hij => proCIntegerTransition (C := C) hij
  continuous_map := by
    intro i j hij
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    ext x
    simp only [proCIntegerTransition, ZMod.castHom_self, RingHom.id_apply, id_eq]
  map_comp := by
    intro i j k hij hjk
    ext x
    exact congrArg (fun f : ZMod k.modulus →+* ZMod i.modulus => f x)
      (ZMod.castHom_comp hij hjk)

def ProCIntegerCompatible
    (x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) : Prop

abbrev ProCIntegerLimitCarrier : Type _

def proCIntegerProj (i : ProCIntegerIndex C) : ProCIntegerLimitCarrier C → ProCIntegerStage C i

theorem ProCIntegerLimitCarrier.ext {x y : ProCIntegerLimitCarrier C}
    (h : ∀ i : ProCIntegerIndex C,
      proCIntegerProj (C := C) i x = proCIntegerProj (C := C) i y) :
    x = y

instance instZeroProCInteger : Zero (ProCIntegerLimitCarrier C) where
  zero := ⟨fun _ => 0, by
    intro i j hij
    exact map_zero (proCIntegerTransition (C := C) hij)⟩

instance instAddProCInteger : Add (ProCIntegerLimitCarrier C) where
  add x y := ⟨fun i => x.1 i + y.1 i, by
    intro i j hij
    rw [map_add]
    exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

instance instNegProCInteger : Neg (ProCIntegerLimitCarrier C) where
  neg x := ⟨fun i => -x.1 i, by
    intro i j hij
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩

instance instSubProCInteger : Sub (ProCIntegerLimitCarrier C) where
  sub x y := ⟨fun i => x.1 i - y.1 i, by
    intro i j hij
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

instance instSMulNatProCInteger : SMul ℕ (ProCIntegerLimitCarrier C) where
  smul n x := ⟨fun i => n • x.1 i, by
    intro i j hij
    rw [map_nsmul]
    exact congrArg (n • ·) (x.2 i j hij)⟩

instance instSMulIntProCInteger : SMul ℤ (ProCIntegerLimitCarrier C) where
  smul n x := ⟨fun i => n • x.1 i, by
    intro i j hij
    rw [map_zsmul]
    exact congrArg (n • ·) (x.2 i j hij)⟩

instance instOneProCInteger : One (ProCIntegerLimitCarrier C) where
  one := ⟨fun _ => 1, by
    intro i j hij
    exact map_one (proCIntegerTransition (C := C) hij)⟩

instance instMulProCInteger : Mul (ProCIntegerLimitCarrier C) where
  mul x y := ⟨fun i => x.1 i * y.1 i, by
    intro i j hij
    rw [map_mul]
    exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩

instance instNatCastProCInteger : NatCast (ProCIntegerLimitCarrier C) where
  natCast n := ⟨fun _ => n, by
    intro i j hij
    exact map_natCast (proCIntegerTransition (C := C) hij) n⟩

instance instIntCastProCInteger : IntCast (ProCIntegerLimitCarrier C) where
  intCast n := ⟨fun _ => n, by
    intro i j hij
    exact map_intCast (proCIntegerTransition (C := C) hij) n⟩

instance instPowProCInteger : Pow (ProCIntegerLimitCarrier C) ℕ where
  pow x n := ⟨fun i => x.1 i ^ n, by
    intro i j hij
    rw [map_pow]
    exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩

theorem coe_zero_proCInteger :
    ((0 : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = 0

theorem coe_one_proCInteger :
    ((1 : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = 1

theorem coe_add_proCInteger (x y : ProCIntegerLimitCarrier C) :
    ((x + y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x +
        y

theorem coe_mul_proCInteger (x y : ProCIntegerLimitCarrier C) :
    ((x * y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x *
        y

theorem coe_neg_proCInteger (x : ProCIntegerLimitCarrier C) :
    ((-x : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = -x

theorem coe_sub_proCInteger (x y : ProCIntegerLimitCarrier C) :
    ((x - y : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x -
        y

theorem coe_natCast_proCInteger (n : ℕ) :
    ((n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = n

theorem coe_intCast_proCInteger (n : ℤ) :
    ((n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) =
      fun i => (n : ProCIntegerStage C i) := by
  funext i
  rfl

theorem coe_pow_proCInteger (x : ProCIntegerLimitCarrier C) (n : ℕ) :
    ((x ^ n : ProCIntegerLimitCarrier C) : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i) = x ^
        n

instance instCommRingProCInteger : CommRing (ProCIntegerLimitCarrier C)

theorem proCIntegerProj_zero (i : ProCIntegerIndex C) :
    proCIntegerProj (C := C) i (0 : ProCIntegerLimitCarrier C) = 0

theorem proCIntegerProj_one (i : ProCIntegerIndex C) :
    proCIntegerProj (C := C) i (1 : ProCIntegerLimitCarrier C) = 1

theorem proCIntegerProj_add (i : ProCIntegerIndex C) (x y : ProCIntegerLimitCarrier C) :
    proCIntegerProj (C := C) i (x + y) =
      proCIntegerProj (C := C) i x + proCIntegerProj (C := C) i y

theorem proCIntegerProj_mul (i : ProCIntegerIndex C) (x y : ProCIntegerLimitCarrier C) :
    proCIntegerProj (C := C) i (x * y) =
      proCIntegerProj (C := C) i x * proCIntegerProj (C := C) i y

theorem proCIntegerProj_neg (i : ProCIntegerIndex C) (x : ProCIntegerLimitCarrier C) :
    proCIntegerProj (C := C) i (-x) = -proCIntegerProj (C := C) i x

theorem proCIntegerProj_sub (i : ProCIntegerIndex C) (x y : ProCIntegerLimitCarrier C) :
    proCIntegerProj (C := C) i (x - y) =
      proCIntegerProj (C := C) i x - proCIntegerProj (C := C) i y

theorem proCIntegerProj_natCast (i : ProCIntegerIndex C) (n : ℕ) :
    proCIntegerProj (C := C) i (n : ProCIntegerLimitCarrier C) = n

theorem proCIntegerProj_intCast (i : ProCIntegerIndex C) (n : ℤ) :
    proCIntegerProj (C := C) i (n : ProCIntegerLimitCarrier C) = n

def proCIntegerProjRingHom (i : ProCIntegerIndex C) :
    ProCIntegerLimitCarrier C →+* ProCIntegerStage C i where
  toFun := proCIntegerProj (C := C) i
  map_zero' := by simp only [proCIntegerProj_zero]
  map_one' := by simp only [proCIntegerProj_one]
  map_add' := by intro x y; simp only [proCIntegerProj_add]
  map_mul' := by intro x y; simp only [proCIntegerProj_mul]

theorem proCIntegerProjRingHom_apply (i : ProCIntegerIndex C) (x : ProCIntegerLimitCarrier C) :
    proCIntegerProjRingHom (C := C) i x = proCIntegerProj (C := C) i x

theorem continuous_proCIntegerProj (i : ProCIntegerIndex C) :
    Continuous (proCIntegerProj (C := C) i)

theorem proCIntegerProj_transition {i j : ProCIntegerIndex C} (hij : i ≤ j)
    (x : ProCIntegerLimitCarrier C) :
    proCIntegerTransition (C := C) hij (proCIntegerProj (C := C) j x) =
      proCIntegerProj (C := C) i x

theorem multiplicative_proCIntegerStage_mem
    {C : FiniteGroupClass.{u}} (i : ProCIntegerIndex C) :
    C.MemAcrossUniverses (Multiplicative (ProCIntegerStage C i))

theorem hasOpenNormalBasisInClass_multiplicative_proCIntegerStage
    {C : FiniteGroupClass.{0}}
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (i : ProCIntegerIndex C) :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (Multiplicative (ProCIntegerStage C i))

def proCIntegerMultiplicativeSystem (C : FiniteGroupClass.{u}) :
    ProCGroups.InverseSystems.InverseSystem (I := ProCIntegerIndex C) where
  X := fun i => Multiplicative (ProCIntegerStage C i)
  topologicalSpace := fun _ => inferInstance
  map := fun {i j} hij =>
    (proCIntegerTransition (C := C) hij).toAddMonoidHom.toMultiplicative
  continuous_map := by
    intro i j hij
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    ext x
    apply Multiplicative.ext
    change proCIntegerTransition (C := C) (le_rfl : i ≤ i) x.toAdd = x.toAdd
    simp only [proCIntegerTransition, ZMod.castHom_self, RingHom.id_apply]
  map_comp := by
    intro i j k hij hjk
    ext x
    apply Multiplicative.ext
    change
      proCIntegerTransition (C := C) hij
          (proCIntegerTransition (C := C) hjk x.toAdd) =
        proCIntegerTransition (C := C) (hij.trans hjk) x.toAdd
    exact congrArg (fun f : ZMod k.modulus →+* ZMod i.modulus => f x.toAdd)
      (ZMod.castHom_comp hij hjk)

instance instGroupProCIntegerMultiplicativeSystemStage
    (C : FiniteGroupClass.{u}) (i : ProCIntegerIndex C) :
    Group ((proCIntegerMultiplicativeSystem C).X i)

instance instIsTopologicalGroupProCIntegerMultiplicativeSystemStage
    (C : FiniteGroupClass.{u}) (i : ProCIntegerIndex C) :
    IsTopologicalGroup ((proCIntegerMultiplicativeSystem C).X i)

instance instIsGroupSystemProCIntegerMultiplicativeSystem
    (C : FiniteGroupClass.{u}) :
    ProCGroups.InverseSystems.IsGroupSystem
      (proCIntegerMultiplicativeSystem C) where
  map_one := by
    intro i j hij
    dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage]
    apply Multiplicative.ext
    exact map_zero (proCIntegerTransition (C := C) hij)
  map_mul := by
    intro i j hij x y
    dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage] at x y ⊢
    apply Multiplicative.ext
    exact map_add (proCIntegerTransition (C := C) hij) x.toAdd y.toAdd
  map_inv := by
    intro i j hij x
    dsimp [proCIntegerMultiplicativeSystem, ProCIntegerStage] at x ⊢
    apply Multiplicative.ext
    exact map_neg (proCIntegerTransition (C := C) hij) x.toAdd

def proCIntegerMultiplicativeLimitEquiv
    (C : FiniteGroupClass.{u}) :
    (proCIntegerMultiplicativeSystem C).inverseLimit ≃ₜ*
      Multiplicative (ProCIntegerLimitCarrier C)

theorem hasOpenNormalBasisInClass_proCIntegerMultiplicativeSystem_inverseLimit
    {C : FiniteGroupClass.{0}}
    [Nonempty (ProCIntegerIndex C)]
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (proCIntegerMultiplicativeSystem C).inverseLimit

theorem isClosed_setOf_proCIntegerCompatible :
    IsClosed {x : ∀ i : ProCIntegerIndex C, ProCIntegerStage C i |
      ProCIntegerCompatible C x}

instance instCompactSpaceProCInteger : CompactSpace (ProCIntegerLimitCarrier C)

instance instT2SpaceProCInteger : T2Space (ProCIntegerLimitCarrier C)

instance instContinuousAddProCInteger : ContinuousAdd (ProCIntegerLimitCarrier C) where
  continuous_add := by
    refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 + p.2).2)
    change Continuous fun p : ProCIntegerLimitCarrier C × ProCIntegerLimitCarrier C =>
      proCIntegerProj (C := C) i p.1 + proCIntegerProj (C := C) i p.2
    exact ((continuous_proCIntegerProj (C := C) i).comp continuous_fst).add
      ((continuous_proCIntegerProj (C := C) i).comp continuous_snd)

instance instContinuousMulProCInteger : ContinuousMul (ProCIntegerLimitCarrier C) where
  continuous_mul := by
    refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun p => (p.1 * p.2).2)
    change Continuous fun p : ProCIntegerLimitCarrier C × ProCIntegerLimitCarrier C =>
      proCIntegerProj (C := C) i p.1 * proCIntegerProj (C := C) i p.2
    exact ((continuous_proCIntegerProj (C := C) i).comp continuous_fst).mul
      ((continuous_proCIntegerProj (C := C) i).comp continuous_snd)

instance instContinuousNegProCInteger : ContinuousNeg (ProCIntegerLimitCarrier C) where
  continuous_neg := by
    refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x => (-x).2)
    change Continuous fun x : ProCIntegerLimitCarrier C => -proCIntegerProj (C := C) i x
    exact (continuous_proCIntegerProj (C := C) i).neg

instance instIsTopologicalRingProCInteger : IsTopologicalRing (ProCIntegerLimitCarrier C)

theorem hasOpenNormalBasisInClass_multiplicative_proCInteger
    {C : FiniteGroupClass.{0}}
    [Nonempty (ProCIntegerIndex C)]
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
    ProCGroups.ProC.HasOpenNormalBasisInClass C (Multiplicative (ProCIntegerLimitCarrier C))

def intToProCInteger : ℤ →+* ProCIntegerLimitCarrier C where
  toFun n := (n : ProCIntegerLimitCarrier C)
  map_zero' := by ext i; exact Int.cast_zero
  map_one' := by ext i; exact Int.cast_one
  map_add' := by intro m n; ext i; exact Int.cast_add m n
  map_mul' := by intro m n; ext i; exact Int.cast_mul m n

theorem intToProCInteger_apply (n : ℤ) :
    intToProCInteger (C := C) n = (n : ProCIntegerLimitCarrier C)

theorem proCIntegerProj_intToProCInteger (i : ProCIntegerIndex C) (n : ℤ) :
    proCIntegerProj (C := C) i (intToProCInteger (C := C) n) = (n : ZMod i.modulus)

theorem denseRange_intToProCInteger_of_directed
    [Nonempty (ProCIntegerIndex C)]
    (hdir : Directed (· ≤ ·) (id : ProCIntegerIndex C → ProCIntegerIndex C)) :
    DenseRange (intToProCInteger (C := C))

theorem directed_proCIntegerIndex_allFinite :
    Directed (· ≤ ·)
      (id : ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}) →
        ProCIntegerIndex (FiniteGroupClass.allFinite : FiniteGroupClass.{u}))

theorem hasOpenNormalBasisInClass_multiplicative_proCInteger_allFinite :
    ProCGroups.ProC.HasOpenNormalBasisInClass
      (FiniteGroupClass.allFinite : FiniteGroupClass.{0})
      (Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))

theorem denseRange_intToProCInteger_allFinite :
    DenseRange (intToProCInteger
      (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u})))

def proCIntegerOne : Multiplicative (ProCIntegerLimitCarrier C)

def multiplicativeIntToProCInteger :
    Multiplicative ℤ →* Multiplicative (ProCIntegerLimitCarrier C) where
  toFun z := Multiplicative.ofAdd ((z.toAdd : ℤ) : ProCIntegerLimitCarrier C)
  map_one' := by
    apply Multiplicative.ext
    simp only [toAdd_one, Int.cast_zero, ofAdd_zero]
  map_mul' z w := by
    apply Multiplicative.ext
    ext i
    change (((z * w).toAdd : ℤ) : ProCIntegerStage C i) =
      ((z.toAdd : ℤ) : ProCIntegerStage C i) + ((w.toAdd : ℤ) : ProCIntegerStage C i)
    exact Int.cast_add z.toAdd w.toAdd

theorem multiplicativeIntToProCInteger_apply (n : ℤ) :
    multiplicativeIntToProCInteger (C := C) (Multiplicative.ofAdd n) =
      Multiplicative.ofAdd ((n : ℤ) : ProCIntegerLimitCarrier C)

theorem multiplicativeIntToProCInteger_zpow_one (n : ℤ) :
    multiplicativeIntToProCInteger (C := C) (Multiplicative.ofAdd n) =
      (proCIntegerOne (C := C)) ^ n

theorem denseRange_multiplicativeIntToProCInteger_allFinite :
    DenseRange
      (multiplicativeIntToProCInteger
        (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{u})))

theorem topologicallyGenerates_singleton_proCIntegerOne_allFinite :
    ProCGroups.Generation.TopologicallyGenerates
      (G := Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))
      ({(proCIntegerOne
        (C := (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))} : Set _)

theorem hasCyclicOpenNormalBasis_multiplicative_proCInteger_allFinite :
    ProCGroups.ProC.HasCyclicOpenNormalBasis
      (Multiplicative
        (ProCIntegerLimitCarrier (FiniteGroupClass.allFinite : FiniteGroupClass.{0})))