Graphs and fibre products of functions

This file adds to Mathlib's API for graphs of functions over a set and for the fibre product Function.Pullback f g of two functions with a common codomain.

Main results

• Set.graphOn_const: the graph of a constant function over s is a horizontal slice s ×ˢ {b}.
• Function.Pullback.ext: a point of the fibre product is determined by its two coordinates.
• Function.Pullback.fstPreimageEquiv: the fibre of the projection X ×_Y Z → X over x is the fibre of g over f x.

@[simp]

theorem Set.graphOn_const {α : Type u_1} {β : Type u_2} (s : Set α) (b : β) : graphOn (Function.const α b) s = s ×ˢ {b}

The graph of a constant function over a set s is the slice s ×ˢ {b}.

theorem Function.Pullback.ext {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} {p q : Pullback f g} (h₁ : p.fst = q.fst) (h₂ : p.snd = q.snd) : p = q

A point of the fibre product X ×_Y Z is determined by its two coordinates.

theorem Function.Pullback.ext_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} {p q : Pullback f g} : p = q ↔ p.fst = q.fst ∧ p.snd = q.snd

def Function.Pullback.fstPreimageEquiv {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} (x : X) : ↑(fst ⁻¹' {x}) ≃ ↑(g ⁻¹' {f x})

The fibre over x of the projection X ×_Y Z → X of the fibre product of f and g is the fibre of g over f x.

@[simp]

theorem Function.Pullback.fstPreimageEquiv_apply_coe {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} (x : X) (y : ↑(fst ⁻¹' {x})) : ↑((fstPreimageEquiv x) y) = (↑y).snd

@[simp]

theorem Function.Pullback.fst_fstPreimageEquiv_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} (x : X) (z : ↑(g ⁻¹' {f x})) : (↑((fstPreimageEquiv x).symm z)).fst = x

@[simp]

theorem Function.Pullback.snd_fstPreimageEquiv_symm_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Z → Y} (x : X) (z : ↑(g ⁻¹' {f x})) : (↑((fstPreimageEquiv x).symm z)).snd = ↑z