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.

source

theorem ContinuousMap.addUnitsLift.proof_6 {X : Type u_2} {M : Type u_1} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : AddUnits C(X, M)) (x : X) :

↑(↑(-f) + ↑f) x = ↑0 x

source

theorem ContinuousMap.addUnitsLift.proof_9 {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (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

source

theorem ContinuousMap.addUnitsLift.proof_4 {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) :

((ContinuousMap.mk fun x => ↑(-↑f x)) + ContinuousMap.mk fun x => ↑(↑f x)) = 0

source

def ContinuousMap.addUnitsLift {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] :

C(X, AddUnits M) ≃ AddUnits C(X, 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.

Instances For

source

theorem ContinuousMap.addUnitsLift.proof_7 {X : Type u_2} {M : Type u_1} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (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) }

source

theorem ContinuousMap.addUnitsLift.proof_2 {X : Type u_2} {M : Type u_1} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) :

Continuous (AddUnits.val ∘ fun x => -↑f x)

source

theorem ContinuousMap.addUnitsLift.proof_5 {X : Type u_2} {M : Type u_1} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : AddUnits C(X, M)) (x : X) :

↑(↑f + ↑(-f)) x = ↑0 x

source

theorem ContinuousMap.addUnitsLift.proof_3 {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) :

((ContinuousMap.mk fun x => ↑(↑f x)) + ContinuousMap.mk fun x => ↑(-↑f x)) = 0

source

theorem ContinuousMap.addUnitsLift.proof_1 {X : Type u_2} {M : Type u_1} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] (f : C(X, AddUnits M)) :

Continuous (AddUnits.val ∘ fun x => ↑f x)

source

theorem ContinuousMap.addUnitsLift.proof_8 {X : Type u_2} {M : Type u_1} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) :

(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

source

@[simp]

theorem ContinuousMap.val_addUnitsLift_apply_apply {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) (x : X) :

↑↑(↑ContinuousMap.addUnitsLift f) x = ↑(↑f x)

source

@[simp]

theorem ContinuousMap.val_addUnitsLift_symm_apply_apply {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : AddUnits C(X, M)) (x : X) :

↑(↑(↑ContinuousMap.addUnitsLift.symm f) x) = ↑↑f x

source

@[simp]

theorem ContinuousMap.val_unitsLift_apply_apply {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Monoid M] [TopologicalSpace M] [ContinuousMul M] (f : C(X, Mˣ)) (x : X) :

↑↑(↑ContinuousMap.unitsLift f) x = ↑(↑f x)

source

@[simp]

theorem ContinuousMap.val_unitsLift_symm_apply_apply {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Monoid M] [TopologicalSpace M] [ContinuousMul M] (f : C(X, M)ˣ) (x : X) :

↑(↑(↑ContinuousMap.unitsLift.symm f) x) = ↑↑f x

source

def ContinuousMap.unitsLift {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Monoid M] [TopologicalSpace M] [ContinuousMul M] :

C(X, Mˣ) ≃ C(X, M)ˣ

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

Instances For

source

@[simp]

theorem ContinuousMap.addUnitsLift_apply_neg_apply {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) (x : X) :

↑↑(-↑ContinuousMap.addUnitsLift f) x = ↑(-↑f x)

source

@[simp]

theorem ContinuousMap.unitsLift_apply_inv_apply {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Monoid M] [TopologicalSpace M] [ContinuousMul M] (f : C(X, Mˣ)) (x : X) :

↑↑(↑ContinuousMap.unitsLift f)⁻¹ x = ↑(↑f x)⁻¹

source

@[simp]

theorem ContinuousMap.addUnitsLift_symm_apply_apply_neg' {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : AddUnits C(X, M)) (x : X) :

↑(-↑(↑ContinuousMap.addUnitsLift.symm f) x) = ↑↑(-f) x

source

@[simp]

theorem ContinuousMap.unitsLift_symm_apply_apply_inv' {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [Monoid M] [TopologicalSpace M] [ContinuousMul M] (f : C(X, M)ˣ) (x : X) :

↑(↑(↑ContinuousMap.unitsLift.symm f) x)⁻¹ = ↑↑f⁻¹ x

source

theorem ContinuousMap.continuous_isUnit_unit {X : Type u_1} {R : Type u_3} [TopologicalSpace X] [NormedRing R] [CompleteSpace R] {f : C(X, R)} (h : ∀ (x : X), IsUnit (↑f x)) :

Continuous fun x => IsUnit.unit (h x)

source

@[simp]

theorem ContinuousMap.unitsOfForallIsUnit_apply {X : Type u_1} {R : Type u_3} [TopologicalSpace X] [NormedRing R] [CompleteSpace R] {f : C(X, R)} (h : ∀ (x : X), IsUnit (↑f x)) (x : X) :

↑(ContinuousMap.unitsOfForallIsUnit h) x = IsUnit.unit (h x)

source

noncomputable def ContinuousMap.unitsOfForallIsUnit {X : Type u_1} {R : Type u_3} [TopologicalSpace X] [NormedRing R] [CompleteSpace R] {f : C(X, R)} (h : ∀ (x : X), IsUnit (↑f x)) :

C(X, Rˣ)

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

source

instance ContinuousMap.canLift {X : Type u_1} {R : Type u_3} [TopologicalSpace X] [NormedRing R] [CompleteSpace R] :

CanLift C(X, R) C(X, Rˣ) (fun f => ContinuousMap.mk fun x => ↑(↑f x)) fun f => ∀ (x : X), IsUnit (↑f x)

source

theorem ContinuousMap.isUnit_iff_forall_isUnit {X : Type u_1} {R : Type u_3} [TopologicalSpace X] [NormedRing R] [CompleteSpace R] (f : C(X, R)) :

IsUnit f ↔ ∀ (x : X), IsUnit (↑f x)

source

theorem ContinuousMap.isUnit_iff_forall_ne_zero {X : Type u_1} {𝕜 : Type u_4} [TopologicalSpace X] [NormedField 𝕜] [CompleteSpace 𝕜] (f : C(X, 𝕜)) :

IsUnit f ↔ ∀ (x : X), ↑f x ≠ 0

source

theorem ContinuousMap.spectrum_eq_range {X : Type u_1} {𝕜 : Type u_4} [TopologicalSpace X] [NormedField 𝕜] [CompleteSpace 𝕜] (f : C(X, 𝕜)) :

spectrum 𝕜 f = Set.range ↑f