This file provides some API surrounding Function.Fiber (see Mathlib.Logic.Function.FiberPartition) 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 #14027).

@[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), (TopologicalSpace.Fiber.sigmaIsoHom f) x = match x with | ⟨a, x⟩ => ↑x

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 := ⋯ }

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

theorem TopologicalSpace.Fiber.sigmaIsoHom_surj {S : Type u_1} {Y : Type u_2} (f : S → Y) [TopologicalSpace S] : Function.Surjective ⇑(TopologicalSpace.Fiber.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 ∘ ⇑(TopologicalSpace.Fiber.sigmaIncl (g ∘ f) a))) : C(↑↑b, ↑↑(Function.Fiber.mk f ↑(Function.Fiber.preimage (f ∘ ⇑(TopologicalSpace.Fiber.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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯