Units of continuous functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file concerns itself with C(X, M)ˣ and C(X, Mˣ) when X is a topological space
and M has some monoid structure compatible with its topology.
@[simp]
theorem
continuous_map.coe_neg_add_units_lift_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[add_monoid M]
[topological_space M]
[has_continuous_add M]
(f : C(X, add_units M))
(x : X) :
@[simp]
theorem
continuous_map.coe_units_lift_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[monoid M]
[topological_space M]
[has_continuous_mul M]
(f : C(X, Mˣ))
(x : X) :
@[simp]
theorem
continuous_map.coe_add_units_lift_symm_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[add_monoid M]
[topological_space M]
[has_continuous_add M]
(f : add_units C(X, M))
(x : X) :
def
continuous_map.add_units_lift
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[add_monoid M]
[topological_space M]
[has_continuous_add M] :
Equivalence between continuous maps into the additive units of an additive monoid with continuous addition and the additive units of the additive monoid of continuous maps.
Equations
- continuous_map.add_units_lift = {to_fun := λ (f : C(X, add_units M)), {val := {to_fun := λ (x : X), ↑(⇑f x), continuous_to_fun := _}, neg := {to_fun := λ (x : X), ↑-⇑f x, continuous_to_fun := _}, val_neg := _, neg_val := _}, inv_fun := λ (f : add_units C(X, M)), {to_fun := λ (x : X), {val := ⇑f x, neg := (⇑-f) x, val_neg := _, neg_val := _}, continuous_to_fun := _}, left_inv := _, right_inv := _}
@[simp]
theorem
continuous_map.coe_neg_add_units_lift_symm_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[add_monoid M]
[topological_space M]
[has_continuous_add M]
(f : add_units C(X, M))
(x : X) :
@[simp]
theorem
continuous_map.coe_inv_units_lift_symm_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[monoid M]
[topological_space M]
[has_continuous_mul M]
(f : C(X, M)ˣ)
(x : X) :
@[simp]
theorem
continuous_map.coe_units_lift_symm_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[monoid M]
[topological_space M]
[has_continuous_mul M]
(f : C(X, M)ˣ)
(x : X) :
@[simp]
theorem
continuous_map.coe_inv_units_lift_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[monoid M]
[topological_space M]
[has_continuous_mul M]
(f : C(X, Mˣ))
(x : X) :
@[simp]
theorem
continuous_map.coe_add_units_lift_apply_apply
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[add_monoid M]
[topological_space M]
[has_continuous_add M]
(f : C(X, add_units M))
(x : X) :
def
continuous_map.units_lift
{X : Type u_1}
{M : Type u_2}
[topological_space X]
[monoid M]
[topological_space M]
[has_continuous_mul M] :
Equivalence between continuous maps into the units of a monoid with continuous multiplication and the units of the monoid of continuous maps.
Equations
- continuous_map.units_lift = {to_fun := λ (f : C(X, Mˣ)), {val := {to_fun := λ (x : X), ↑(⇑f x), continuous_to_fun := _}, inv := {to_fun := λ (x : X), ↑(⇑f x)⁻¹, continuous_to_fun := _}, val_inv := _, inv_val := _}, inv_fun := λ (f : C(X, M)ˣ), {to_fun := λ (x : X), {val := ⇑f x, inv := ⇑f⁻¹ x, val_inv := _, inv_val := _}, continuous_to_fun := _}, left_inv := _, right_inv := _}
theorem
normed_ring.is_unit_unit_continuous
{X : Type u_1}
{R : Type u_3}
[topological_space X]
[normed_ring R]
[complete_space R]
{f : C(X, R)}
(h : ∀ (x : X), is_unit (⇑f x)) :
continuous (λ (x : X), _.unit)
@[simp]
theorem
continuous_map.units_of_forall_is_unit_apply
{X : Type u_1}
{R : Type u_3}
[topological_space X]
[normed_ring R]
[complete_space R]
{f : C(X, R)}
(h : ∀ (x : X), is_unit (⇑f x))
(x : X) :
noncomputable
def
continuous_map.units_of_forall_is_unit
{X : Type u_1}
{R : Type u_3}
[topological_space X]
[normed_ring R]
[complete_space R]
{f : C(X, R)}
(h : ∀ (x : X), is_unit (⇑f x)) :
Construct a continuous map into the group of units of a normed ring from a function into the normed ring and a proof that every element of the range is a unit.
Equations
- continuous_map.units_of_forall_is_unit h = {to_fun := λ (x : X), _.unit, continuous_to_fun := _}
@[protected, instance]
def
continuous_map.can_lift
{X : Type u_1}
{R : Type u_3}
[topological_space X]
[normed_ring R]
[complete_space R] :
Equations
- continuous_map.can_lift = {prf := _}
theorem
continuous_map.is_unit_iff_forall_is_unit
{X : Type u_1}
{R : Type u_3}
[topological_space X]
[normed_ring R]
[complete_space R]
(f : C(X, R)) :
theorem
continuous_map.is_unit_iff_forall_ne_zero
{X : Type u_1}
{𝕜 : Type u_4}
[topological_space X]
[normed_field 𝕜]
[complete_space 𝕜]
(f : C(X, 𝕜)) :
theorem
continuous_map.spectrum_eq_range
{X : Type u_1}
{𝕜 : Type u_4}
[topological_space X]
[normed_field 𝕜]
[complete_space 𝕜]
(f : C(X, 𝕜)) :