doc-next-gen

Mathlib.Topology.Algebra.Constructions

Module docstring

{"# Topological space structure on the opposite monoid and on the units group

In this file we define TopologicalSpace structure on Mᵐᵒᵖ, Mᵃᵒᵖ, Mˣ, and AddUnits M. This file does not import definitions of a topological monoid and/or a continuous multiplicative action, so we postpone the proofs of HasContinuousMul Mᵐᵒᵖ etc till we have these definitions.

Tags

topological space, opposite monoid, units "}

MulOpposite.instTopologicalSpaceMulOpposite instance
[TopologicalSpace M] : TopologicalSpace Mᵐᵒᵖ
Full source 
/-- Put the same topological space structure on the opposite monoid as on the original space. -/
@[to_additive "Put the same topological space structure on the opposite monoid as on the original
space."]
instance instTopologicalSpaceMulOpposite [TopologicalSpace M] : TopologicalSpace Mᵐᵒᵖ :=
  TopologicalSpace.induced (unop : Mᵐᵒᵖ → M) ‹_›
Topological Space Structure on the Opposite Monoid
Informal description
For any topological space $M$, the opposite monoid $M^{\text{op}}$ inherits the same topological space structure as $M$.
MulOpposite.continuous_unop theorem
: Continuous (unop : Mᵐᵒᵖ → M)
Full source 
@[to_additive (attr := continuity)]
theorem continuous_unop : Continuous (unop : Mᵐᵒᵖ → M) :=
  continuous_induced_dom
Continuity of the Unary Operation from Opposite Monoid to Original Space
Informal description
The unary operation `unop` from the opposite monoid $M^{\text{op}}$ to $M$ is continuous, where $M$ is a topological space.
MulOpposite.continuous_op theorem
: Continuous (op : M → Mᵐᵒᵖ)
Full source 
@[to_additive (attr := continuity)]
theorem continuous_op : Continuous (op : M → Mᵐᵒᵖ) :=
  continuous_induced_rng.2 continuous_id
Continuity of the Opposite Monoid Construction Map
Informal description
The canonical map $\text{op} : M \to M^{\text{op}}$ is continuous, where $M^{\text{op}}$ is the opposite monoid of $M$ equipped with the same topological structure as $M$.
MulOpposite.opHomeomorph definition
: M ≃ₜ Mᵐᵒᵖ
Full source 
/-- `MulOpposite.op` as a homeomorphism. -/
@[to_additive (attr := simps!) "`AddOpposite.op` as a homeomorphism."]
def opHomeomorph : M ≃ₜ Mᵐᵒᵖ where
  toEquiv := opEquiv
  continuous_toFun := continuous_op
  continuous_invFun := continuous_unop
Homeomorphism between a space and its opposite monoid
Informal description
The homeomorphism $\text{opHomeomorph} : M \simeq M^{\text{op}}$ between a topological space $M$ and its opposite monoid $M^{\text{op}}$, where the forward map is the canonical operation $\text{op}$ and the inverse map is $\text{unop}$. Both maps are continuous, making this a topological equivalence.
MulOpposite.instT2Space instance
[T2Space M] : T2Space Mᵐᵒᵖ
Full source 
@[to_additive]
instance instT2Space [T2Space M] : T2Space Mᵐᵒᵖ := opHomeomorph.t2Space
Hausdorff Property of the Opposite Monoid
Informal description
For any topological space $M$ that is Hausdorff, the opposite monoid $M^{\text{op}}$ is also Hausdorff.
MulOpposite.map_op_nhds theorem
(x : M) : map (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (op x)
Full source 
@[to_additive (attr := simp)]
theorem map_op_nhds (x : M) : map (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (op x) :=
  opHomeomorph.map_nhds_eq x
Neighborhood Filter Preservation under Opposite Monoid Map
Informal description
For any point $x$ in a topological space $M$, the image of the neighborhood filter $\mathcal{N}(x)$ under the canonical map $\text{op} : M \to M^{\text{op}}$ is equal to the neighborhood filter $\mathcal{N}(\text{op}(x))$ in the opposite monoid $M^{\text{op}}$.
MulOpposite.map_unop_nhds theorem
(x : Mᵐᵒᵖ) : map (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (unop x)
Full source 
@[to_additive (attr := simp)]
theorem map_unop_nhds (x : Mᵐᵒᵖ) : map (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (unop x) :=
  opHomeomorph.symm.map_nhds_eq x
Neighborhood Filter Preservation under Opposite Monoid Unop Map
Informal description
For any element $x$ in the opposite monoid $M^{\text{op}}$, the image of the neighborhood filter $\mathcal{N}(x)$ under the canonical map $\text{unop} : M^{\text{op}} \to M$ is equal to the neighborhood filter $\mathcal{N}(\text{unop}(x))$ in $M$.
MulOpposite.comap_op_nhds theorem
(x : Mᵐᵒᵖ) : comap (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (unop x)
Full source 
@[to_additive (attr := simp)]
theorem comap_op_nhds (x : Mᵐᵒᵖ) : comap (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (unop x) :=
  opHomeomorph.comap_nhds_eq x
Neighborhood Filter Preimage under Opposite Monoid Map
Informal description
For any element $x$ in the opposite monoid $M^{\text{op}}$, the preimage of the neighborhood filter $\mathcal{N}(x)$ under the canonical map $\text{op} : M \to M^{\text{op}}$ is equal to the neighborhood filter $\mathcal{N}(\text{unop}(x))$ in $M$.
MulOpposite.comap_unop_nhds theorem
(x : M) : comap (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (op x)
Full source 
@[to_additive (attr := simp)]
theorem comap_unop_nhds (x : M) : comap (unop : Mᵐᵒᵖ → M) (𝓝 x) = 𝓝 (op x) :=
  opHomeomorph.symm.comap_nhds_eq x
Neighborhood Filter Preimage under Opposite Monoid Unop Map
Informal description
For any element $x$ in a topological space $M$, the preimage of the neighborhood filter $\mathcal{N}(x)$ under the canonical map $\text{unop} : M^{\text{op}} \to M$ is equal to the neighborhood filter $\mathcal{N}(\text{op}(x))$ in $M^{\text{op}}$.
Units.instTopologicalSpaceUnits instance
: TopologicalSpace Mˣ
Full source 
/-- The units of a monoid are equipped with a topology, via the embedding into `M × M`. -/
@[to_additive "The additive units of a monoid are equipped with a topology, via the embedding into
`M × M`."]
instance instTopologicalSpaceUnits : TopologicalSpace Mˣ :=
  TopologicalSpace.induced (embedProduct M) inferInstance
Topological Space Structure on the Group of Units
Informal description
The group of units $M^\times$ of a monoid $M$ is equipped with the topology induced by the embedding $M^\times \to M \times M$ that sends each unit to itself and its inverse.
Units.isInducing_embedProduct theorem
: IsInducing (embedProduct M)
Full source 
@[to_additive]
theorem isInducing_embedProduct : IsInducing (embedProduct M) := ⟨rfl⟩
Embedding of Units into Product Space is Inducing
Informal description
The embedding $\text{embedProduct} : M^\times \to M \times M$ of the group of units into the product space is inducing, meaning that the topology on $M^\times$ is the coarsest topology such that $\text{embedProduct}$ is continuous.
Units.isEmbedding_embedProduct theorem
: IsEmbedding (embedProduct M)
Full source 
@[to_additive]
theorem isEmbedding_embedProduct : IsEmbedding (embedProduct M) :=
  ⟨isInducing_embedProduct, embedProduct_injective M⟩
Embedding of Units into Product Space is Topological Embedding
Informal description
The embedding $\text{embedProduct} : M^\times \to M \times M$ of the group of units into the product space is an embedding, meaning it is both injective and induces the topology on $M^\times$ as a subspace of $M \times M$.
Units.topology_eq_inf theorem
: instTopologicalSpaceUnits = .induced (val : Mˣ → M) ‹_› ⊓ .induced (fun u ↦ ↑u⁻¹ : Mˣ → M) ‹_›
Full source 
@[to_additive] lemma topology_eq_inf :
    instTopologicalSpaceUnits =
      .induced.induced (val : Mˣ → M) ‹_› ⊓ .induced (fun u ↦ ↑u⁻¹ : Mˣ → M) ‹_› := by
  simp only [isInducing_embedProduct.1, instTopologicalSpaceProd, induced_inf,
    instTopologicalSpaceMulOpposite, induced_compose]; rfl
Topology on Units as Infimum of Induced Topologies
Informal description
The topology on the group of units $M^\times$ of a monoid $M$ is equal to the infimum (coarsest topology finer than both) of the topology induced by the inclusion map $M^\times \to M$ and the topology induced by the map $u \mapsto u^{-1}$ from $M^\times$ to $M$.
Units.isEmbedding_val_mk' theorem
{M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M} (hc : ContinuousOn f {x : M | IsUnit x}) (hf : ∀ u : Mˣ, f u.1 = ↑u⁻¹) : IsEmbedding (val : Mˣ → M)
Full source 
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/
@[to_additive "An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead."]
lemma isEmbedding_val_mk' {M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M}
    (hc : ContinuousOn f {x : M | IsUnit x}) (hf : ∀ u : Mˣ, f u.1 = ↑u⁻¹) :
    IsEmbedding (val : Mˣ → M) := by
  refine ⟨⟨?_⟩, ext⟩
  rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
    @continuous_iff_continuousAt _ _ (.induced _ _)]
  intros u s hs
  simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
  exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩
Topological Embedding of Units via Inverse Condition
Informal description
Let $M$ be a monoid with a topological space structure, and let $f \colon M \to M$ be a function that is continuous on the subset $\{x \in M \mid \text{$x$ is a unit}\}$. If for every unit $u \in M^\times$, the function $f$ satisfies $f(u) = u^{-1}$, then the inclusion map $M^\times \to M$ is a topological embedding.
Units.embedding_val_mk theorem
{M : Type*} [DivisionMonoid M] [TopologicalSpace M] (h : ContinuousOn Inv.inv {x : M | IsUnit x}) : IsEmbedding (val : Mˣ → M)
Full source 
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/
@[to_additive "An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead."]
lemma embedding_val_mk {M : Type*} [DivisionMonoid M] [TopologicalSpace M]
    (h : ContinuousOn Inv.inv {x : M | IsUnit x}) : IsEmbedding (val : Mˣ → M) :=
  isEmbedding_val_mk' h fun u ↦ (val_inv_eq_inv_val u).symm
Topological Embedding of Units via Continuous Inversion
Informal description
Let $M$ be a division monoid with a topological space structure. If the inversion operation $\text{Inv.inv}$ is continuous on the subset $\{x \in M \mid \text{$x$ is a unit}\}$, then the inclusion map $M^\times \to M$ is a topological embedding.
Units.continuous_embedProduct theorem
: Continuous (embedProduct M)
Full source 
@[to_additive]
theorem continuous_embedProduct : Continuous (embedProduct M) :=
  continuous_induced_dom
Continuity of the Embedding of Units into $M \times M$
Informal description
The embedding map $\text{embedProduct} : M^\times \to M \times M$, which sends each unit $u \in M^\times$ to the pair $(u, u^{-1})$, is continuous when $M^\times$ is equipped with the induced topology from $M \times M$.
Units.continuous_val theorem
: Continuous ((↑) : Mˣ → M)
Full source 
@[to_additive]
theorem continuous_val : Continuous ((↑) : Mˣ → M) :=
  (@continuous_embedProduct M _ _).fst
Continuity of the Unit Inclusion Map $M^\times \to M$
Informal description
The canonical inclusion map from the group of units $M^\times$ to the monoid $M$ is continuous, where $M^\times$ is equipped with the induced topology from $M \times M$.
Units.continuous_iff theorem
{f : X → Mˣ} : Continuous f ↔ Continuous (val ∘ f) ∧ Continuous (fun x => ↑(f x)⁻¹ : X → M)
Full source 
@[to_additive]
protected theorem continuous_iff {f : X → Mˣ} :
    ContinuousContinuous f ↔ Continuous (val ∘ f) ∧ Continuous (fun x => ↑(f x)⁻¹ : X → M) := by
  simp only [isInducing_embedProduct.continuous_iff, embedProduct_apply, Function.comp_def,
    continuous_prodMk, opHomeomorph.symm.isInducing.continuous_iff, opHomeomorph_symm_apply,
    unop_op]
Characterization of Continuous Functions into the Group of Units
Informal description
For any function $f : X \to M^\times$ from a topological space $X$ to the group of units $M^\times$ of a monoid $M$, the function $f$ is continuous if and only if both the composition $\text{val} \circ f : X \to M$ (where $\text{val}$ is the inclusion map) and the function $x \mapsto (f(x))^{-1} : X \to M$ are continuous.
Units.continuous_coe_inv theorem
: Continuous (fun u => ↑u⁻¹ : Mˣ → M)
Full source 
@[to_additive]
theorem continuous_coe_inv : Continuous (fun u => ↑u⁻¹ : Mˣ → M) :=
  (Units.continuous_iff.1 continuous_id).2
Continuity of the Inverse Map $M^\times \to M$
Informal description
The function that maps each unit $u$ in the group of units $M^\times$ to its inverse $u^{-1}$ (considered as an element of $M$) is continuous, where $M^\times$ is equipped with the topology induced by the embedding $M^\times \to M \times M$.