FiniteQuotients.lean

theorem profiniteModule_hasFiniteIndexSubmoduleBasis_of_linearTopology
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
    [TopologicalSpace M] [Module Λ M] [IsLinearTopology Λ M]
    [IsTopologicalAddGroup M] [CompactSpace M] :
    HasFiniteIndexSubmoduleBasis Λ M

theorem profiniteModule_hasFiniteIndexSubmoduleBasis
    (Λ : Type u) (M : Type v) [Ring Λ] [TopologicalSpace Λ] [AddCommGroup M]
    [TopologicalSpace M] [Module Λ M] [IsTopologicalRing Λ] [CompactSpace Λ]
    [IsTopologicalAddGroup M] [ContinuousSMul Λ M] [CompactSpace M] [T2Space M]
    [TotallyDisconnectedSpace M] :
    HasFiniteIndexSubmoduleBasis Λ M

theorem profiniteModule_ext_of_openSubmoduleQuotients
    {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
    [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [IsTopologicalRing R] [CompactSpace R] [IsTopologicalAddGroup N]
    [ContinuousSMul R N] [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
    {x y : N}
    (h : ∀ W : Submodule R N, IsOpen (W : Set N) → Submodule.mkQ W x = Submodule.mkQ W y) :
    x = y

abbrev ProfiniteModuleOpenSubmodule
    (R : Type u) (N : Type v) [Ring R] [AddCommGroup N] [Module R N]
    [TopologicalSpace N] : Type _

theorem continuous_of_forall_openSubmodule_quotient_continuous
    {R : Type u} (N : Type v) [Ring R] [TopologicalSpace R]
    [AddCommGroup N] [TopologicalSpace N] [Module R N]
    [IsTopologicalRing R] [CompactSpace R] [IsTopologicalAddGroup N]
    [ContinuousSMul R N] [CompactSpace N] [T2Space N] [TotallyDisconnectedSpace N]
    {Y : Type z} [TopologicalSpace Y] {F : Y → N}
    (hF : ∀ W : Submodule R N, IsOpen (W : Set N) →
      Continuous fun y : Y => Submodule.mkQ W (F y)) :
    Continuous F := by
  rw [continuous_iff_continuousAt]
  intro y
  rw [continuousAt_def]
  intro A hA
  rcases mem_nhds_iff.mp hA with ⟨O, hOA, hOopen, hFO⟩
  let U0 : Set N := {z | F y + z ∈ O}
  have hU0 : U0 ∈ 𝓝 (0 : N) := by
    apply IsOpen.mem_nhds
    · exact hOopen.preimage (continuous_const.add continuous_id)
    · simp only [Set.mem_ofPred_eq, add_zero, hFO, U0]
  rcases profiniteModule_hasFiniteIndexSubmoduleBasis R N U0 hU0 with
    ⟨W, hWopen, hWU, _hfinite⟩
  let hdisc : IsDiscreteModule R (N ⧸ W) :=
    quotient_openSubmodule_isDiscreteModule R N W hWopen
  let : DiscreteTopology (N ⧸ W) := hdisc.2
  let q : Y → N ⧸ W := fun z => Submodule.mkQ W (F z)
  let B : Set (N ⧸ W) := {Submodule.mkQ W (F y)}
  have hqcont : Continuous q := hF W hWopen
  have hpreOpen : IsOpen (q ⁻¹' B) := (isOpen_discrete B).preimage hqcont
  have hypre : y ∈ q ⁻¹' B := by
    simp only [Submodule.mkQ_apply, Set.mem_preimage, Set.mem_singleton_iff, q, B]
  refine Filter.mem_of_superset (hpreOpen.mem_nhds hypre) ?_
  intro z hz
  apply hOA
  have hquot : Submodule.mkQ W (F z) = Submodule.mkQ W (F y) := by
    simpa [q, B] using hz
  rw [Submodule.mkQ_apply, Submodule.mkQ_apply] at hquot
  have hdiff : F z - F y ∈ W := (Submodule.Quotient.eq W).1 hquot
  have hU : F z - F y ∈ U0 := hWU hdiff
  change F y + (F z - F y) ∈ O at hU
  simpa [sub_eq_add_neg, add_assoc, add_comm, add_left_comm] using hU

theorem exists_openSubmodule_le_finset
    {R : Type u} (N : Type v) [Ring R] [AddCommGroup N] [TopologicalSpace N] [Module R N]
    (s : Finset (ProfiniteModuleOpenSubmodule (R := R) N)) :
    ∃ K : ProfiniteModuleOpenSubmodule (R := R) N,
      ∀ W ∈ s, K.1 ≤ W.1