Fibers of a map from a topological space

This file provides some API surrounding Function.Fiber (see Mathlib/Logic/Function/FiberPartition.lean) in the presence of a topology on the domain of the function.

Note: this API is designed to be useful when defining the counit of the adjunction between the functor which takes a set to the condensed set corresponding to locally constant maps to that set, and the forgetful functor from the category of condensed sets to the category of sets (see PR https://github.com/leanprover-community/mathlib4/pull/14027).

def TopologicalSpace.Fiber.sigmaIsoHom {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] : C((x : Function.Fiber f) × ↑↑x, S)

The canonical map from the disjoint union induced by f to S.

Equations

• TopologicalSpace.Fiber.sigmaIsoHom f = { toFun := fun (x : (x : Function.Fiber f) × ↑↑x) => match x with | ⟨a, x⟩ => ↑x, continuous_toFun := ⋯ }

@[simp]

theorem TopologicalSpace.Fiber.sigmaIsoHom_apply {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] (x✝ : (x : Function.Fiber f) × ↑↑x) : (sigmaIsoHom f) x✝ = match x✝ with | ⟨a, x⟩ => ↑x

theorem TopologicalSpace.Fiber.sigmaIsoHom_inj {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] : Function.Injective ⇑(sigmaIsoHom f)

theorem TopologicalSpace.Fiber.sigmaIsoHom_surj {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] : Function.Surjective ⇑(sigmaIsoHom f)

def TopologicalSpace.Fiber.sigmaIncl {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] (a : Function.Fiber f) : C(↑↑a, S)

The inclusion map from a component of the disjoint union induced by f into S.

Equations

• TopologicalSpace.Fiber.sigmaIncl f a = { toFun := fun (x : ↑↑a) => ↑x, continuous_toFun := ⋯ }

def TopologicalSpace.Fiber.sigmaInclIncl {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] {X : Type u_3} (g : Y → X) (a : Function.Fiber (g ∘ f)) (b : Function.Fiber (f ∘ ⇑(sigmaIncl (g ∘ f) a))) : C(↑↑b, ↑↑(Function.Fiber.mk f ↑(Function.Fiber.preimage (f ∘ ⇑(sigmaIncl (g ∘ f) a)) b)))

The inclusion map from a fiber of a composition into the intermediate fiber.

Equations

• TopologicalSpace.Fiber.sigmaInclIncl f g a b = { toFun := fun (x : ↑↑b) => ⟨↑↑x, ⋯⟩, continuous_toFun := ⋯ }

instance TopologicalSpace.Fiber.instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton {S : Type u_1} {Y : Type u_2} [TopologicalSpace S] (l : LocallyConstant S Y) [CompactSpace S] (x : Function.Fiber ⇑l) : CompactSpace ↑↑x

instance TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant {S : Type u_1} {Y : Type u_2} [TopologicalSpace S] (l : LocallyConstant S Y) [CompactSpace S] : Finite (Function.Fiber ⇑l)