Documentation

Mathlib.Topology.Algebra.UniformRing

Completion of topological rings: #

This files endows the completion of a topological ring with a ring structure. More precisely the instance UniformSpace.Completion.ring builds a ring structure on the completion of a ring endowed with a compatible uniform structure in the sense of UniformAddGroup. There is also a commutative version when the original ring is commutative. Moreover, if a topological ring is an algebra over a commutative semiring, then so is its UniformSpace.Completion.

The last part of the file builds a ring structure on the biggest separated quotient of a ring.

Main declarations: #

Beyond the instances explained above (that don't have to be explicitly invoked), the main constructions deal with continuous ring morphisms.

TODO: Generalise the results here from the concrete Completion to any AbstractCompletion.

Equations
Equations
theorem UniformSpace.Completion.coe_one (α : Type u_1) [Ring α] [UniformSpace α] :
α 1 = 1
theorem UniformSpace.Completion.coe_mul {α : Type u_1} [Ring α] [UniformSpace α] [TopologicalRing α] (a : α) (b : α) :
α (a * b) = α a * α b
theorem UniformSpace.Completion.Continuous.mul {α : Type u_1} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] {β : Type u_2} [TopologicalSpace β] {f : βUniformSpace.Completion α} {g : βUniformSpace.Completion α} (hf : Continuous f) (hg : Continuous g) :
Continuous fun (b : β) => f b * g b
Equations
  • UniformSpace.Completion.ring = Ring.mk SubNegMonoid.zsmul

The map from a uniform ring to its completion, as a ring homomorphism.

Equations
  • UniformSpace.Completion.coeRingHom = { toFun := α, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
    theorem UniformSpace.Completion.continuous_coeRingHom {α : Type u_1} [Ring α] [UniformSpace α] [TopologicalRing α] [UniformAddGroup α] :
    Continuous UniformSpace.Completion.coeRingHom

    The completion extension as a ring morphism.

    Equations
    Instances For

      The completion map as a ring morphism.

      Equations
      Instances For
        @[simp]
        Equations

        A shortcut instance for the common case

        Equations
        @[deprecated UniformSpace.inseparableSetoid_ring]

        Alias of UniformSpace.inseparableSetoid_ring.

        @[deprecated UniformSpace.inseparableSetoid_ring]

        Given a topological ring α equipped with a uniform structure that makes subtraction uniformly continuous, get an homeomorphism between the separated quotient of α and the quotient ring corresponding to the closure of zero.

        Equations
        Instances For
          Equations

          Given a topological ring α equipped with a uniform structure that makes subtraction uniformly continuous, get an equivalence between the separated quotient of α and the quotient ring corresponding to the closure of zero.

          Equations
          Instances For
            noncomputable def IsDenseInducing.extendRingHom {α : Type u_1} [UniformSpace α] [Semiring α] {β : Type u_2} [UniformSpace β] [Semiring β] [TopologicalSemiring β] {γ : Type u_3} [UniformSpace γ] [Semiring γ] [TopologicalSemiring γ] [T2Space γ] [CompleteSpace γ] {i : α →+* β} {f : α →+* γ} (ue : IsUniformInducing i) (dr : DenseRange i) (hf : UniformContinuous f) :
            β →+* γ

            The dense inducing extension as a ring homomorphism.

            Equations
            Instances For