# Documentation

Mathlib.Topology.ContinuousFunction.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.

theorem ContinuousMap.addUnitsLift.proof_6 {X : Type u_2} {M : Type u_1} [] [] [] [] (f : AddUnits C(X, M)) (x : X) :
↑(↑(-f) + f) x = 0 x
theorem ContinuousMap.addUnitsLift.proof_9 {X : Type u_1} {M : Type u_2} [] [] [] [] (f : AddUnits C(X, M)) :
(fun f => { val := ContinuousMap.mk fun x => ↑(f x), neg := ContinuousMap.mk fun x => ↑(-f x), val_neg := (_ : ((ContinuousMap.mk fun x => ↑(f x)) + ContinuousMap.mk fun x => ↑(-f x)) = 0), neg_val := (_ : ((ContinuousMap.mk fun x => ↑(-f x)) + ContinuousMap.mk fun x => ↑(f x)) = 0) }) ((fun f => ContinuousMap.mk fun x => { val := f x, neg := ↑(-f) x, val_neg := (_ : ↑(f + ↑(-f)) x = 0 x), neg_val := (_ : ↑(↑(-f) + f) x = 0 x) }) f) = f
theorem ContinuousMap.addUnitsLift.proof_4 {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, )) :
((ContinuousMap.mk fun x => ↑(-f x)) + ContinuousMap.mk fun x => ↑(f x)) = 0
def ContinuousMap.addUnitsLift {X : Type u_1} {M : Type u_2} [] [] [] [] :

Instances For
theorem ContinuousMap.addUnitsLift.proof_7 {X : Type u_2} {M : Type u_1} [] [] [] [] (f : AddUnits C(X, M)) :
Continuous fun x => { val := f x, neg := ↑(-f) x, val_neg := (_ : ↑(f + ↑(-f)) x = 0 x), neg_val := (_ : ↑(↑(-f) + f) x = 0 x) }
theorem ContinuousMap.addUnitsLift.proof_2 {X : Type u_2} {M : Type u_1} [] [] [] [] (f : C(X, )) :
Continuous (AddUnits.val fun x => -f x)
theorem ContinuousMap.addUnitsLift.proof_5 {X : Type u_2} {M : Type u_1} [] [] [] [] (f : AddUnits C(X, M)) (x : X) :
↑(f + ↑(-f)) x = 0 x
theorem ContinuousMap.addUnitsLift.proof_3 {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, )) :
((ContinuousMap.mk fun x => ↑(f x)) + ContinuousMap.mk fun x => ↑(-f x)) = 0
theorem ContinuousMap.addUnitsLift.proof_1 {X : Type u_2} {M : Type u_1} [] [] [] (f : C(X, )) :
Continuous (AddUnits.val fun x => f x)
theorem ContinuousMap.addUnitsLift.proof_8 {X : Type u_2} {M : Type u_1} [] [] [] [] (f : C(X, )) :
(fun f => ContinuousMap.mk fun x => { val := f x, neg := ↑(-f) x, val_neg := (_ : ↑(f + ↑(-f)) x = 0 x), neg_val := (_ : ↑(↑(-f) + f) x = 0 x) }) ((fun f => { val := ContinuousMap.mk fun x => ↑(f x), neg := ContinuousMap.mk fun x => ↑(-f x), val_neg := (_ : ((ContinuousMap.mk fun x => ↑(f x)) + ContinuousMap.mk fun x => ↑(-f x)) = 0), neg_val := (_ : ((ContinuousMap.mk fun x => ↑(-f x)) + ContinuousMap.mk fun x => ↑(f x)) = 0) }) f) = f
@[simp]
theorem ContinuousMap.val_addUnitsLift_apply_apply {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, )) (x : X) :
↑(ContinuousMap.addUnitsLift f) x = ↑(f x)
@[simp]
theorem ContinuousMap.val_addUnitsLift_symm_apply_apply {X : Type u_1} {M : Type u_2} [] [] [] [] (f : AddUnits C(X, M)) (x : X) :
↑(↑(ContinuousMap.addUnitsLift.symm f) x) = f x
@[simp]
theorem ContinuousMap.val_unitsLift_apply_apply {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, Mˣ)) (x : X) :
↑(ContinuousMap.unitsLift f) x = ↑(f x)
@[simp]
theorem ContinuousMap.val_unitsLift_symm_apply_apply {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, M)ˣ) (x : X) :
↑(↑(ContinuousMap.unitsLift.symm f) x) = f x
def ContinuousMap.unitsLift {X : Type u_1} {M : Type u_2} [] [] [] [] :

Equivalence between continuous maps into the units of a monoid with continuous multiplication and the units of the monoid of continuous maps.

Instances For
@[simp]
theorem ContinuousMap.addUnitsLift_apply_neg_apply {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, )) (x : X) :
↑(-ContinuousMap.addUnitsLift f) x = ↑(-f x)
@[simp]
theorem ContinuousMap.unitsLift_apply_inv_apply {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, Mˣ)) (x : X) :
(ContinuousMap.unitsLift f)⁻¹ x = (f x)⁻¹
@[simp]
theorem ContinuousMap.addUnitsLift_symm_apply_apply_neg' {X : Type u_1} {M : Type u_2} [] [] [] [] (f : AddUnits C(X, M)) (x : X) :
↑(-↑(ContinuousMap.addUnitsLift.symm f) x) = ↑(-f) x
@[simp]
theorem ContinuousMap.unitsLift_symm_apply_apply_inv' {X : Type u_1} {M : Type u_2} [] [] [] [] (f : C(X, M)ˣ) (x : X) :
(↑(ContinuousMap.unitsLift.symm f) x)⁻¹ = f⁻¹ x
theorem ContinuousMap.continuous_isUnit_unit {X : Type u_1} {R : Type u_3} [] [] [] {f : C(X, R)} (h : ∀ (x : X), IsUnit (f x)) :
Continuous fun x => IsUnit.unit (h x)
@[simp]
theorem ContinuousMap.unitsOfForallIsUnit_apply {X : Type u_1} {R : Type u_3} [] [] [] {f : C(X, R)} (h : ∀ (x : X), IsUnit (f x)) (x : X) :
= IsUnit.unit (h x)
noncomputable def ContinuousMap.unitsOfForallIsUnit {X : Type u_1} {R : Type u_3} [] [] [] {f : C(X, R)} (h : ∀ (x : X), IsUnit (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.

Instances For
instance ContinuousMap.canLift {X : Type u_1} {R : Type u_3} [] [] [] :
CanLift C(X, R) C(X, Rˣ) (fun f => ContinuousMap.mk fun x => ↑(f x)) fun f => ∀ (x : X), IsUnit (f x)
theorem ContinuousMap.isUnit_iff_forall_isUnit {X : Type u_1} {R : Type u_3} [] [] [] (f : C(X, R)) :
∀ (x : X), IsUnit (f x)
theorem ContinuousMap.isUnit_iff_forall_ne_zero {X : Type u_1} {𝕜 : Type u_4} [] [] [] (f : C(X, 𝕜)) :
∀ (x : X), f x 0
theorem ContinuousMap.spectrum_eq_range {X : Type u_1} {𝕜 : Type u_4} [] [] [] (f : C(X, 𝕜)) :
spectrum 𝕜 f =