Documentation

Mathlib.Topology.Algebra.FilterBasis

Group and ring filter bases #

A GroupFilterBasis is a FilterBasis on a group with some properties relating the basis to the group structure. The main theorem is that a GroupFilterBasis on a group gives a topology on the group which makes it into a topological group with neighborhoods of the neutral element generated by the given basis.

Main definitions and results #

Given a group G and a ring R:

References #

class GroupFilterBasis (G : Type u) [Group G] extends FilterBasis G :

A GroupFilterBasis on a group is a FilterBasis satisfying some additional axioms. Example : if G is a topological group then the neighbourhoods of the identity are a GroupFilterBasis. Conversely given a GroupFilterBasis one can define a topology compatible with the group structure on G.

  • sets : Set (Set G)
  • nonempty : GroupFilterBasis.toFilterBasis.sets.Nonempty
  • inter_sets : ∀ {x y : Set G}, x GroupFilterBasis.toFilterBasis.setsy GroupFilterBasis.toFilterBasis.setszGroupFilterBasis.toFilterBasis.sets, z x y
  • one' : ∀ {U : Set G}, U GroupFilterBasis.toFilterBasis.sets1 U
  • mul' : ∀ {U : Set G}, U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V * V U
  • inv' : ∀ {U : Set G}, U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V (fun (x : G) => x⁻¹) ⁻¹' U
  • conj' : ∀ (x₀ : G) {U : Set G}, U GroupFilterBasis.toFilterBasis.setsVGroupFilterBasis.toFilterBasis.sets, V (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U
Instances
    class AddGroupFilterBasis (A : Type u) [AddGroup A] extends FilterBasis A :

    An AddGroupFilterBasis on an additive group is a FilterBasis satisfying some additional axioms. Example : if G is a topological group then the neighbourhoods of the identity are an AddGroupFilterBasis. Conversely given an AddGroupFilterBasis one can define a topology compatible with the group structure on G.

    • sets : Set (Set A)
    • nonempty : AddGroupFilterBasis.toFilterBasis.sets.Nonempty
    • inter_sets : ∀ {x y : Set A}, x AddGroupFilterBasis.toFilterBasis.setsy AddGroupFilterBasis.toFilterBasis.setszAddGroupFilterBasis.toFilterBasis.sets, z x y
    • zero' : ∀ {U : Set A}, U AddGroupFilterBasis.toFilterBasis.sets0 U
    • add' : ∀ {U : Set A}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V + V U
    • neg' : ∀ {U : Set A}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : A) => -x) ⁻¹' U
    • conj' : ∀ (x₀ : A) {U : Set A}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : A) => x₀ + x + -x₀) ⁻¹' U
    Instances
      def groupFilterBasisOfComm {G : Type u_1} [CommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x setsy setszsets, z x y) (one : Usets, 1 U) (mul : Usets, Vsets, V * V U) (inv : Usets, Vsets, V (fun (x : G) => x⁻¹) ⁻¹' U) :

      GroupFilterBasis constructor in the commutative group case.

      Equations
      • groupFilterBasisOfComm sets nonempty inter_sets one mul inv = { sets := sets, nonempty := nonempty, inter_sets := , one' := , mul' := , inv' := , conj' := }
      Instances For
        def addGroupFilterBasisOfComm {G : Type u_1} [AddCommGroup G] (sets : Set (Set G)) (nonempty : sets.Nonempty) (inter_sets : ∀ (x y : Set G), x setsy setszsets, z x y) (one : Usets, 0 U) (mul : Usets, Vsets, V + V U) (inv : Usets, Vsets, V (fun (x : G) => -x) ⁻¹' U) :

        AddGroupFilterBasis constructor in the additive commutative group case.

        Equations
        • addGroupFilterBasisOfComm sets nonempty inter_sets one mul inv = { sets := sets, nonempty := nonempty, inter_sets := , zero' := , add' := , neg' := , conj' := }
        Instances For
          Equations
          • GroupFilterBasis.instMembershipSet = { mem := fun (f : GroupFilterBasis G) (s : Set G) => s GroupFilterBasis.toFilterBasis.sets }
          Equations
          • AddGroupFilterBasis.instMembershipSet = { mem := fun (f : AddGroupFilterBasis G) (s : Set G) => s AddGroupFilterBasis.toFilterBasis.sets }
          theorem GroupFilterBasis.one {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} :
          U B1 U
          theorem AddGroupFilterBasis.zero {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} {U : Set G} :
          U B0 U
          theorem GroupFilterBasis.mul {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} :
          U BVB, V * V U
          theorem AddGroupFilterBasis.add {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} {U : Set G} :
          U BVB, V + V U
          theorem GroupFilterBasis.inv {G : Type u} [Group G] {B : GroupFilterBasis G} {U : Set G} :
          U BVB, V (fun (x : G) => x⁻¹) ⁻¹' U
          theorem AddGroupFilterBasis.neg {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} {U : Set G} :
          U BVB, V (fun (x : G) => -x) ⁻¹' U
          theorem GroupFilterBasis.conj {G : Type u} [Group G] {B : GroupFilterBasis G} (x₀ : G) {U : Set G} :
          U BVB, V (fun (x : G) => x₀ * x * x₀⁻¹) ⁻¹' U
          theorem AddGroupFilterBasis.conj {G : Type u} [AddGroup G] {B : AddGroupFilterBasis G} (x₀ : G) {U : Set G} :
          U BVB, V (fun (x : G) => x₀ + x + -x₀) ⁻¹' U

          The trivial group filter basis consists of {1} only. The associated topology is discrete.

          Equations
          • GroupFilterBasis.instInhabited = { default := { sets := {{1}}, nonempty := , inter_sets := , one' := , mul' := , inv' := , conj' := } }

          The trivial additive group filter basis consists of {0} only. The associated topology is discrete.

          Equations
          • AddGroupFilterBasis.instInhabited = { default := { sets := {{0}}, nonempty := , inter_sets := , zero' := , add' := , neg' := , conj' := } }
          theorem GroupFilterBasis.subset_mul_self {G : Type u} [Group G] (B : GroupFilterBasis G) {U : Set G} (h : U B) :
          U U * U
          theorem AddGroupFilterBasis.subset_add_self {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) {U : Set G} (h : U B) :
          U U + U
          def GroupFilterBasis.N {G : Type u} [Group G] (B : GroupFilterBasis G) :
          GFilter G

          The neighborhood function of a GroupFilterBasis.

          Equations
          • B.N x = Filter.map (fun (y : G) => x * y) GroupFilterBasis.toFilterBasis.filter
          Instances For

            The neighborhood function of an AddGroupFilterBasis.

            Equations
            • B.N x = Filter.map (fun (y : G) => x + y) AddGroupFilterBasis.toFilterBasis.filter
            Instances For
              @[simp]
              theorem GroupFilterBasis.N_one {G : Type u} [Group G] (B : GroupFilterBasis G) :
              B.N 1 = GroupFilterBasis.toFilterBasis.filter
              @[simp]
              theorem AddGroupFilterBasis.N_zero {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) :
              B.N 0 = AddGroupFilterBasis.toFilterBasis.filter
              theorem GroupFilterBasis.hasBasis {G : Type u} [Group G] (B : GroupFilterBasis G) (x : G) :
              (B.N x).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x * y) '' V
              theorem AddGroupFilterBasis.hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) (x : G) :
              (B.N x).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x + y) '' V

              The topological space structure coming from a group filter basis.

              Equations
              Instances For

                The topological space structure coming from an additive group filter basis.

                Equations
                Instances For
                  theorem GroupFilterBasis.nhds_eq {G : Type u} [Group G] (B : GroupFilterBasis G) {x₀ : G} :
                  nhds x₀ = B.N x₀
                  theorem AddGroupFilterBasis.nhds_eq {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) {x₀ : G} :
                  nhds x₀ = B.N x₀
                  theorem GroupFilterBasis.nhds_one_eq {G : Type u} [Group G] (B : GroupFilterBasis G) :
                  nhds 1 = GroupFilterBasis.toFilterBasis.filter
                  theorem AddGroupFilterBasis.nhds_zero_eq {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) :
                  nhds 0 = AddGroupFilterBasis.toFilterBasis.filter
                  theorem GroupFilterBasis.nhds_hasBasis {G : Type u} [Group G] (B : GroupFilterBasis G) (x₀ : G) :
                  (nhds x₀).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x₀ * y) '' V
                  theorem AddGroupFilterBasis.nhds_hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) (x₀ : G) :
                  (nhds x₀).HasBasis (fun (V : Set G) => V B) fun (V : Set G) => (fun (y : G) => x₀ + y) '' V
                  theorem GroupFilterBasis.nhds_one_hasBasis {G : Type u} [Group G] (B : GroupFilterBasis G) :
                  (nhds 1).HasBasis (fun (V : Set G) => V B) id
                  theorem AddGroupFilterBasis.nhds_zero_hasBasis {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) :
                  (nhds 0).HasBasis (fun (V : Set G) => V B) id
                  theorem GroupFilterBasis.mem_nhds_one {G : Type u} [Group G] (B : GroupFilterBasis G) {U : Set G} (hU : U B) :
                  U nhds 1
                  theorem AddGroupFilterBasis.mem_nhds_zero {G : Type u} [AddGroup G] (B : AddGroupFilterBasis G) {U : Set G} (hU : U B) :
                  U nhds 0

                  If a group is endowed with a topological structure coming from a group filter basis then it's a topological group.

                  If a group is endowed with a topological structure coming from a group filter basis then it's a topological group.

                  class RingFilterBasis (R : Type u) [Ring R] extends AddGroupFilterBasis R :

                  A RingFilterBasis on a ring is a FilterBasis satisfying some additional axioms. Example : if R is a topological ring then the neighbourhoods of the identity are a RingFilterBasis. Conversely given a RingFilterBasis on a ring R, one can define a topology on R which is compatible with the ring structure.

                  • sets : Set (Set R)
                  • nonempty : AddGroupFilterBasis.toFilterBasis.sets.Nonempty
                  • inter_sets : ∀ {x y : Set R}, x AddGroupFilterBasis.toFilterBasis.setsy AddGroupFilterBasis.toFilterBasis.setszAddGroupFilterBasis.toFilterBasis.sets, z x y
                  • zero' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.sets0 U
                  • add' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V + V U
                  • neg' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => -x) ⁻¹' U
                  • conj' : ∀ (x₀ : R) {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x₀ + x + -x₀) ⁻¹' U
                  • mul' : ∀ {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V * V U
                  • mul_left' : ∀ (x₀ : R) {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x₀ * x) ⁻¹' U
                  • mul_right' : ∀ (x₀ : R) {U : Set R}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : R) => x * x₀) ⁻¹' U
                  Instances
                    Equations
                    • RingFilterBasis.instMembershipSet = { mem := fun (B : RingFilterBasis R) (s : Set R) => s AddGroupFilterBasis.toFilterBasis.sets }
                    theorem RingFilterBasis.mul {R : Type u} [Ring R] (B : RingFilterBasis R) {U : Set R} (hU : U B) :
                    VB, V * V U
                    theorem RingFilterBasis.mul_left {R : Type u} [Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R} (hU : U B) :
                    VB, V (fun (x : R) => x₀ * x) ⁻¹' U
                    theorem RingFilterBasis.mul_right {R : Type u} [Ring R] (B : RingFilterBasis R) (x₀ : R) {U : Set R} (hU : U B) :
                    VB, V (fun (x : R) => x * x₀) ⁻¹' U

                    The topology associated to a ring filter basis. It has the given basis as a basis of neighborhoods of zero.

                    Equations
                    • B.topology = RingFilterBasis.toAddGroupFilterBasis.topology
                    Instances For

                      If a ring is endowed with a topological structure coming from a ring filter basis then it's a topological ring.

                      structure ModuleFilterBasis (R : Type u_1) (M : Type u_2) [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] extends AddGroupFilterBasis M :
                      Type u_2

                      A ModuleFilterBasis on a module is a FilterBasis satisfying some additional axioms. Example : if M is a topological module then the neighbourhoods of zero are a ModuleFilterBasis. Conversely given a ModuleFilterBasis one can define a topology compatible with the module structure on M.

                      • sets : Set (Set M)
                      • nonempty : AddGroupFilterBasis.toFilterBasis.sets.Nonempty
                      • inter_sets : ∀ {x y : Set M}, x AddGroupFilterBasis.toFilterBasis.setsy AddGroupFilterBasis.toFilterBasis.setszAddGroupFilterBasis.toFilterBasis.sets, z x y
                      • zero' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.sets0 U
                      • add' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V + V U
                      • neg' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => -x) ⁻¹' U
                      • conj' : ∀ (x₀ : M) {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => x₀ + x + -x₀) ⁻¹' U
                      • smul' : ∀ {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVnhds 0, WAddGroupFilterBasis.toFilterBasis.sets, V W U
                      • smul_left' : ∀ (x₀ : R) {U : Set M}, U AddGroupFilterBasis.toFilterBasis.setsVAddGroupFilterBasis.toFilterBasis.sets, V (fun (x : M) => x₀ x) ⁻¹' U
                      • smul_right' : ∀ (m₀ : M) {U : Set M}, U AddGroupFilterBasis.toFilterBasis.sets∀ᶠ (x : R) in nhds 0, x m₀ U
                      Instances For
                        Equations
                        • ModuleFilterBasis.GroupFilterBasis.hasMem = { mem := fun (B : ModuleFilterBasis R M) (s : Set M) => s AddGroupFilterBasis.toFilterBasis.sets }
                        theorem ModuleFilterBasis.smul {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) {U : Set M} (hU : U B) :
                        Vnhds 0, WB, V W U
                        theorem ModuleFilterBasis.smul_left {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) (x₀ : R) {U : Set M} (hU : U B) :
                        VB, V (fun (x : M) => x₀ x) ⁻¹' U
                        theorem ModuleFilterBasis.smul_right {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] (B : ModuleFilterBasis R M) (m₀ : M) {U : Set M} (hU : U B) :
                        ∀ᶠ (x : R) in nhds 0, x m₀ U

                        If R is discrete then the trivial additive group filter basis on any R-module is a module filter basis.

                        Equations
                        • One or more equations did not get rendered due to their size.

                        The topology associated to a module filter basis on a module over a topological ring. It has the given basis as a basis of neighborhoods of zero.

                        Equations
                        • B.topology = B.topology
                        Instances For

                          The topology associated to a module filter basis on a module over a topological ring. It has the given basis as a basis of neighborhoods of zero. This version gets the ring topology by unification instead of type class inference.

                          Equations
                          • B.topology' = B.topology
                          Instances For
                            theorem ContinuousSMul.of_basis_zero {R : Type u_1} {M : Type u_2} [CommRing R] [TopologicalSpace R] [AddCommGroup M] [Module R M] {ι : Type u_3} [TopologicalRing R] [TopologicalSpace M] [TopologicalAddGroup M] {p : ιProp} {b : ιSet M} (h : (nhds 0).HasBasis p b) (hsmul : ∀ {i : ι}, p iVnhds 0, ∃ (j : ι), p j V b j b i) (hsmul_left : ∀ (x₀ : R) {i : ι}, p i∃ (j : ι), p j Set.MapsTo (fun (x : M) => x₀ x) (b j) (b i)) (hsmul_right : ∀ (m₀ : M) {i : ι}, p i∀ᶠ (x : R) in nhds 0, x m₀ b i) :

                            A topological add group with a basis of 𝓝 0 satisfying the axioms of ModuleFilterBasis is a topological module.

                            This lemma is mathematically useless because one could obtain such a result by applying ModuleFilterBasis.continuousSMul and use the fact that group topologies are characterized by their neighborhoods of 0 to obtain the ContinuousSMul on the pre-existing topology.

                            But it turns out it's just easier to get it as a byproduct of the proof, so this is just a free quality-of-life improvement.

                            If a module is endowed with a topological structure coming from a module filter basis then it's a topological module.

                            def ModuleFilterBasis.ofBases {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) (BM : AddGroupFilterBasis M) (smul : ∀ {U : Set M}, U BMVBR, WBM, V W U) (smul_left : ∀ (x₀ : R) {U : Set M}, U BMVBM, V (fun (x : M) => x₀ x) ⁻¹' U) (smul_right : ∀ (m₀ : M) {U : Set M}, U BMVBR, V (fun (x : R) => x m₀) ⁻¹' U) :

                            Build a module filter basis from compatible ring and additive group filter bases.

                            Equations
                            • ModuleFilterBasis.ofBases BR BM smul smul_left smul_right = { toAddGroupFilterBasis := BM, smul' := , smul_left' := smul_left, smul_right' := }
                            Instances For