Documentation

TauCeti.Topology.ContinuousMap.FiberIndicator

Continuous fibre indicators #

A continuous map to a discrete space has continuous fibre indicators. These functions pull back under composition and vanish on empty fibres. Integer-valued decompositions into finite sums of separated products transport to any topological commutative ring, which allows the same decomposition to be used with different coefficient rings.

source
noncomputable def ContinuousMap.fiberIndicator {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [Zero R] [One R] [DiscreteTopology A] (q : C(X, A)) (a : A) :
C(X, R)

The continuous characteristic function of a fibre of a map to a discrete space.

Instances For
    source
    @[simp]
    theorem ContinuousMap.fiberIndicator_apply {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [Zero R] [One R] [DiscreteTopology A] [DecidableEq A] (q : C(X, A)) (a : A) (x : X) :
    (q.fiberIndicator a) x = if q x = a then 1 else 0
    source
    @[simp]
    theorem ContinuousMap.fiberIndicator_comp {X : Type u_1} {A : Type u_2} {B : Type u_3} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace R] [Zero R] [One R] [DiscreteTopology A] (q : C(X, A)) (φ : C(B, X)) (a : A) :
    (q.fiberIndicator a).comp φ = (q.comp φ).fiberIndicator a

    The fibre indicators of q pull back to the fibre indicators of q ∘ φ.

    source
    theorem ContinuousMap.fiberIndicator_eq_zero_of_notMem_range {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [Zero R] [One R] [DiscreteTopology A] {q : C(X, A)} {a : A} (ha : a ∉ Set.range ⇑q) :
    q.fiberIndicator a = 0

    The indicator of an empty fibre vanishes.

    source
    theorem ContinuousMap.fiberIndicator_comp_eq_sum_intCast {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [DiscreteTopology A] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (q : C(X, A)) (m : C(X × X, X)) (a : A) {n : ℕ} (g h : Fin n → C(X, ℤ)) (hgh : ∀ (x y : X), ((q.comp m).fiberIndicator a) (x, y) = ∑ i : Fin n, (g i) x * (h i) y) :
    (q.fiberIndicator a).comp m = ∑ i : Fin n, (prodMul ↑(g i).intCastLocallyConstant) ↑(h i).intCastLocallyConstant

    Transport an integer fibre-indicator decomposition into any topological commutative ring.