Mathlib.Topology.FiberPartition

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 https://github.com/leanprover-community/mathlib4/pull/14027).

source

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

Instances For

source

@[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

source

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

Function.Injective ⇑(TopologicalSpace.Fiber.sigmaIsoHom f)

source

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

Function.Surjective ⇑(TopologicalSpace.Fiber.sigmaIsoHom f)

source

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

Instances For

source

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

Instances For

source

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

⋯ = ⋯

source

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

⋯ = ⋯