mathlib documentation

topology.continuous_function.units

Units of continuous functions #

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]

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
@[simp]
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
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
@[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
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)) :
is_unit f ∀ (x : X), is_unit (f x)
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, 𝕜)) :
is_unit f ∀ (x : X), f x 0
theorem continuous_map.spectrum_eq_range {X : Type u_1} {𝕜 : Type u_4} [topological_space X] [normed_field 𝕜] [complete_space 𝕜] (f : C(X, 𝕜)) :