Mathlib.Topology.Algebra.GroupCompletion

instZeroCompletion instance

[Zero α] : Zero (Completion α)

Full source

instance [Zero α] : Zero (Completion α) :=
  ⟨(0 : α)⟩

Zero Element in the Completion of a Space with Zero

Informal description

For any type $\alpha$ with a zero element, the completion $\overline{\alpha}$ of $\alpha$ inherits a zero element.

instNegCompletion instance

[Neg α] : Neg (Completion α)

Full source

instance [Neg α] : Neg (Completion α) :=
  ⟨Completion.map (fun a ↦ -a : α → α)⟩

Negation Operation on Completion Space

Informal description

For any type $\alpha$ equipped with a negation operation, the completion $\text{Completion}(\alpha)$ inherits a negation operation.

instAddCompletion instance

[Add α] : Add (Completion α)

Full source

instance [Add α] : Add (Completion α) :=
  ⟨Completion.map₂ (· + ·)⟩

Addition Operation on the Completion of a Space with Addition

Informal description

For any type $\alpha$ with an addition operation, the completion $\overline{\alpha}$ of $\alpha$ inherits an addition operation.

instSubCompletion instance

[Sub α] : Sub (Completion α)

Full source

instance [Sub α] : Sub (Completion α) :=
  ⟨Completion.map₂ Sub.sub⟩

Subtraction Operation on the Completion of a Uniform Space

Informal description

For any type $\alpha$ equipped with a subtraction operation, the completion of $\alpha$ as a uniform space inherits a subtraction operation.

UniformSpace.Completion.coe_zero theorem

[Zero α] : ((0 : α) : Completion α) = 0

Full source

@[norm_cast]
theorem UniformSpace.Completion.coe_zero [Zero α] : ((0 : α) : Completion α) = 0 :=
  rfl

Preservation of Zero in Completion

Informal description

For any type $\alpha$ with a zero element, the canonical inclusion map from $\alpha$ to its completion $\overline{\alpha}$ preserves the zero element, i.e., $(0 : \alpha) = 0$ in $\overline{\alpha}$.

UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul instance

 [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α] [UniformContinuousConstSMul M α] :
  MulActionWithZero M (Completion α)

Full source

instance [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α]
    [UniformContinuousConstSMul M α] : MulActionWithZero M (Completion α) :=
  { (inferInstance : MulAction M <| Completion α) with
    smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
    zero_smul :=
      ext' (continuous_const_smul _) continuous_const fun a ↦ by
        rw [← coe_smul, zero_smul, coe_zero] }

Multiplicative Action with Zero on the Completion of a Uniform Space

Informal description

For any uniform space $\alpha$ equipped with a zero element and a multiplicative action by a monoid with zero $M$ that is uniformly continuous, the completion of $\alpha$ inherits a multiplicative action with zero by $M$.

UniformSpace.Completion.coe_neg theorem

(a : α) : ((-a : α) : Completion α) = -a

Full source

@[norm_cast]
theorem coe_neg (a : α) : ((-a : α) : Completion α) = -a :=
  (map_coe uniformContinuous_neg a).symm

Negation Commutes with Completion Embedding

Informal description

For any element $a$ in a type $\alpha$ with a negation operation, the image of $-a$ under the canonical embedding into the completion $\text{Completion}(\alpha)$ is equal to the negation of the image of $a$ in the completion, i.e., $(-a : \text{Completion}(\alpha)) = - (a : \text{Completion}(\alpha))$.

UniformSpace.Completion.coe_sub theorem

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

Full source

@[norm_cast]
theorem coe_sub (a b : α) : ((a - b : α) : Completion α) = a - b :=
  (map₂_coe_coe a b Sub.sub uniformContinuous_sub).symm

Subtraction Commutes with Completion Embedding

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with a subtraction operation, the image of $a - b$ under the canonical embedding into the completion $\text{Completion}(\alpha)$ is equal to the subtraction of the images of $a$ and $b$ in the completion, i.e., $(a - b : \text{Completion}(\alpha)) = a - b$.

UniformSpace.Completion.coe_add theorem

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

Full source

@[norm_cast]
theorem coe_add (a b : α) : ((a + b : α) : Completion α) = a + b :=
  (map₂_coe_coe a b (· + ·) uniformContinuous_add).symm

Addition Commutes with Completion Embedding

Informal description

For any elements $a$ and $b$ in a type $\alpha$ with an addition operation, the image of $a + b$ under the canonical embedding into the completion $\overline{\alpha}$ is equal to the sum of the images of $a$ and $b$ in the completion, i.e., $(a + b : \overline{\alpha}) = (a : \overline{\alpha}) + (b : \overline{\alpha})$.

UniformSpace.Completion.instAddMonoid instance

: AddMonoid (Completion α)

Full source

instance : AddMonoid (Completion α) :=
  { (inferInstance : Zero <| Completion α),
    (inferInstance : Add <| Completion α) with
    zero_add := fun a ↦
      Completion.induction_on a
        (isClosed_eq (continuous_map₂ continuous_const continuous_id) continuous_id) fun a ↦
        show 0 + (a : Completion α) = a by rw [← coe_zero, ← coe_add, zero_add]
    add_zero := fun a ↦
      Completion.induction_on a
        (isClosed_eq (continuous_map₂ continuous_id continuous_const) continuous_id) fun a ↦
        show (a : Completion α) + 0 = a by rw [← coe_zero, ← coe_add, add_zero]
    add_assoc := fun a b c ↦
      Completion.induction_on₃ a b c
        (isClosed_eq
          (continuous_map₂ (continuous_map₂ continuous_fst (continuous_fst.comp continuous_snd))
            (continuous_snd.comp continuous_snd))
          (continuous_map₂ continuous_fst
            (continuous_map₂ (continuous_fst.comp continuous_snd)
              (continuous_snd.comp continuous_snd))))
        fun a b c ↦
        show (a : Completion α) + b + c = a + (b + c) by repeat' rw_mod_cast [add_assoc]
    nsmul := (· • ·)
    nsmul_zero := fun a ↦
      Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
        show 0 • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
    nsmul_succ := fun n a ↦
      Completion.induction_on a
        (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
        show (n + 1) • (a : Completion α) = n • (a : Completion α) + (a : Completion α) by
          rw [← coe_smul, succ_nsmul, coe_add, coe_smul] }

Additive Monoid Structure on the Completion of an Abelian Group

Informal description

The completion $\overline{\alpha}$ of an abelian group $\alpha$ with a compatible uniform structure inherits an additive monoid structure.

UniformSpace.Completion.instSubNegMonoid instance

: SubNegMonoid (Completion α)

Full source

instance : SubNegMonoid (Completion α) :=
  { (inferInstance : AddMonoid <| Completion α),
    (inferInstance : Neg <| Completion α),
    (inferInstance : Sub <| Completion α) with
    sub_eq_add_neg := fun a b ↦
      Completion.induction_on₂ a b
        (isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
          (continuous_map₂ continuous_fst (Completion.continuous_map.comp continuous_snd)))
        fun a b ↦ mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
    zsmul := (· • ·)
    zsmul_zero' := fun a ↦
      Completion.induction_on a (isClosed_eq continuous_map continuous_const) fun a ↦
        show (0 : ℤ) • (a : Completion α) = 0 by rw [← coe_smul, ← coe_zero, zero_smul]
    zsmul_succ' := fun n a ↦
      Completion.induction_on a
        (isClosed_eq continuous_map <| continuous_map₂ continuous_map continuous_id) fun a ↦
          show (n.succ : ℤ) • (a : Completion α) = _ by
            rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
    zsmul_neg' := fun n a ↦
      Completion.induction_on a
        (isClosed_eq continuous_map <| Completion.continuous_map.comp continuous_map) fun a ↦
          show (Int.negSucc n) • (a : Completion α) = _ by
            rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul] }

Sub-Neg-Monoid Structure on the Completion of an Abelian Group

Informal description

The completion $\overline{\alpha}$ of an abelian group $\alpha$ with a compatible uniform structure inherits a sub-neg-monoid structure, which includes operations for subtraction and negation.

UniformSpace.Completion.addGroup instance

: AddGroup (Completion α)

Full source

instance addGroup : AddGroup (Completion α) :=
  { (inferInstance : SubNegMonoid <| Completion α) with
    neg_add_cancel := fun a ↦
      Completion.induction_on a
        (isClosed_eq (continuous_map₂ Completion.continuous_map continuous_id) continuous_const)
        fun a ↦
        show -(a : Completion α) + a = 0 by
          rw_mod_cast [neg_add_cancel]
          rfl }

Abelian Group Structure on the Completion of an Abelian Group

Informal description

The completion $\overline{\alpha}$ of an abelian group $\alpha$ with a compatible uniform structure inherits an abelian group structure.

UniformSpace.Completion.isUniformAddGroup instance

: IsUniformAddGroup (Completion α)

Full source

instance isUniformAddGroup : IsUniformAddGroup (Completion α) :=
  ⟨uniformContinuous_map₂ Sub.sub⟩

Uniform Continuity of Group Operations on Completion

Informal description

The abelian group structure on the completion $\overline{\alpha}$ of an abelian group $\alpha$ is compatible with the uniform structure of the completion, meaning that the addition and negation operations are uniformly continuous.

UniformSpace.Completion.instDistribMulActionOfUniformContinuousConstSMul instance

{M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] : DistribMulAction M (Completion α)

Full source

instance {M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] :
    DistribMulAction M (Completion α) :=
  { (inferInstance : MulAction M <| Completion α) with
    smul_add := fun r x y ↦
      induction_on₂ x y
        (isClosed_eq ((continuous_fst.add continuous_snd).const_smul _)
          ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
        fun a b ↦ by simp only [← coe_add, ← coe_smul, smul_add]
    smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, smul_zero r] }

Distributive Multiplicative Action on the Completion of an Abelian Group

Informal description

For any monoid $M$ acting distributively on an abelian group $\alpha$ with uniformly continuous scalar multiplication, the completion $\overline{\alpha}$ inherits a distributive multiplicative action by $M$.

UniformSpace.Completion.toCompl definition

: α →+ Completion α

Full source

/-- The map from a group to its completion as a group hom. -/
@[simps]
def toCompl : α →+ Completion α where
  toFun := (↑)
  map_add' := coe_add
  map_zero' := coe_zero

Canonical embedding into the completion of a topological abelian group

Informal description

The canonical group homomorphism from a topological abelian group $\alpha$ to its completion $\overline{\alpha}$, which maps each element $a \in \alpha$ to its image in the completion. This homomorphism preserves addition and maps the zero element of $\alpha$ to the zero element of $\overline{\alpha}$.

UniformSpace.Completion.continuous_toCompl theorem

: Continuous (toCompl : α → Completion α)

Full source

theorem continuous_toCompl : Continuous (toCompl : α → Completion α) :=
  continuous_coe α

Continuity of the Completion Embedding

Informal description

The canonical embedding map $\overline{\cdot} : \alpha \to \overline{\alpha}$ from a topological abelian group $\alpha$ to its completion $\overline{\alpha}$ is continuous.

UniformSpace.Completion.isDenseInducing_toCompl theorem

: IsDenseInducing (toCompl : α → Completion α)

Full source

theorem isDenseInducing_toCompl : IsDenseInducing (toCompl : α → Completion α) :=
  isDenseInducing_coe

Dense Inducing Property of the Completion Embedding

Informal description

The canonical embedding $a \mapsto \overline{a}$ from a topological abelian group $\alpha$ to its completion $\overline{\alpha}$ is a dense inducing map. This means that the image of $\alpha$ under this embedding is dense in $\overline{\alpha}$, and the topology on $\overline{\alpha}$ is the coarsest topology making this embedding continuous.

UniformSpace.Completion.instAddCommGroup instance

: AddCommGroup (Completion α)

Full source

instance instAddCommGroup : AddCommGroup (Completion α) :=
  { (inferInstance : AddGroup <| Completion α) with
    add_comm := fun a b ↦
      Completion.induction_on₂ a b
        (isClosed_eq (continuous_map₂ continuous_fst continuous_snd)
          (continuous_map₂ continuous_snd continuous_fst))
        fun x y ↦ by
        change (x : Completion α) + ↑y = ↑y + ↑x
        rw [← coe_add, ← coe_add, add_comm] }

Completion of an Abelian Group is an Abelian Group

Informal description

The completion $\overline{\alpha}$ of an abelian group $\alpha$ with a compatible uniform structure inherits an abelian commutative group structure.

UniformSpace.Completion.instModule instance

[Semiring R] [Module R α] [UniformContinuousConstSMul R α] : Module R (Completion α)

Full source

instance instModule [Semiring R] [Module R α] [UniformContinuousConstSMul R α] :
    Module R (Completion α) :=
  { (inferInstance : DistribMulAction R <| Completion α),
    (inferInstance : MulActionWithZero R <| Completion α) with
    add_smul := fun a b ↦
      ext' (continuous_const_smul _) ((continuous_const_smul _).add (continuous_const_smul _))
        fun x ↦ by
          rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul] }

Module Structure on the Completion of a Uniform Module

Informal description

For any semiring $R$ and any $R$-module $\alpha$ with a compatible uniform structure where scalar multiplication by each element of $R$ is uniformly continuous, the completion $\overline{\alpha}$ of $\alpha$ inherits an $R$-module structure.

AddMonoidHom.extension definition

[CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) : Completion α →+ β

Full source

/-- Extension to the completion of a continuous group hom. -/
def AddMonoidHom.extension [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) :
    CompletionCompletion α →+ β :=
  have hf : UniformContinuous f := uniformContinuous_addMonoidHom_of_continuous hf
  { toFun := Completion.extension f
    map_zero' := by 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 ↦
        show Completion.extension f _ = Completion.extension f _ + Completion.extension f _ by
        rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add] }

Extension of a continuous additive group homomorphism to the completion

Informal description

Given a continuous additive group homomorphism $f \colon \alpha \to \beta$ where $\beta$ is a complete and separated topological abelian group, the extension of $f$ to the completion $\overline{\alpha}$ of $\alpha$ is an additive group homomorphism $\overline{f} \colon \overline{\alpha} \to \beta$ that coincides with $f$ on the image of $\alpha$ in $\overline{\alpha}$.

AddMonoidHom.extension_coe theorem

[CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) (a : α) : f.extension hf a = f a

Full source

theorem AddMonoidHom.extension_coe [CompleteSpace β] [T0Space β] (f : α →+ β)
    (hf : Continuous f) (a : α) : f.extension hf a = f a :=
  UniformSpace.Completion.extension_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

Extension of Continuous Homomorphism Agrees on Original Group

Informal description

Let $\alpha$ be a topological abelian group and $\beta$ be a complete and separated topological abelian group. Given a continuous additive group homomorphism $f \colon \alpha \to \beta$, the extension $\overline{f} \colon \overline{\alpha} \to \beta$ of $f$ to the completion $\overline{\alpha}$ of $\alpha$ satisfies $\overline{f}(a) = f(a)$ for every $a \in \alpha$.

AddMonoidHom.continuous_extension theorem

[CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) : Continuous (f.extension hf)

Full source

@[continuity]
theorem AddMonoidHom.continuous_extension [CompleteSpace β] [T0Space β] (f : α →+ β)
    (hf : Continuous f) : Continuous (f.extension hf) :=
  UniformSpace.Completion.continuous_extension

Continuity of the Extension of a Continuous Additive Group Homomorphism to Completion

Informal description

Let $\alpha$ be a topological abelian group and $\beta$ be a complete and separated topological abelian group. Given a continuous additive group homomorphism $f \colon \alpha \to \beta$, the extension $\overline{f} \colon \overline{\alpha} \to \beta$ of $f$ to the completion $\overline{\alpha}$ of $\alpha$ is continuous.

AddMonoidHom.completion definition

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

Full source

/-- Completion of a continuous group hom, as a group hom. -/
def AddMonoidHom.completion (f : α →+ β) (hf : Continuous f) : CompletionCompletion α →+ Completion β :=
  (toCompl.comp f).extension (continuous_toCompl.comp hf)

Completion of a continuous additive group homomorphism

Informal description

Given a continuous additive group homomorphism $f \colon \alpha \to \beta$ between topological abelian groups, the completion of $f$ is an additive group homomorphism $\overline{f} \colon \overline{\alpha} \to \overline{\beta}$ between their respective completions, defined as the extension of the composition of $f$ with the canonical embedding into $\overline{\beta}$.

AddMonoidHom.continuous_completion theorem

(f : α →+ β) (hf : Continuous f) : Continuous (AddMonoidHom.completion f hf : Completion α → Completion β)

Full source

@[continuity]
theorem AddMonoidHom.continuous_completion (f : α →+ β) (hf : Continuous f) :
    Continuous (AddMonoidHom.completion f hf : Completion α → Completion β) :=
  continuous_map

Continuity of the Completion of a Continuous Additive Group Homomorphism

Informal description

For any continuous additive group homomorphism $f \colon \alpha \to \beta$ between topological abelian groups, the completion $\overline{f} \colon \overline{\alpha} \to \overline{\beta}$ is continuous.

AddMonoidHom.completion_coe theorem

(f : α →+ β) (hf : Continuous f) (a : α) : AddMonoidHom.completion f hf a = f a

Full source

theorem AddMonoidHom.completion_coe (f : α →+ β) (hf : Continuous f) (a : α) :
    AddMonoidHom.completion f hf a = f a :=
  map_coe (uniformContinuous_addMonoidHom_of_continuous hf) a

Completion Preserves Evaluation of Continuous Additive Homomorphisms

Informal description

For any continuous additive group homomorphism $f \colon \alpha \to \beta$ between topological abelian groups and any element $a \in \alpha$, the completion $\overline{f}$ of $f$ evaluated at the canonical embedding of $a$ in the completion $\overline{\alpha}$ equals $f(a)$, i.e., $\overline{f}(a) = f(a)$.

AddMonoidHom.completion_zero theorem

: AddMonoidHom.completion (0 : α →+ β) continuous_const = 0

Full source

theorem AddMonoidHom.completion_zero :
    AddMonoidHom.completion (0 : α →+ β) continuous_const = 0 := by
  ext x
  refine Completion.induction_on x ?_ ?_
  · apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
    exact continuous_const
  · intro a
    simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]

Completion of the Zero Homomorphism is Zero

Informal description

The completion of the zero homomorphism $0 \colon \alpha \to \beta$ is equal to the zero homomorphism on the completions, i.e., $\overline{0} = 0 \colon \overline{\alpha} \to \overline{\beta}$.

AddMonoidHom.completion_add theorem

 {γ : Type*} [AddCommGroup γ] [UniformSpace γ] [IsUniformAddGroup γ] (f g : α →+ γ) (hf : Continuous f)
  (hg : Continuous g) :
  AddMonoidHom.completion (f + g) (hf.add hg) = AddMonoidHom.completion f hf + AddMonoidHom.completion g hg

Full source

theorem AddMonoidHom.completion_add {γ : Type*} [AddCommGroup γ] [UniformSpace γ]
    [IsUniformAddGroup γ] (f g : α →+ γ) (hf : Continuous f) (hg : Continuous g) :
    AddMonoidHom.completion (f + g) (hf.add hg) =
    AddMonoidHom.completion f hf + AddMonoidHom.completion g hg := by
  have hfg := hf.add hg
  ext x
  refine Completion.induction_on x ?_ ?_
  · exact isClosed_eq ((f + g).continuous_completion hfg)
      ((f.continuous_completion hf).add (g.continuous_completion hg))
  · intro a
    simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]

Completion Preserves Sum of Continuous Additive Homomorphisms

Informal description

Let $\gamma$ be a topological abelian group with a compatible uniform structure. For any continuous additive group homomorphisms $f, g \colon \alpha \to \gamma$, the completion of their sum $f + g$ is equal to the sum of their completions, i.e., $\overline{f + g} = \overline{f} + \overline{g}$.

Main declarations: