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 := ⋯ }
Instances For
theorem
TopologicalSpace.Fiber.sigmaIsoHom_inj
{S : Type u_1}
{Y : Type u_2}
(f : S → Y)
[TopologicalSpace S]
:
theorem
TopologicalSpace.Fiber.sigmaIsoHom_surj
{S : Type u_1}
{Y : Type u_2}
(f : S → Y)
[TopologicalSpace S]
:
def
TopologicalSpace.Fiber.sigmaIncl
{S : Type u_1}
{Y : Type u_2}
(f : S → Y)
[TopologicalSpace S]
(a : Function.Fiber f)
:
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
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
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
- ⋯ = ⋯