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.

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 : C(X, AddUnits M)) => { val := { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ }, neg := { toFun := fun (x : X) => ↑(-f x), continuous_toFun := ⋯ }, val_neg := ⋯, neg_val := ⋯ }) ((fun (f : AddUnits C(X, M)) => { toFun := fun (x : X) => { val := ↑f x, neg := ↑(-f) x, val_neg := ⋯, neg_val := ⋯ }, continuous_toFun := ⋯ }) 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)) :
{ toFun := fun (x : X) => ↑(-f x), continuous_toFun := ⋯ } + { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ } = 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ContinuousMap.addUnitsLift.proof_7 {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : AddUnits C(X, M)) :
    Continuous fun (x : X) => { val := ↑f x, neg := ↑(-f) x, val_neg := ⋯, neg_val := ⋯ }
    source
    theorem ContinuousMap.addUnitsLift.proof_2 {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : C(X, AddUnits M)) :
    Continuous (AddUnits.val ∘ fun (x : 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)) :
    { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ } + { toFun := fun (x : X) => ↑(-f x), continuous_toFun := ⋯ } = 0
    source
    theorem ContinuousMap.addUnitsLift.proof_1 {X : Type u_1} {M : Type u_2} [TopologicalSpace X] [AddMonoid M] [TopologicalSpace M] (f : C(X, AddUnits M)) :
    Continuous (AddUnits.val ∘ fun (x : 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 : AddUnits C(X, M)) => { toFun := fun (x : X) => { val := ↑f x, neg := ↑(-f) x, val_neg := ⋯, neg_val := ⋯ }, continuous_toFun := ⋯ }) ((fun (f : C(X, AddUnits M)) => { val := { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ }, neg := { toFun := fun (x : X) => ↑(-f x), continuous_toFun := ⋯ }, val_neg := ⋯, neg_val := ⋯ }) 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.

    Equations
    • One or more equations did not get rendered due to their size.
    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 : X) => ⋯.unit
      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 = ⋯.unit
      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.

      Equations
      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 : C(X, Rˣ)) => { toFun := fun (x : X) => ↑(f x), continuous_toFun := ⋯ }) fun (f : C(X, R)) => ∀ (x : X), IsUnit (f x)
        Equations
        • ⋯ = ⋯
        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} {R : Type u_3} [TopologicalSpace X] [NormedDivisionRing R] [CompleteSpace R] (f : C(X, R)) :
        IsUnit f ↔ ∀ (x : X), f x ≠ 0
        source
        theorem ContinuousMap.spectrum_eq_preimage_range {X : Type u_1} {R : Type u_3} {𝕜 : Type u_4} [TopologicalSpace X] [NormedField 𝕜] [NormedDivisionRing R] [Algebra 𝕜 R] [CompleteSpace R] (f : C(X, R)) :
        spectrum 𝕜 f = ⇑(algebraMap 𝕜 R) ⁻¹' Set.range ⇑f
        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