Documentation

Mathlib.Topology.Algebra.Nonarchimedean.Bases

Neighborhood bases for non-archimedean rings and modules #

This files contains special families of filter bases on rings and modules that give rise to non-archimedean topologies.

The main definition is RingSubgroupsBasis which is a predicate on a family of additive subgroups of a ring. The predicate ensures there is a topology RingSubgroupsBasis.topology which is compatible with a ring structure and admits the given family as a basis of neighborhoods of zero. In particular the given subgroups become open subgroups (bundled in RingSubgroupsBasis.openAddSubgroup) and we get a non-archimedean topological ring (RingSubgroupsBasis.nonarchimedean).

A special case of this construction is given by SubmodulesBasis where the subgroups are sub-modules in a commutative algebra. This important example gives rise to the adic topology (studied in its own file).

structure RingSubgroupsBasis {A : Type u_1} {ι : Type u_2} [Ring A] (B : ιAddSubgroup A) :

A family of additive subgroups on a ring A is a subgroups basis if it satisfies some axioms ensuring there is a topology on A which is compatible with the ring structure and admits this family as a basis of neighborhoods of zero.

  • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j

    Condition for B to be a filter basis on A.

  • mul : ∀ (i : ι), ∃ (j : ι), (B j) * (B j) (B i)

    For each set B in the submodule basis on A, there is another basis element B' such that the set-theoretic product B' * B' is in B.

  • leftMul : ∀ (x : A) (i : ι), ∃ (j : ι), (B j) (fun (x_1 : A) => x * x_1) ⁻¹' (B i)

    For any element x : A and any set B in the submodule basis on A, there is another basis element B' such that B' * x is in B.

  • rightMul : ∀ (x : A) (i : ι), ∃ (j : ι), (B j) (fun (x_1 : A) => x_1 * x) ⁻¹' (B i)

    For any element x : A and any set B in the submodule basis on A, there is another basis element B' such that x * B' is in B.

Instances For
    theorem RingSubgroupsBasis.inter {A : Type u_1} {ι : Type u_2} [Ring A] {B : ιAddSubgroup A} (self : RingSubgroupsBasis B) (i : ι) (j : ι) :
    ∃ (k : ι), B k B i B j

    Condition for B to be a filter basis on A.

    theorem RingSubgroupsBasis.mul {A : Type u_1} {ι : Type u_2} [Ring A] {B : ιAddSubgroup A} (self : RingSubgroupsBasis B) (i : ι) :
    ∃ (j : ι), (B j) * (B j) (B i)

    For each set B in the submodule basis on A, there is another basis element B' such that the set-theoretic product B' * B' is in B.

    theorem RingSubgroupsBasis.leftMul {A : Type u_1} {ι : Type u_2} [Ring A] {B : ιAddSubgroup A} (self : RingSubgroupsBasis B) (x : A) (i : ι) :
    ∃ (j : ι), (B j) (fun (x_1 : A) => x * x_1) ⁻¹' (B i)

    For any element x : A and any set B in the submodule basis on A, there is another basis element B' such that B' * x is in B.

    theorem RingSubgroupsBasis.rightMul {A : Type u_1} {ι : Type u_2} [Ring A] {B : ιAddSubgroup A} (self : RingSubgroupsBasis B) (x : A) (i : ι) :
    ∃ (j : ι), (B j) (fun (x_1 : A) => x_1 * x) ⁻¹' (B i)

    For any element x : A and any set B in the submodule basis on A, there is another basis element B' such that x * B' is in B.

    theorem RingSubgroupsBasis.of_comm {A : Type u_3} {ι : Type u_4} [CommRing A] (B : ιAddSubgroup A) (inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j) (mul : ∀ (i : ι), ∃ (j : ι), (B j) * (B j) (B i)) (leftMul : ∀ (x : A) (i : ι), ∃ (j : ι), (B j) (fun (y : A) => x * y) ⁻¹' (B i)) :
    def RingSubgroupsBasis.toRingFilterBasis {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) :

    Every subgroups basis on a ring leads to a ring filter basis.

    Equations
    Instances For
      theorem RingSubgroupsBasis.mem_addGroupFilterBasis_iff {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) {V : Set A} :
      V RingFilterBasis.toAddGroupFilterBasis ∃ (i : ι), V = (B i)
      theorem RingSubgroupsBasis.mem_addGroupFilterBasis {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) (i : ι) :
      (B i) RingFilterBasis.toAddGroupFilterBasis
      def RingSubgroupsBasis.topology {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) :

      The topology defined from a subgroups basis, admitting the given subgroups as a basis of neighborhoods of zero.

      Equations
      • hB.topology = RingFilterBasis.toAddGroupFilterBasis.topology
      Instances For
        theorem RingSubgroupsBasis.hasBasis_nhds_zero {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) :
        (nhds 0).HasBasis (fun (x : ι) => True) fun (i : ι) => (B i)
        theorem RingSubgroupsBasis.hasBasis_nhds {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) (a : A) :
        (nhds a).HasBasis (fun (x : ι) => True) fun (i : ι) => {b : A | b - a B i}
        def RingSubgroupsBasis.openAddSubgroup {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) (i : ι) :

        Given a subgroups basis, the basis elements as open additive subgroups in the associated topology.

        Equations
        • hB.openAddSubgroup i = { toAddSubgroup := B i, isOpen' := }
        Instances For
          theorem RingSubgroupsBasis.nonarchimedean {A : Type u_1} {ι : Type u_2} [Ring A] [Nonempty ι] {B : ιAddSubgroup A} (hB : RingSubgroupsBasis B) :
          structure SubmodulesRingBasis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] (B : ιSubmodule R A) :

          A family of submodules in a commutative R-algebra A is a submodules basis if it satisfies some axioms ensuring there is a topology on A which is compatible with the ring structure and admits this family as a basis of neighborhoods of zero.

          • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j

            Condition for B to be a filter basis on A.

          • leftMul : ∀ (a : A) (i : ι), ∃ (j : ι), a B j B i

            For any element a : A and any set B in the submodule basis on A, there is another basis element B' such that a • B' is in B.

          • mul : ∀ (i : ι), ∃ (j : ι), (B j) * (B j) (B i)

            For each set B in the submodule basis on A, there is another basis element B' such that the set-theoretic product B' * B' is in B.

          Instances For
            theorem SubmodulesRingBasis.inter {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ιSubmodule R A} (self : SubmodulesRingBasis B) (i : ι) (j : ι) :
            ∃ (k : ι), B k B i B j

            Condition for B to be a filter basis on A.

            theorem SubmodulesRingBasis.leftMul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ιSubmodule R A} (self : SubmodulesRingBasis B) (a : A) (i : ι) :
            ∃ (j : ι), a B j B i

            For any element a : A and any set B in the submodule basis on A, there is another basis element B' such that a • B' is in B.

            theorem SubmodulesRingBasis.mul {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ιSubmodule R A} (self : SubmodulesRingBasis B) (i : ι) :
            ∃ (j : ι), (B j) * (B j) (B i)

            For each set B in the submodule basis on A, there is another basis element B' such that the set-theoretic product B' * B' is in B.

            theorem SubmodulesRingBasis.toRing_subgroups_basis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ιSubmodule R A} (hB : SubmodulesRingBasis B) :
            RingSubgroupsBasis fun (i : ι) => (B i).toAddSubgroup
            def SubmodulesRingBasis.topology {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {B : ιSubmodule R A} [Nonempty ι] (hB : SubmodulesRingBasis B) :

            The topology associated to a basis of submodules in an algebra.

            Equations
            • hB.topology = .topology
            Instances For
              structure SubmodulesBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] (B : ιSubmodule R M) :

              A family of submodules in an R-module M is a submodules basis if it satisfies some axioms ensuring there is a topology on M which is compatible with the module structure and admits this family as a basis of neighborhoods of zero.

              • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j

                Condition for B to be a filter basis on M.

              • smul : ∀ (m : M) (i : ι), ∀ᶠ (a : R) in nhds 0, a m B i

                For any element m : M and any set B in the basis, a • m lies in B for all a sufficiently close to 0.

              Instances For
                theorem SubmodulesBasis.inter {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] {B : ιSubmodule R M} (self : SubmodulesBasis B) (i : ι) (j : ι) :
                ∃ (k : ι), B k B i B j

                Condition for B to be a filter basis on M.

                theorem SubmodulesBasis.smul {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] {B : ιSubmodule R M} (self : SubmodulesBasis B) (m : M) (i : ι) :
                ∀ᶠ (a : R) in nhds 0, a m B i

                For any element m : M and any set B in the basis, a • m lies in B for all a sufficiently close to 0.

                def SubmodulesBasis.toModuleFilterBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ιSubmodule R M} (hB : SubmodulesBasis B) :

                The image of a submodules basis is a module filter basis.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def SubmodulesBasis.topology {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ιSubmodule R M} (hB : SubmodulesBasis B) :

                  The topology associated to a basis of submodules in a module.

                  Equations
                  • hB.topology = hB.toModuleFilterBasis.topology
                  Instances For
                    def SubmodulesBasis.openAddSubgroup {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ιSubmodule R M} (hB : SubmodulesBasis B) (i : ι) :

                    Given a submodules basis, the basis elements as open additive subgroups in the associated topology.

                    Equations
                    • hB.openAddSubgroup i = { toAddSubgroup := (B i).toAddSubgroup, isOpen' := }
                    Instances For
                      theorem SubmodulesBasis.nonarchimedean {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [TopologicalSpace R] [Nonempty ι] {B : ιSubmodule R M} (hB : SubmodulesBasis B) :
                      theorem SubmodulesRingBasis.toSubmodulesBasis {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [TopologicalSpace R] {B : ιSubmodule R A} (hB : SubmodulesRingBasis B) (hsmul : ∀ (m : A) (i : ι), ∀ᶠ (a : R) in nhds 0, a m B i) :
                      structure RingFilterBasis.SubmodulesBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) (B : ιSubmodule R M) :

                      Given a ring filter basis on a commutative ring R, define a compatibility condition on a family of submodules of an R-module M. This compatibility condition allows to get a topological module structure.

                      • inter : ∀ (i j : ι), ∃ (k : ι), B k B i B j

                        Condition for B to be a filter basis on M.

                      • smul : ∀ (m : M) (i : ι), UBR, U (fun (x : R) => x m) ⁻¹' (B i)

                        For any element m : M and any set B i in the submodule basis on M, there is a U in the ring filter basis on R such that U * m is in B i.

                      Instances For
                        theorem RingFilterBasis.SubmodulesBasis.inter {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] {BR : RingFilterBasis R} {B : ιSubmodule R M} (self : BR.SubmodulesBasis B) (i : ι) (j : ι) :
                        ∃ (k : ι), B k B i B j

                        Condition for B to be a filter basis on M.

                        theorem RingFilterBasis.SubmodulesBasis.smul {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] {BR : RingFilterBasis R} {B : ιSubmodule R M} (self : BR.SubmodulesBasis B) (m : M) (i : ι) :
                        UBR, U (fun (x : R) => x m) ⁻¹' (B i)

                        For any element m : M and any set B i in the submodule basis on M, there is a U in the ring filter basis on R such that U * m is in B i.

                        theorem RingFilterBasis.submodulesBasisIsBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] (BR : RingFilterBasis R) {B : ιSubmodule R M} (hB : BR.SubmodulesBasis B) :
                        def RingFilterBasis.moduleFilterBasis {ι : Type u_1} {R : Type u_2} [CommRing R] {M : Type u_4} [AddCommGroup M] [Module R M] [Nonempty ι] (BR : RingFilterBasis R) {B : ιSubmodule R M} (hB : BR.SubmodulesBasis B) :

                        The module filter basis associated to a ring filter basis and a compatible submodule basis. This allows to build a topological module structure compatible with the given module structure and the topology associated to the given ring filter basis.

                        Equations
                        • BR.moduleFilterBasis hB = .toModuleFilterBasis
                        Instances For