Documentation

Mathlib.Topology.Algebra.OpenSubgroup

Open subgroups of a topological groups #

This files builds the lattice OpenSubgroup G of open subgroups in a topological group G, and its additive version OpenAddSubgroup. This lattice has a top element, the subgroup of all elements, but no bottom element in general. The trivial subgroup which is the natural candidate bottom has no reason to be open (this happens only in discrete groups).

Note that this notion is especially relevant in a non-archimedean context, for instance for p-adic groups.

Main declarations #

TODO #

structure OpenAddSubgroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] extends AddSubgroup G :
Type u_1

The type of open subgroups of a topological additive group.

Instances For
    structure OpenSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] extends Subgroup G :
    Type u_1

    The type of open subgroups of a topological group.

    Instances For
      Equations
      • OpenSubgroup.hasCoeSubgroup = { coe := OpenSubgroup.toSubgroup }
      Equations
      • OpenAddSubgroup.hasCoeAddSubgroup = { coe := OpenAddSubgroup.toAddSubgroup }
      theorem OpenSubgroup.toSubgroup_injective {G : Type u_1} [Group G] [TopologicalSpace G] :
      Function.Injective OpenSubgroup.toSubgroup
      theorem OpenAddSubgroup.toAddSubgroup_injective {G : Type u_1} [AddGroup G] [TopologicalSpace G] :
      Function.Injective OpenAddSubgroup.toAddSubgroup
      Equations
      • OpenSubgroup.instSetLike = { coe := fun (U : OpenSubgroup G) => U, coe_injective' := }
      Equations
      • OpenAddSubgroup.instSetLike = { coe := fun (U : OpenAddSubgroup G) => U, coe_injective' := }

      Coercion from OpenSubgroup G to Opens G.

      Equations
      • U = { carrier := U, is_open' := }
      Instances For

        Coercion from OpenAddSubgroup G to Opens G.

        Equations
        • U = { carrier := U, is_open' := }
        Instances For
          Equations
          • OpenSubgroup.hasCoeOpens = { coe := OpenSubgroup.toOpens }
          Equations
          • OpenAddSubgroup.hasCoeOpens = { coe := OpenAddSubgroup.toOpens }
          @[simp]
          theorem OpenSubgroup.coe_toOpens {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} :
          U = U
          @[simp]
          theorem OpenAddSubgroup.coe_toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} :
          U = U
          @[simp]
          theorem OpenSubgroup.coe_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} :
          U = U
          @[simp]
          theorem OpenAddSubgroup.coe_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} :
          U = U
          @[simp]
          theorem OpenSubgroup.mem_toOpens {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {g : G} :
          g U g U
          @[simp]
          theorem OpenAddSubgroup.mem_toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {g : G} :
          g U g U
          @[simp]
          theorem OpenSubgroup.mem_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {g : G} :
          g U g U
          @[simp]
          theorem OpenAddSubgroup.mem_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {g : G} :
          g U g U
          theorem OpenAddSubgroup.ext {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenAddSubgroup G} (h : ∀ (x : G), x U x V) :
          U = V
          theorem OpenSubgroup.ext {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenSubgroup G} (h : ∀ (x : G), x U x V) :
          U = V
          Equations
          • OpenSubgroup.instTop = { top := { toSubgroup := , isOpen' := } }
          Equations
          • OpenAddSubgroup.instTop = { top := { toAddSubgroup := , isOpen' := } }
          @[simp]
          theorem OpenSubgroup.mem_top {G : Type u_1} [Group G] [TopologicalSpace G] (x : G) :
          @[simp]
          theorem OpenAddSubgroup.mem_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] (x : G) :
          @[simp]
          theorem OpenSubgroup.coe_top {G : Type u_1} [Group G] [TopologicalSpace G] :
          = Set.univ
          @[simp]
          theorem OpenAddSubgroup.coe_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] :
          = Set.univ
          @[simp]
          @[simp]
          Equations
          • OpenSubgroup.instInhabited = { default := }
          Equations
          • OpenAddSubgroup.instInhabited = { default := }
          def OpenSubgroup.prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) :

          The product of two open subgroups as an open subgroup of the product group.

          Equations
          • U.prod V = { toSubgroup := (↑U).prod V, isOpen' := }
          Instances For

            The product of two open subgroups as an open subgroup of the product group.

            Equations
            • U.sum V = { toAddSubgroup := (↑U).prod V, isOpen' := }
            Instances For
              @[simp]
              theorem OpenSubgroup.coe_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) :
              (U.prod V) = U ×ˢ V
              @[simp]
              theorem OpenAddSubgroup.coe_sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) :
              (U.sum V) = U ×ˢ V
              @[simp]
              theorem OpenSubgroup.toSubgroup_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) :
              (U.prod V) = (↑U).prod V
              @[simp]
              theorem OpenAddSubgroup.toAddSubgroup_sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) :
              (U.sum V) = (↑U).prod V
              Equations
              • OpenSubgroup.instInfOpenSubgroup = { min := fun (U V : OpenSubgroup G) => { toSubgroup := U V, isOpen' := } }
              Equations
              • OpenAddSubgroup.instInfOpenAddSubgroup = { min := fun (U V : OpenAddSubgroup G) => { toAddSubgroup := U V, isOpen' := } }
              @[simp]
              theorem OpenSubgroup.coe_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenSubgroup G} :
              (U V) = U V
              @[simp]
              theorem OpenAddSubgroup.coe_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenAddSubgroup G} :
              (U V) = U V
              @[simp]
              theorem OpenSubgroup.toSubgroup_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenSubgroup G} :
              (U V) = U V
              @[simp]
              theorem OpenAddSubgroup.toAddSubgroup_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenAddSubgroup G} :
              (U V) = U V
              @[simp]
              theorem OpenSubgroup.toOpens_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenSubgroup G} :
              (U V) = U V
              @[simp]
              theorem OpenAddSubgroup.toOpens_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenAddSubgroup G} :
              (U V) = U V
              @[simp]
              theorem OpenSubgroup.mem_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenSubgroup G} {x : G} :
              x U V x U x V
              @[simp]
              theorem OpenAddSubgroup.mem_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenAddSubgroup G} {x : G} :
              x U V x U x V
              Equations
              • OpenSubgroup.instPartialOrderOpenSubgroup = inferInstance
              Equations
              • OpenAddSubgroup.instPartialOrderOpenAddSubgroup = inferInstance
              Equations
              • OpenSubgroup.instSemilatticeInfOpenSubgroup = SemilatticeInf.mk SemilatticeInf.inf
              Equations
              • OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup = SemilatticeInf.mk SemilatticeInf.inf
              Equations
              Equations
              @[simp]
              theorem OpenSubgroup.toSubgroup_le {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenSubgroup G} :
              U V U V
              @[simp]
              theorem OpenAddSubgroup.toAddSubgroup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenAddSubgroup G} :
              U V U V
              def OpenSubgroup.comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (f : G →* N) (hf : Continuous f) (H : OpenSubgroup N) :

              The preimage of an OpenSubgroup along a continuous Monoid homomorphism is an OpenSubgroup.

              Equations
              Instances For
                def OpenAddSubgroup.comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (f : G →+ N) (hf : Continuous f) (H : OpenAddSubgroup N) :

                The preimage of an OpenAddSubgroup along a continuous AddMonoid homomorphism is an OpenAddSubgroup.

                Equations
                Instances For
                  @[simp]
                  theorem OpenSubgroup.coe_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous f) :
                  (OpenSubgroup.comap f hf H) = f ⁻¹' H
                  @[simp]
                  theorem OpenAddSubgroup.coe_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous f) :
                  (OpenAddSubgroup.comap f hf H) = f ⁻¹' H
                  @[simp]
                  theorem OpenSubgroup.toSubgroup_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous f) :
                  @[simp]
                  theorem OpenAddSubgroup.toAddSubgroup_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous f) :
                  @[simp]
                  theorem OpenSubgroup.mem_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] {H : OpenSubgroup N} {f : G →* N} {hf : Continuous f} {x : G} :
                  x OpenSubgroup.comap f hf H f x H
                  @[simp]
                  theorem OpenAddSubgroup.mem_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] {H : OpenAddSubgroup N} {f : G →+ N} {hf : Continuous f} {x : G} :
                  theorem OpenSubgroup.comap_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] {P : Type u_3} [Group P] [TopologicalSpace P] (K : OpenSubgroup P) (f₂ : N →* P) (hf₂ : Continuous f₂) (f₁ : G →* N) (hf₁ : Continuous f₁) :
                  OpenSubgroup.comap f₁ hf₁ (OpenSubgroup.comap f₂ hf₂ K) = OpenSubgroup.comap (f₂.comp f₁) K
                  theorem OpenAddSubgroup.comap_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] {P : Type u_3} [AddGroup P] [TopologicalSpace P] (K : OpenAddSubgroup P) (f₂ : N →+ P) (hf₂ : Continuous f₂) (f₁ : G →+ N) (hf₁ : Continuous f₁) :
                  OpenAddSubgroup.comap f₁ hf₁ (OpenAddSubgroup.comap f₂ hf₂ K) = OpenAddSubgroup.comap (f₂.comp f₁) K
                  theorem Subgroup.isOpen_of_mem_nhds {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) {g : G} (hg : H nhds g) :
                  IsOpen H
                  theorem AddSubgroup.isOpen_of_mem_nhds {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) {g : G} (hg : H nhds g) :
                  IsOpen H
                  theorem Subgroup.isOpen_mono {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {H₁ H₂ : Subgroup G} (h : H₁ H₂) (h₁ : IsOpen H₁) :
                  IsOpen H₂
                  theorem AddSubgroup.isOpen_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] {H₁ H₂ : AddSubgroup G} (h : H₁ H₂) (h₁ : IsOpen H₁) :
                  IsOpen H₂
                  theorem Subgroup.isOpen_of_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) {U : OpenSubgroup G} (h : U H) :
                  IsOpen H
                  theorem Subgroup.isOpen_of_one_mem_interior {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) (h_1_int : 1 interior H) :
                  IsOpen H

                  If a subgroup of a topological group has 1 in its interior, then it is open.

                  If a subgroup of an additive topological group has 0 in its interior, then it is open.

                  theorem Subgroup.isClosed_of_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (h : IsOpen U) :
                  theorem Subgroup.subgroupOf_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] (U K : Subgroup G) (h : IsOpen K) :
                  IsOpen (K.subgroupOf U)
                  theorem AddSubgroup.addSubgroupOf_isOpen {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U K : AddSubgroup G) (h : IsOpen K) :
                  IsOpen (K.addSubgroupOf U)
                  theorem Subgroup.quotient_finite_of_isOpen' {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] (U : Subgroup G) (K : Subgroup U) (hUopen : IsOpen U) (hKopen : IsOpen K) :
                  Finite (U K)
                  theorem AddSubgroup.quotient_finite_of_isOpen' {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] (U : AddSubgroup G) (K : AddSubgroup U) (hUopen : IsOpen U) (hKopen : IsOpen K) :
                  Finite (U K)
                  Equations
                  • OpenSubgroup.instMax = { max := fun (U V : OpenSubgroup G) => { toSubgroup := U V, isOpen' := } }
                  Equations
                  • OpenAddSubgroup.instMax = { max := fun (U V : OpenAddSubgroup G) => { toAddSubgroup := U V, isOpen' := } }
                  @[simp]
                  theorem OpenSubgroup.toSubgroup_sup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U V : OpenSubgroup G) :
                  (U V) = U V
                  @[simp]
                  theorem OpenAddSubgroup.toAddSubgroup_sup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U V : OpenAddSubgroup G) :
                  (U V) = U V
                  Equations
                  • OpenSubgroup.instLattice = Lattice.mk SemilatticeInf.inf
                  Equations
                  • OpenAddSubgroup.instLattice = Lattice.mk SemilatticeInf.inf
                  theorem Submodule.isOpen_mono {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] [Module R M] {U P : Submodule R M} (h : U P) (hU : IsOpen U) :
                  IsOpen P
                  theorem Ideal.isOpen_of_isOpen_subideal {R : Type u_1} [CommRing R] [TopologicalSpace R] [TopologicalRing R] {U I : Ideal R} (h : U I) (hU : IsOpen U) :
                  IsOpen I

                  Open normal subgroups of a topological group #

                  This section builds the lattice OpenNormalSubgroup G of open subgroups in a topological group G, and its additive version OpenNormalAddSubgroup.

                  structure OpenNormalSubgroup (G : Type u) [Group G] [TopologicalSpace G] extends OpenSubgroup G :

                  The type of open normal subgroups of a topological group.

                  • mul_mem' : ∀ {a b : G}, a (↑self.toOpenSubgroup).carrierb (↑self.toOpenSubgroup).carriera * b (↑self.toOpenSubgroup).carrier
                  • one_mem' : 1 (↑self.toOpenSubgroup).carrier
                  • inv_mem' : ∀ {x : G}, x (↑self.toOpenSubgroup).carrierx⁻¹ (↑self.toOpenSubgroup).carrier
                  • isOpen' : IsOpen (↑self.toOpenSubgroup).carrier
                  • isNormal' : (↑self.toOpenSubgroup).Normal
                  Instances For
                    theorem OpenNormalSubgroup.ext {G : Type u} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {x y : OpenNormalSubgroup G} (carrier : (↑x.toOpenSubgroup).carrier = (↑y.toOpenSubgroup).carrier) :
                    x = y

                    The type of open normal subgroups of a topological additive group.

                    • add_mem' : ∀ {a b : G}, a (↑self.toOpenAddSubgroup).carrierb (↑self.toOpenAddSubgroup).carriera + b (↑self.toOpenAddSubgroup).carrier
                    • zero_mem' : 0 (↑self.toOpenAddSubgroup).carrier
                    • neg_mem' : ∀ {x : G}, x (↑self.toOpenAddSubgroup).carrier-x (↑self.toOpenAddSubgroup).carrier
                    • isOpen' : IsOpen (↑self.toOpenAddSubgroup).carrier
                    • isNormal' : (↑self.toOpenAddSubgroup).Normal
                    Instances For
                      theorem OpenNormalAddSubgroup.ext {G : Type u} {inst✝ : AddGroup G} {inst✝¹ : TopologicalSpace G} {x y : OpenNormalAddSubgroup G} (carrier : (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier) :
                      x = y
                      instance OpenNormalSubgroup.instNormal {G : Type u} [Group G] [TopologicalSpace G] (H : OpenNormalSubgroup G) :
                      (↑H.toOpenSubgroup).Normal
                      instance OpenNormalAddSubgroup.instNormal {G : Type u} [AddGroup G] [TopologicalSpace G] (H : OpenNormalAddSubgroup G) :
                      (↑H.toOpenAddSubgroup).Normal
                      Equations
                      • OpenNormalSubgroup.instSetLike = { coe := fun (U : OpenNormalSubgroup G) => U.toOpenSubgroup, coe_injective' := }
                      Equations
                      • OpenNormalAddSubgroup.instSetLike = { coe := fun (U : OpenNormalAddSubgroup G) => U.toOpenAddSubgroup, coe_injective' := }
                      Equations
                      • OpenNormalSubgroup.instCoeSubgroup = { coe := fun (H : OpenNormalSubgroup G) => H.toOpenSubgroup }
                      Equations
                      • OpenNormalAddSubgroup.instCoeAddSubgroup = { coe := fun (H : OpenNormalAddSubgroup G) => H.toOpenAddSubgroup }
                      Equations
                      • OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup = inferInstance
                      Equations
                      • OpenNormalAddSubgroup.instPartialOrderOpenNormalAddSubgroup = inferInstance
                      Equations
                      • OpenNormalSubgroup.instInfOpenNormalSubgroup = { min := fun (U V : OpenNormalSubgroup G) => { toOpenSubgroup := U.toOpenSubgroup V.toOpenSubgroup, isNormal' := } }
                      Equations
                      • OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup = { min := fun (U V : OpenNormalAddSubgroup G) => { toOpenAddSubgroup := U.toOpenAddSubgroup V.toOpenAddSubgroup, isNormal' := } }
                      Equations
                      Equations
                      Equations
                      • OpenNormalSubgroup.instMaxOfContinuousMul = { max := fun (U V : OpenNormalSubgroup G) => { toOpenSubgroup := U.toOpenSubgroup V.toOpenSubgroup, isNormal' := } }
                      Equations
                      • OpenNormalAddSubgroup.instMaxOfContinuousAdd = { max := fun (U V : OpenNormalAddSubgroup G) => { toOpenAddSubgroup := U.toOpenAddSubgroup V.toOpenAddSubgroup, isNormal' := } }
                      Equations
                      Equations
                      Equations
                      • OpenNormalSubgroup.instLatticeOfContinuousMul = Lattice.mk SemilatticeInf.inf
                      Equations
                      • OpenNormalAddSubgroup.instLatticeOfContinuousAdd = Lattice.mk SemilatticeInf.inf

                      Existence of an open subgroup in any clopen neighborhood of the neutral element #

                      This section proves the lemma TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one, which states that in a compact topological group, for any clopen neighborhood of 1, there exists an open subgroup contained within it.

                      For a set W, T is a neighborhood of 0 which is open, stable under negation and satisfies T + W ⊆ W.

                      Instances For
                        structure TopologicalGroup.mulInvClosureNhd {G : Type u_1} [TopologicalSpace G] (T W : Set G) [Group G] :

                        For a set W, T is a neighborhood of 1 which is open, statble under inverse and satisfies T * W ⊆ W.

                        Instances For
                          theorem TopologicalGroup.exist_mul_closure_nhd {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) :
                          Tnhds 1, W * T W
                          theorem TopologicalAddGroup.exist_add_closure_nhd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) :
                          Tnhds 0, W + T W
                          theorem TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one {G : Type u_2} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 W) :
                          ∃ (H : OpenSubgroup G), H W