ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies

7 Theorem

This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.

Open this file on GitHub

import

Imported by

Theorem ProCGroups.ProC.directed_finset_has_lower_bound GitHub

theorem directed_finset_has_lower_bound {α : Type*} {ι : Type*} {U : ι → Set α}
    (hdir : Directed (· ⊇ ·) U) :
    ∀ s : Finset ι, s.Nonempty → ∃ k : ι, ∀ i ∈ s, U k ⊆ U i

A nonempty finite subfamily of a directed family of sets has a common lower bound for the reverse-inclusion order.

Show proof

Theorem ProCGroups.ProC.closedSubgroup_mul_iInter_eq_iInter_mul GitHub

theorem closedSubgroup_mul_iInter_eq_iInter_mul [CompactSpace G]
    (H : ClosedSubgroup G) {ι : Type v} (U : ι → Set G)
    (hclosed : ∀ i, IsClosed (U i))
    (hdir : Directed (· ⊇ ·) U) :
    ((H : Set G) * ⋂ i, U i) = ⋂ i, ((H : Set G) * U i)

For a closed subgroup of a profinite group, multiplication by the intersection of a filtered family of closed sets is the intersection of the products.

Show proof

Theorem ProCGroups.ProC.continuous_surjective_image_iInter_eq_iInter_image GitHub

theorem continuous_surjective_image_iInter_eq_iInter_image {X : Type u}
    [TopologicalSpace X] [CompactSpace X] {R : Type v} [TopologicalSpace R] [T2Space R]
    (φ : X → R) (hφ : Continuous φ) (hsurj : Function.Surjective φ)
    {ι : Type w} (U : ι → Set X)
    (hclosed : ∀ i, IsClosed (U i))
    (hdir : Directed (· ⊇ ·) U) :
    φ '' ⋂ i, U i = ⋂ i, φ '' U i

Continuous surjections commute with the intersection of a filtered family of closed sets in a compact domain.

Show proof

Theorem ProCGroups.ProC.exists_openNormalSubgroup_mul_subset_openSubgroup GitHub

theorem exists_openNormalSubgroup_mul_subset_openSubgroup [CompactSpace G]
    (H : ClosedSubgroup G) (V : OpenSubgroup G)
    (hHV : (H : Subgroup G) ≤ (V : Subgroup G)) :
    ∃ U : OpenNormalSubgroup G, ((H : Set G) * (U : Set G)) ⊆ (V : Set G)

Every open subgroup containing a closed subgroup also contains a set of the form \(H U\) with \(U\) open and normal.

Show proof

Theorem ProCGroups.ProC.closedSubgroup_eq_sInf_openNormal GitHub

theorem closedSubgroup_eq_sInf_openNormal [CompactSpace G] [TotallyDisconnectedSpace G]
    (H : ClosedSubgroup G) [((H : Subgroup G).Normal)] :
    (H : Subgroup G) =
      sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N ∧ N.Normal}

A closed normal subgroup of a profinite group is the intersection of all open normal subgroups containing it.

Show proof

Theorem ProCGroups.finite_iInter_subgroup_subset_openSubgroup GitHub

theorem finite_iInter_subgroup_subset_openSubgroup [CompactSpace G] {ι : Type v}
    (H : ι → Subgroup G)
    (hclosed : ∀ i, IsClosed (((H i : Subgroup G) : Set G)))
    (U : OpenSubgroup G)
    (hInter : (⋂ i, (((H i : Subgroup G) : Set G))) ⊆ (((U : Subgroup G) : Set G))) :
    ∃ s : Finset ι, (⋂ i ∈ s, (((H i : Subgroup G) : Set G))) ⊆ (((U : Subgroup G) : Set G))

If the intersection of a family of closed subgroups lies inside an open subgroup, then already a finite subfamily has the same property. We formulate the family as plain subgroups together with explicit closedness hypotheses in order to keep the later formulation flexible.

Show proof

Theorem ProCGroups.finite_openSubgroup_intersections_form_nhds_basis GitHub

theorem finite_openSubgroup_intersections_form_nhds_basis [CompactSpace G]
    [IsTopologicalGroup G] [TotallyDisconnectedSpace G] {ι : Type v} (U : ι → OpenSubgroup G)
    (hInter : (⋂ i, (((U i : Subgroup G) : Set G))) = ({1} : Set G)) :
    ∀ W : Set G, IsOpen W → (1 : G) ∈ W →
      ∃ s : Finset ι, (⋂ i ∈ s, (((U i : Subgroup G) : Set G))) ⊆ W

If a family of open subgroups of a profinite group has trivial total intersection, then finite intersections of members of the family form a neighborhood basis of 1.

Show proof

ProCGroups.ProC.OpenNormalSubgroups.FilteredFamilies

Declarations