Documentation

Mathlib.Topology.Algebra.Nonarchimedean.Basic

Nonarchimedean Topology #

In this file we set up the theory of nonarchimedean topological groups and rings.

A nonarchimedean group is a topological group whose topology admits a basis of open neighborhoods of the identity element in the group consisting of open subgroups. A nonarchimedean ring is a topological ring whose underlying topological (additive) group is nonarchimedean.

Definitions #

A topological additive group is nonarchimedean if every neighborhood of 0 contains an open subgroup.

Instances
    theorem NonarchimedeanAddGroup.is_nonarchimedean {G : Type u_1} :
    ∀ {inst : AddGroup G} {inst_1 : TopologicalSpace G} [self : NonarchimedeanAddGroup G], Unhds 0, ∃ (V : OpenAddSubgroup G), V U

    A topological group is nonarchimedean if every neighborhood of 1 contains an open subgroup.

    Instances
      theorem NonarchimedeanGroup.is_nonarchimedean {G : Type u_1} :
      ∀ {inst : Group G} {inst_1 : TopologicalSpace G} [self : NonarchimedeanGroup G], Unhds 1, ∃ (V : OpenSubgroup G), V U

      A topological ring is nonarchimedean if its underlying topological additive group is nonarchimedean.

      Instances
        theorem NonarchimedeanRing.is_nonarchimedean {R : Type u_1} :
        ∀ {inst : Ring R} {inst_1 : TopologicalSpace R} [self : NonarchimedeanRing R], Unhds 0, ∃ (V : OpenAddSubgroup R), V U
        @[instance 100]

        Every nonarchimedean ring is naturally a nonarchimedean additive group.

        Equations
        • =

        If a topological group embeds into a nonarchimedean group, then it is nonarchimedean.

        theorem NonarchimedeanAddGroup.prod_subset {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3} [AddGroup K] [TopologicalSpace K] [NonarchimedeanAddGroup K] {U : Set (G × K)} (hU : U nhds 0) :
        ∃ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K), V ×ˢ W U

        An open neighborhood of the identity in the cartesian product of two nonarchimedean groups contains the cartesian product of an open neighborhood in each group.

        theorem NonarchimedeanGroup.prod_subset {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {K : Type u_3} [Group K] [TopologicalSpace K] [NonarchimedeanGroup K] {U : Set (G × K)} (hU : U nhds 1) :
        ∃ (V : OpenSubgroup G) (W : OpenSubgroup K), V ×ˢ W U

        An open neighborhood of the identity in the cartesian product of two nonarchimedean groups contains the cartesian product of an open neighborhood in each group.

        theorem NonarchimedeanAddGroup.prod_self_subset {G : Type u_1} [AddGroup G] [TopologicalSpace G] [NonarchimedeanAddGroup G] {U : Set (G × G)} (hU : U nhds 0) :
        ∃ (V : OpenAddSubgroup G), V ×ˢ V U

        An open neighborhood of the identity in the cartesian square of a nonarchimedean group contains the cartesian square of an open neighborhood in the group.

        theorem NonarchimedeanGroup.prod_self_subset {G : Type u_1} [Group G] [TopologicalSpace G] [NonarchimedeanGroup G] {U : Set (G × G)} (hU : U nhds 1) :
        ∃ (V : OpenSubgroup G), V ×ˢ V U

        An open neighborhood of the identity in the cartesian square of a nonarchimedean group contains the cartesian square of an open neighborhood in the group.

        The cartesian product of two nonarchimedean groups is nonarchimedean.

        Equations
        • =

        The cartesian product of two nonarchimedean groups is nonarchimedean.

        Equations
        • =

        The cartesian product of two nonarchimedean rings is nonarchimedean.

        Equations
        • =
        theorem NonarchimedeanRing.left_mul_subset {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) (r : R) :
        ∃ (V : OpenAddSubgroup R), r V U

        Given an open subgroup U and an element r of a nonarchimedean ring, there is an open subgroup V such that r • V is contained in U.

        theorem NonarchimedeanRing.mul_subset {R : Type u_1} [Ring R] [TopologicalSpace R] [NonarchimedeanRing R] (U : OpenAddSubgroup R) :
        ∃ (V : OpenAddSubgroup R), V * V U

        An open subgroup of a nonarchimedean ring contains the square of another one.