Mathlib.Topology.Algebra.UniformRing

Module docstring

{"# 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 IsUniformAddGroup. 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.

UniformSpace.Completion.extensionHom: extends a continuous ring morphism from R to a complete separated group S to Completion R.
UniformSpace.Completion.mapRingHom : promotes a continuous ring morphism from R to S into a continuous ring morphism from Completion R to Completion S.

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

UniformSpace.Completion.one instance

: One (Completion α)

Full source

instance one : One (Completion α) :=
  ⟨(1 : α)⟩

Multiplicative Identity in the Completion of a Topological Ring

Informal description

The completion of a topological ring $\alpha$ has a canonical multiplicative identity element.

UniformSpace.Completion.mul instance

: Mul (Completion α)

Full source

instance mul : Mul (Completion α) :=
  ⟨curry <| (isDenseInducing_coe.prodMap isDenseInducing_coe).extend ((↑) ∘ uncurry (· * ·))⟩

Multiplication on the Completion of a Topological Ring

Informal description

The completion of a topological ring $\alpha$ has a multiplication operation extending the multiplication on $\alpha$.

UniformSpace.Completion.coe_one theorem

: ((1 : α) : Completion α) = 1

Full source

@[norm_cast]
theorem coe_one : ((1 : α) : Completion α) = 1 :=
  rfl

Preservation of Multiplicative Identity in Completion of Topological Ring

Informal description

The canonical map from a topological ring $\alpha$ to its completion preserves the multiplicative identity, i.e., the image of $1 \in \alpha$ under the completion map is equal to $1$ in the completion of $\alpha$.

UniformSpace.Completion.coe_mul theorem

(a b : α) : ((a * b : α) : Completion α) = a * b

Full source

@[norm_cast]
theorem coe_mul (a b : α) : ((a * b : α) : Completion α) = a * b :=
  ((isDenseInducing_coe.prodMap isDenseInducing_coe).extend_eq
      ((continuous_coe α).comp (@continuous_mul α _ _ _)) (a, b)).symm

Multiplication Preservation in Completion of Topological Ring

Informal description

For any elements $a$ and $b$ in a topological ring $\alpha$, the canonical inclusion map from $\alpha$ to its completion $\overline{\alpha}$ preserves multiplication, i.e., $(a * b) = a * b$ in $\overline{\alpha}$.

UniformSpace.Completion.instContinuousMul instance

: ContinuousMul (Completion α)

Full source

instance : ContinuousMul (Completion α) where
  continuous_mul := by
    let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
    have : Continuous fun p : α × α => m p.1 p.2 := (continuous_coe α).comp continuous_mul
    have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
    exact (di.extend_Z_bilin di this :)

Continuous Multiplication on the Completion of a Topological Ring

Informal description

The completion of a topological ring $\alpha$ has a continuous multiplication operation extending the multiplication on $\alpha$.

UniformSpace.Completion.continuous_mul theorem

: Continuous fun p : Completion α × Completion α => p.1 * p.2

Full source

@[deprecated _root_.continuous_mul (since := "2024-12-21")]
protected theorem continuous_mul : Continuous fun p : CompletionCompletion α × Completion α => p.1 * p.2 :=
  _root_.continuous_mul

Continuity of Multiplication in Completion of Topological Ring

Informal description

The multiplication operation on the completion $\overline{\alpha}$ of a topological ring $\alpha$ is continuous, i.e., the map $(x, y) \mapsto x * y$ is continuous from $\overline{\alpha} \times \overline{\alpha}$ to $\overline{\alpha}$.

UniformSpace.Completion.Continuous.mul theorem

 {β : Type*} [TopologicalSpace β] {f g : β → Completion α} (hf : Continuous f) (hg : Continuous g) :
  Continuous fun b => f b * g b

Full source

@[deprecated _root_.Continuous.mul (since := "2024-12-21")]
protected theorem Continuous.mul {β : Type*} [TopologicalSpace β] {f g : β → Completion α}
    (hf : Continuous f) (hg : Continuous g) : Continuous fun b => f b * g b :=
  hf.mul hg

Continuity of Pointwise Multiplication in Completion of Topological Ring

Informal description

Let $\beta$ be a topological space and $f, g \colon \beta \to \overline{\alpha}$ be continuous functions, where $\overline{\alpha}$ is the completion of a topological ring $\alpha$. Then the function $b \mapsto f(b) * g(b)$ is continuous.

UniformSpace.Completion.ring instance

: Ring (Completion α)

Full source

instance ring : Ring (Completion α) :=
  { AddMonoidWithOne.unary, (inferInstanceAs (AddCommGroup (Completion α))),
      (inferInstanceAs (Mul (Completion α))), (inferInstanceAs (One (Completion α))) with
    zero_mul := fun a =>
      Completion.induction_on a
        (isClosed_eq (continuous_const.mul continuous_id) continuous_const)
        fun a => by rw [← coe_zero, ← coe_mul, zero_mul]
    mul_zero := fun a =>
      Completion.induction_on a
        (isClosed_eq (continuous_id.mul continuous_const) continuous_const)
        fun a => by rw [← coe_zero, ← coe_mul, mul_zero]
    one_mul := fun a =>
      Completion.induction_on a
        (isClosed_eq (continuous_const.mul continuous_id) continuous_id) fun a => by
        rw [← coe_one, ← coe_mul, one_mul]
    mul_one := fun a =>
      Completion.induction_on a
        (isClosed_eq (continuous_id.mul continuous_const) continuous_id) fun a => by
        rw [← coe_one, ← coe_mul, mul_one]
    mul_assoc := fun a b c =>
      Completion.induction_on₃ a b c
        (isClosed_eq
          ((continuous_fst.mul (continuous_fst.comp continuous_snd)).mul
            (continuous_snd.comp continuous_snd))
          (continuous_fst.mul
            ((continuous_fst.comp continuous_snd).mul
              (continuous_snd.comp continuous_snd))))
                fun a b c => by rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
    left_distrib := fun a b c =>
      Completion.induction_on₃ a b c
        (isClosed_eq
          (continuous_fst.mul
            (Continuous.add (continuous_fst.comp continuous_snd)
              (continuous_snd.comp continuous_snd)))
          (Continuous.add (continuous_fst.mul (continuous_fst.comp continuous_snd))
            (continuous_fst.mul (continuous_snd.comp continuous_snd))))
        fun a b c => by rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
    right_distrib := fun a b c =>
      Completion.induction_on₃ a b c
        (isClosed_eq
          ((Continuous.add continuous_fst (continuous_fst.comp continuous_snd)).mul
            (continuous_snd.comp continuous_snd))
          (Continuous.add (continuous_fst.mul (continuous_snd.comp continuous_snd))
            ((continuous_fst.comp continuous_snd).mul
              (continuous_snd.comp continuous_snd))))
        fun a b c => by rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul] }

Ring Structure on the Completion of a Topological Ring

Informal description

The completion of a topological ring $\alpha$ forms a ring, where the ring operations are defined by extending the operations from $\alpha$ to its completion.

UniformSpace.Completion.coeRingHom definition

: α →+* Completion α

Full source

/-- The map from a uniform ring to its completion, as a ring homomorphism. -/
def coeRingHom : α →+* Completion α where
  toFun := (↑)
  map_one' := coe_one α
  map_zero' := coe_zero
  map_add' := coe_add
  map_mul' := coe_mul

Canonical inclusion homomorphism into completion

Informal description

The canonical ring homomorphism from a topological ring $\alpha$ to its completion $\overline{\alpha}$, which maps each element $x \in \alpha$ to its equivalence class in $\overline{\alpha}$. This homomorphism preserves the ring operations: it maps $1$ to $1$, $0$ to $0$, addition to addition, and multiplication to multiplication.

UniformSpace.Completion.continuous_coeRingHom theorem

: Continuous (coeRingHom : α → Completion α)

Full source

theorem continuous_coeRingHom : Continuous (coeRingHom : α → Completion α) :=
  continuous_coe α

Continuity of the Canonical Inclusion into Completion

Informal description

The canonical ring homomorphism from a topological ring $\alpha$ to its completion $\overline{\alpha}$ is continuous.

UniformSpace.Completion.extensionHom definition

[CompleteSpace β] [T0Space β] : Completion α →+* β

Full source

/-- The completion extension as a ring morphism. -/
def extensionHom [CompleteSpace β] [T0Space β] : CompletionCompletion α →+* β :=
  have hf' : Continuous (f : α →+ β) := hf
  -- helping the elaborator
  have hf : UniformContinuous f := uniformContinuous_addMonoidHom_of_continuous hf'
  { toFun := Completion.extension f
    map_zero' := by simp_rw [← coe_zero, extension_coe hf, f.map_zero]
    map_add' := fun a b =>
      Completion.induction_on₂ a b
        (isClosed_eq (continuous_extension.comp continuous_add)
          ((continuous_extension.comp continuous_fst).add
            (continuous_extension.comp continuous_snd)))
        fun a b => by
        simp_rw [← coe_add, extension_coe hf, f.map_add]
    map_one' := by rw [← coe_one, extension_coe hf, f.map_one]
    map_mul' := fun a b =>
      Completion.induction_on₂ a b
        (isClosed_eq (continuous_extension.comp continuous_mul)
          ((continuous_extension.comp continuous_fst).mul
            (continuous_extension.comp continuous_snd)))
        fun a b => by
        simp_rw [← coe_mul, extension_coe hf, f.map_mul] }

Extension of a continuous ring homomorphism to the completion

Informal description

Given a continuous ring homomorphism $ f \colon \alpha \to \beta $ where $ \beta $ is a complete and separated topological ring, the function `UniformSpace.Completion.extensionHom` extends $ f $ to a ring homomorphism from the completion of $ \alpha $ to $ \beta $. This extension preserves the ring operations: addition, multiplication, zero, and one.

UniformSpace.Completion.extensionHom_coe theorem

[CompleteSpace β] [T0Space β] (a : α) : Completion.extensionHom f hf a = f a

Full source

theorem extensionHom_coe [CompleteSpace β] [T0Space β] (a : α) :
    Completion.extensionHom f hf a = f a := by
  simp only [Completion.extensionHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    UniformSpace.Completion.extension_coe <| uniformContinuous_addMonoidHom_of_continuous hf]

Extension Homomorphism Preserves Evaluation on Original Ring Elements

Informal description

Let $\alpha$ be a topological ring and $\beta$ be a complete and separated topological ring. Given a continuous ring homomorphism $f \colon \alpha \to \beta$ and an element $a \in \alpha$, the extension of $f$ to the completion of $\alpha$ evaluated at the canonical image of $a$ equals $f(a)$. In other words, $\overline{f}(a) = f(a)$, where $\overline{f} \colon \overline{\alpha} \to \beta$ is the extension of $f$ to the completion $\overline{\alpha}$ of $\alpha$.

UniformSpace.Completion.topologicalRing instance

: IsTopologicalRing (Completion α)

Full source

instance topologicalRing : IsTopologicalRing (Completion α) where
  continuous_add := continuous_add
  continuous_mul := continuous_mul

Completion of a Topological Ring is a Topological Ring

Informal description

The completion of a topological ring $\alpha$ is itself a topological ring, where the ring operations are continuous with respect to the topology induced by the completion.

UniformSpace.Completion.mapRingHom definition

(hf : Continuous f) : Completion α →+* Completion β

Full source

/-- The completion map as a ring morphism. -/
def mapRingHom (hf : Continuous f) : CompletionCompletion α →+* Completion β :=
  extensionHom (coeRingHom.comp f) (continuous_coeRingHom.comp hf)

Induced ring homomorphism on completions

Informal description

Given a continuous ring homomorphism $ f \colon \alpha \to \beta $ between topological rings, the function `UniformSpace.Completion.mapRingHom` promotes $ f $ to a continuous ring homomorphism from the completion of $ \alpha $ to the completion of $ \beta $. This is constructed by extending the composition of $ f $ with the canonical inclusion homomorphism of $ \beta $ into its completion.

UniformSpace.Completion.map_smul_eq_mul_coe theorem

(r : R) : Completion.map (r • ·) = ((algebraMap R A r : Completion A) * ·)

Full source

@[simp]
theorem map_smul_eq_mul_coe (r : R) :
    Completion.map (r • ·) = ((algebraMap R A r : Completion A) * ·) := by
  ext x
  refine Completion.induction_on x ?_ fun a => ?_
  · exact isClosed_eq Completion.continuous_map (continuous_mul_left _)
  · simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]

Scalar Multiplication as Multiplication by Algebra Map in Completion

Informal description

For any element $r$ in a commutative semiring $R$, the map induced by scalar multiplication by $r$ on the completion of a topological $R$-algebra $A$ is equal to the multiplication by the image of $r$ under the algebra map from $R$ to the completion of $A$. In symbols: $$\text{Completion.map}(r \cdot \cdot) = \left(\text{algebraMap}_R(A)(r)\right) \cdot \cdot$$

UniformSpace.Completion.algebra instance

: Algebra R (Completion A)

Full source

instance algebra : Algebra R (Completion A) where
  algebraMap := (UniformSpace.Completion.coeRingHom : A →+* Completion A).comp (algebraMap R A)
  commutes' := fun r x =>
    Completion.induction_on x (isClosed_eq (continuous_mul_left _) (continuous_mul_right _))
      fun a => by
      simpa only [coe_mul] using congr_arg ((↑) : A → Completion A) (Algebra.commutes r a)
  smul_def' := fun r x => congr_fun (map_smul_eq_mul_coe A R r) x

Algebra Structure on the Completion of a Topological Algebra

Informal description

For a topological ring $A$ that is an algebra over a commutative semiring $R$, the completion of $A$ inherits an algebra structure over $R$.

UniformSpace.Completion.algebraMap_def theorem

(r : R) : algebraMap R (Completion A) r = (algebraMap R A r : Completion A)

Full source

theorem algebraMap_def (r : R) :
    algebraMap R (Completion A) r = (algebraMap R A r : Completion A) :=
  rfl

Characterization of Algebra Map on Completion: $\text{algebraMap}_R(\text{Completion}(A))(r) = \text{algebraMap}_R(A)(r)$

Informal description

For any element $r$ in a commutative semiring $R$, the algebra map from $R$ to the completion of a topological $R$-algebra $A$ evaluated at $r$ is equal to the image of the algebra map from $R$ to $A$ evaluated at $r$, considered as an element in the completion of $A$. In symbols: $$\text{algebraMap}_R(\text{Completion}(A))(r) = \left(\text{algebraMap}_R(A)(r)\right) \in \text{Completion}(A)$$

UniformSpace.Completion.commRing instance

: CommRing (Completion R)

Full source

instance commRing : CommRing (Completion R) :=
  { Completion.ring with
    mul_comm := fun a b =>
      Completion.induction_on₂ a b
        (isClosed_eq (continuous_fst.mul continuous_snd) (continuous_snd.mul continuous_fst))
        fun a b => by rw [← coe_mul, ← coe_mul, mul_comm] }

Commutative Ring Structure on the Completion of a Topological Ring

Informal description

The completion of a commutative topological ring $R$ forms a commutative ring.

UniformSpace.Completion.algebra' instance

: Algebra R (Completion R)

Full source

/-- A shortcut instance for the common case -/
instance algebra' : Algebra R (Completion R) := by infer_instance

Algebra Structure on the Completion of a Topological Algebra over Itself

Informal description

For a commutative semiring $R$ and a topological ring $R$ that is an algebra over $R$, the completion of $R$ inherits an algebra structure over $R$.

UniformSpace.inseparableSetoid_ring theorem

 (α) [Ring α] [TopologicalSpace α] [IsTopologicalRing α] : inseparableSetoid α = Submodule.quotientRel (Ideal.closure ⊥)

Full source

theorem inseparableSetoid_ring (α) [Ring α] [TopologicalSpace α] [IsTopologicalRing α] :
    inseparableSetoid α = Submodule.quotientRel (Ideal.closure ⊥) :=
  Setoid.ext fun x y =>
    addGroup_inseparable_iff.trans <| .trans (by rfl) (Submodule.quotientRel_def _).symm

Inseparable Equivalence Relation as Quotient by Zero Ideal Closure in Topological Rings

Informal description

For a topological ring $\alpha$ with a uniform structure making subtraction uniformly continuous, the inseparable equivalence relation on $\alpha$ coincides with the quotient relation induced by the closure of the zero ideal in $\alpha$.

UniformSpace.sepQuotHomeomorphRingQuot definition

 (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : SeparationQuotient α ≃ₜ α ⧸ (⊥ : Ideal α).closure

Full source

/-- 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. -/
def sepQuotHomeomorphRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
    SeparationQuotientSeparationQuotient α ≃ₜ α ⧸ (⊥ : Ideal α).closure where
  toEquiv := Quotient.congrRight fun x y => by rw [inseparableSetoid_ring]
  continuous_toFun := continuous_id.quotient_map' <| by
    rw [inseparableSetoid_ring]; exact fun _ _ ↦ id
  continuous_invFun := continuous_id.quotient_map' <| by
    rw [inseparableSetoid_ring]; exact fun _ _ ↦ id

Homeomorphism between separated quotient and quotient by zero closure

Informal description

For a commutative topological ring $\alpha$ with a uniform structure making subtraction uniformly continuous, there is a homeomorphism between the separated quotient of $\alpha$ and the quotient ring $\alpha / \overline{\{0\}}$, where $\overline{\{0\}}$ denotes the closure of the zero ideal.

UniformSpace.commRing instance

[CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : CommRing (SeparationQuotient α)

Full source

instance commRing [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
    CommRing (SeparationQuotient α) :=
  (sepQuotHomeomorphRingQuot _).commRing

Commutative Ring Structure on the Separated Quotient of a Topological Ring

Informal description

For any commutative topological ring $\alpha$ with a uniform structure making subtraction uniformly continuous, the separated quotient of $\alpha$ inherits a commutative ring structure.

UniformSpace.sepQuotRingEquivRingQuot definition

 (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : SeparationQuotient α ≃+* α ⧸ (⊥ : Ideal α).closure

Full source

/-- 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. -/
def sepQuotRingEquivRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
    SeparationQuotientSeparationQuotient α ≃+* α ⧸ (⊥ : Ideal α).closure :=
  (sepQuotHomeomorphRingQuot _).ringEquiv

Ring isomorphism between separated quotient and quotient by zero closure

Informal description

For a commutative topological ring $\alpha$ with a uniform structure making subtraction uniformly continuous, there is a ring isomorphism between the separated quotient of $\alpha$ and the quotient ring $\alpha / \overline{\{0\}}$, where $\overline{\{0\}}$ denotes the closure of the zero ideal. This isomorphism preserves both the ring structure and the topological structure.

UniformSpace.topologicalRing instance

[CommRing α] [TopologicalSpace α] [IsTopologicalRing α] : IsTopologicalRing (SeparationQuotient α)

Full source

instance topologicalRing [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
    IsTopologicalRing (SeparationQuotient α) where
  toContinuousAdd :=
    (sepQuotHomeomorphRingQuot α).isInducing.continuousAdd (sepQuotRingEquivRingQuot α)
  toContinuousMul :=
    (sepQuotHomeomorphRingQuot α).isInducing.continuousMul (sepQuotRingEquivRingQuot α)
  toContinuousNeg :=
    (sepQuotHomeomorphRingQuot α).isInducing.continuousNeg <|
      map_neg (sepQuotRingEquivRingQuot α)

Topological Ring Structure on the Separated Quotient of a Commutative Topological Ring

Informal description

For any commutative topological ring $\alpha$ where the ring operations are continuous with respect to the topology, the separated quotient of $\alpha$ inherits a topological ring structure.

IsDenseInducing.extendRingHom definition

 {i : α →+* β} {f : α →+* γ} (ue : IsUniformInducing i) (dr : DenseRange i) (hf : UniformContinuous f) : β →+* γ

Full source

/-- The dense inducing extension as a ring homomorphism. -/
noncomputable def IsDenseInducing.extendRingHom {i : α →+* β} {f : α →+* γ}
    (ue : IsUniformInducing i) (dr : DenseRange i) (hf : UniformContinuous f) : β →+* γ where
  toFun := (ue.isDenseInducing dr).extend f
  map_one' := by
    convert IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 1
    exacts [i.map_one.symm, f.map_one.symm]
  map_zero' := by
    convert IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0 <;>
    simp only [map_zero]
  map_add' := by
    have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
    refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
    · exact isClosed_eq (Continuous.comp h continuous_add)
        ((h.comp continuous_fst).add (h.comp continuous_snd))
    · simp_rw [← i.map_add, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_add]
  map_mul' := by
    have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
    refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
    · exact isClosed_eq (Continuous.comp h continuous_mul)
        ((h.comp continuous_fst).mul (h.comp continuous_snd))
    · simp_rw [← i.map_mul, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_mul]

Extension of a uniformly continuous ring homomorphism with dense range

Informal description

Given ring homomorphisms $ i \colon \alpha \to \beta $ and $ f \colon \alpha \to \gamma $, where $ i $ is a uniform inducing map with dense range and $ f $ is uniformly continuous, the function extends $ f $ to a ring homomorphism from $ \beta $ to $ \gamma $. This extension preserves the ring structure, including addition, multiplication, zero, and one.