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