ProfiniteIntegerFiniteQuotient.lean

theorem finiteIndexNormalAddSubgroup_eq_zmultiples_index
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    H.toAddSubgroup =
      AddSubgroup.zmultiples (H.toAddSubgroup.index : ℤ)

theorem finiteIndexNormalAddSubgroup_index_pos
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    0 < H.toAddSubgroup.index

theorem finiteIndexNormalAddSubgroup_index_mem
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    (H.toAddSubgroup.index : ℤ) ∈ H.toAddSubgroup

def zHatFiniteIndexQuotientReduction
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    ZMod H.toAddSubgroup.index →+ ℤ ⧸ H.toAddSubgroup

def zHatReductionToFiniteIndexQuotient
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    ZHat →ₜ+ ℤ ⧸ H.toAddSubgroup

theorem zHatReductionToFiniteIndexQuotient_intCast
    (H : FiniteIndexNormalAddSubgroup ℤ) (a : ℤ) :
    zHatReductionToFiniteIndexQuotient H (a : ZHat) =
      QuotientAddGroup.mk' H.toAddSubgroup a

def zHatFiniteIndexQuotientDiagramLeg
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    zHatProfiniteAddGrp ⟶
      (ProfiniteAddGrp.ProfiniteCompletion.diagram (AddGrpCat.of ℤ)).obj H

theorem zHatFiniteIndexQuotientDiagramLeg_intCast
    (H : FiniteIndexNormalAddSubgroup ℤ) (a : ℤ) :
    (zHatFiniteIndexQuotientDiagramLeg H).hom (a : ZHat) =
      QuotientAddGroup.mk' H.toAddSubgroup a

theorem zHatFiniteIndexQuotientDiagramLeg_naturality
    {H K : FiniteIndexNormalAddSubgroup ℤ} (f : H ⟶ K) :
    zHatFiniteIndexQuotientDiagramLeg H ≫
        (ProfiniteAddGrp.ProfiniteCompletion.diagram (AddGrpCat.of ℤ)).map f =
      zHatFiniteIndexQuotientDiagramLeg K

def zHatFiniteIndexQuotientCone :
    Cone (ProfiniteAddGrp.ProfiniteCompletion.diagram (AddGrpCat.of ℤ)) where
  pt := zHatProfiniteAddGrp
  π :=
    { app := zHatFiniteIndexQuotientDiagramLeg
      naturality := by
        intro H K f
        change 𝟙 zHatProfiniteAddGrp ≫ zHatFiniteIndexQuotientDiagramLeg K =
          zHatFiniteIndexQuotientDiagramLeg H ≫
            (ProfiniteAddGrp.ProfiniteCompletion.diagram (AddGrpCat.of ℤ)).map f
        simpa only [Category.id_comp] using
          (zHatFiniteIndexQuotientDiagramLeg_naturality f).symm }

def zHatToIntegerProfiniteCompletion :
    zHatProfiniteAddGrp ⟶
      ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of ℤ)

theorem zHatToIntegerProfiniteCompletion_fac
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    zHatToIntegerProfiniteCompletion ≫
        (ProfiniteAddGrp.limitCone
          (ProfiniteAddGrp.ProfiniteCompletion.diagram (AddGrpCat.of ℤ))).π.app H =
      zHatFiniteIndexQuotientDiagramLeg H

theorem zHatToIntegerProfiniteCompletion_intCast
    (a : ℤ) :
    zHatToIntegerProfiniteCompletion (a : ZHat) =
      ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of ℤ) a

theorem zHatFiniteIndexQuotientReduction_injective
    (H : FiniteIndexNormalAddSubgroup ℤ) :
    Function.Injective (zHatFiniteIndexQuotientReduction H)

theorem zHatToIntegerProfiniteCompletion_injective :
    Function.Injective
      (fun z : ZHat => zHatToIntegerProfiniteCompletion z) := by
  intro x y hxy
  apply ZHat.ext
  intro n hn
  have hnatAbs : (n : ℤ).natAbs = n := by
    cases n <;> rfl
  let H : FiniteIndexNormalAddSubgroup ℤ :=
    { toAddSubgroup := AddSubgroup.zmultiples (n : ℤ)
      isFiniteIndex' :=
        ⟨by
          simpa only [Int.index_zmultiples, hnatAbs] using
            Nat.ne_of_gt hn⟩ }
  have hindex : H.toAddSubgroup.index = n := by
    simp only [H, Int.index_zmultiples, hnatAbs]
  have hprojection := congrArg
    (fun z =>
      ((ProfiniteAddGrp.limitCone
        (ProfiniteAddGrp.ProfiniteCompletion.diagram
          (AddGrpCat.of ℤ))).π.app H).hom z)
    hxy
  have hleg :
      (zHatFiniteIndexQuotientDiagramLeg H).hom x =
        (zHatFiniteIndexQuotientDiagramLeg H).hom y := by
    calc
      (zHatFiniteIndexQuotientDiagramLeg H).hom x =
          ((ProfiniteAddGrp.limitCone
            (ProfiniteAddGrp.ProfiniteCompletion.diagram
              (AddGrpCat.of ℤ))).π.app H).hom
            (zHatToIntegerProfiniteCompletion x) :=
        (ConcreteCategory.congr_hom
          (zHatToIntegerProfiniteCompletion_fac H) x).symm
      _ = ((ProfiniteAddGrp.limitCone
            (ProfiniteAddGrp.ProfiniteCompletion.diagram
              (AddGrpCat.of ℤ))).π.app H).hom
            (zHatToIntegerProfiniteCompletion y) := hprojection
      _ = (zHatFiniteIndexQuotientDiagramLeg H).hom y :=
        ConcreteCategory.congr_hom
          (zHatToIntegerProfiniteCompletion_fac H) y
  have hreduction :
      zHatReduction H.toAddSubgroup.index
          (finiteIndexNormalAddSubgroup_index_pos H) x =
        zHatReduction H.toAddSubgroup.index
          (finiteIndexNormalAddSubgroup_index_pos H) y := by
    apply zHatFiniteIndexQuotientReduction_injective H
    change zHatReductionToFiniteIndexQuotient H x =
      zHatReductionToFiniteIndexQuotient H y
    exact hleg
  have hreductionAll :
      ∀ hm : 0 < H.toAddSubgroup.index,
        zHatReduction H.toAddSubgroup.index hm x =
          zHatReduction H.toAddSubgroup.index hm y := by
    intro hm
    exact hreduction
  have hreductionAtN :
      ∀ hm : 0 < n,
        zHatReduction n hm x = zHatReduction n hm y :=
    hindex ▸ hreductionAll
  exact hreductionAtN hn

theorem zHatToIntegerProfiniteCompletion_surjective :
    Function.Surjective
      (fun z : ZHat => zHatToIntegerProfiniteCompletion z) := by
  have hsubset :
      Set.range
          (ProfiniteAddGrp.ProfiniteCompletion.etaFn
            (AddGrpCat.of ℤ)) ⊆
        Set.range (fun z : ZHat => zHatToIntegerProfiniteCompletion z) := by
    rintro _ ⟨a, rfl⟩
    exact ⟨(a : ZHat), zHatToIntegerProfiniteCompletion_intCast a⟩
  have hdense : DenseRange
      (fun z : ZHat => zHatToIntegerProfiniteCompletion z) :=
    (ProfiniteAddGrp.ProfiniteCompletion.denseRange
      (G := AddGrpCat.of ℤ)).mono hsubset
  have hclosed : IsClosed
      (Set.range (fun z : ZHat => zHatToIntegerProfiniteCompletion z)) :=
    zHatToIntegerProfiniteCompletion.hom.continuous_toFun.isClosedMap.isClosed_range
  rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr hclosed,
    Dense.closure_eq hdense]

def zHatContinuousAddEquivIntegerProfiniteCompletion :
    ZHat ≃ₜ+
      ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of ℤ)

theorem zHatContinuousAddEquivIntegerProfiniteCompletion_apply (z : ZHat) :
    zHatContinuousAddEquivIntegerProfiniteCompletion z =
      zHatToIntegerProfiniteCompletion z

def integerProfiniteCompletionToZHat :
    ProfiniteAddGrp.ProfiniteCompletion.completion (AddGrpCat.of ℤ) ⟶
      zHatProfiniteAddGrp

theorem integerProfiniteCompletionToZHat_etaFn (a : ℤ) :
    integerProfiniteCompletionToZHat
        (ProfiniteAddGrp.ProfiniteCompletion.etaFn (AddGrpCat.of ℤ) a) =
      (a : ZHat)

theorem zHatContinuousAddEquivIntegerProfiniteCompletion_symm_apply
    (x : ProfiniteAddGrp.ProfiniteCompletion.completion
      (AddGrpCat.of ℤ)) :
    zHatContinuousAddEquivIntegerProfiniteCompletion.symm x =
      integerProfiniteCompletionToZHat x