Products of abstract completions

A product of uniform inducing maps is uniform inducing (IsUniformInducing.piMap), so the product of a family of abstract completions is an abstract completion of the product (AbstractCompletion.pi). This is the indexed analogue of Mathlib's AbstractCompletion.prod.

Combined with AbstractCompletion.compareEquiv, it identifies the separated completion of a product with the product of the separated completions (UniformSpace.Completion.piEquiv), which is how completions of free modules ι → A are compared with ι → Completion A.

theorem IsUniformInducing.piMap {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} [(i : ι) → UniformSpace (α i)] [(i : ι) → UniformSpace (β i)] {f : (i : ι) → α i → β i} (hf : ∀ (i : ι), IsUniformInducing (f i)) : IsUniformInducing (Pi.map f)

A product of uniform inducing maps is uniform inducing.

def AbstractCompletion.pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → UniformSpace (α i)] (pkg : (i : ι) → AbstractCompletion.{u_3, u_2} (α i)) : AbstractCompletion.{max u_1 u_3, max u_1 u_2} ((i : ι) → α i)

Products of completions. The product of abstract completions of the factors is an abstract completion of the product, with the product of the completion maps. The body is exposed so that the completion space is definitionally the product ∀ i, (pkg i).space.

noncomputable def UniformSpace.Completion.piEquiv {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → UniformSpace (α i)] : Completion ((i : ι) → α i) ≃ᵤ ((i : ι) → Completion (α i))

The separated completion of a product is the product of the separated completions.

@[simp]

theorem UniformSpace.Completion.piEquiv_coe {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → UniformSpace (α i)] (x : (i : ι) → α i) : (piEquiv α) ↑x = fun (i : ι) => ↑(x i)

The comparison piEquiv sends the image of x to the family of images of its coordinates.