This file defines the type f.Fiber of fibers of a function f : Y → Z, and provides some API to work with and construct terms of this type.

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).

def Function.Fiber {Y : Type u_2} {Z : Type u_3} (f : Y → Z) : Type u_2

The indexing set of the partition.

Equations

• Function.Fiber f = ↑(Set.range fun (x : ↑(Set.range f)) => f ⁻¹' {↑x})

noncomputable def Function.Fiber.image {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) : Z

Any a : Fiber f is of the form f ⁻¹' {x} for some x in the image of f. We define a.image as an arbitrary such x.

Equations

• Function.Fiber.image f a = ↑(Exists.choose ⋯)

theorem Function.Fiber.eq_fiber_image {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) : ↑a = f ⁻¹' {Function.Fiber.image f a}

def Function.Fiber.mk {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y) : Function.Fiber f

Given y : Y, Fiber.mk f y is the fiber of f that y belongs to, as an element of Fiber f.

Equations

• Function.Fiber.mk f y = ⟨f ⁻¹' {f y}, ⋯⟩

def Function.Fiber.mkSelf {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y) : ↑↑(Function.Fiber.mk f y)

y : Y as a term of the type Fiber.mk f y

Equations

• Function.Fiber.mkSelf f y = ⟨y, ⋯⟩

theorem Function.Fiber.map_eq_image {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) (x : ↑↑a) : f ↑x = Function.Fiber.image f a

theorem Function.Fiber.mk_image {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y) : Function.Fiber.image f (Function.Fiber.mk f y) = f y

theorem Function.Fiber.mem_iff_eq_image {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (y : Y) (a : Function.Fiber f) : y ∈ ↑a ↔ f y = Function.Fiber.image f a

noncomputable def Function.Fiber.preimage {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) : Y

An arbitrary element of a : Fiber f.

Equations

• Function.Fiber.preimage f a = Exists.choose ⋯

theorem Function.Fiber.map_preimage_eq_image {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) : f (Function.Fiber.preimage f a) = Function.Fiber.image f a

theorem Function.Fiber.fiber_nonempty {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (a : Function.Fiber f) : (↑a).Nonempty

theorem Function.Fiber.map_preimage_eq_image_map {Y : Type u_2} {Z : Type u_3} {W : Type u_4} (f : Y → Z) (g : Z → W) (a : Function.Fiber (g ∘ f)) : g (f (Function.Fiber.preimage (g ∘ f) a)) = Function.Fiber.image (g ∘ f) a

theorem Function.Fiber.image_eq_image_mk {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (g : X → Y) (a : Function.Fiber (f ∘ g)) : Function.Fiber.image (f ∘ g) a = Function.Fiber.image f (Function.Fiber.mk f (g (Function.Fiber.preimage (f ∘ g) a)))