Composition of total arrows and sums over arrows with a given source

The total arrows Quiver.Total C of a category form a space of their own, as for the arrows of a topological or étale groupoid. Two total arrows a and b are composable when the target of a is the source of b, and then Quiver.Total.comp is the total arrow a ≫ b. Its continuity on the subspace of composable pairs is the continuity of composition of a topological groupoid.

A total arrow with identified endpoints is read as a morphism between those endpoints by Mathlib's Quiver.homOfEq, which recovers the total arrow (Quiver.Total.mk_homOfEq) and turns composition of morphisms into composition of total arrows (Quiver.Total.mk_homOfEq_comp_homOfEq).

A sum over the total arrows with source x is a sum over the arrows x ⟶ y for all y (Quiver.Total.finsum_mem_preimage_left_singleton). In a category, an isomorphism x ≅ y matches the arrows out of x with those out of y with the same targets, so the sum of a function of the target over the arrows with source x depends only on the isomorphism class of x (Quiver.Total.finsum_mem_preimage_left_singleton_eq_of_iso). Such sums define the cutoff functions of étale groupoids. In a groupoid, inverting arrows turns it into the sum of the same function of the source over the arrows Quiver.Costar x with target x (Quiver.Total.finsum_costar_eq_finsum_mem_preimage_left_singleton).

Main declarations

• Quiver.Total.comp: the composite of two composable total arrows of a category.
• Quiver.Total.comp_inv_comp, Quiver.Total.inv_comp_comp: in a groupoid, composing with an arrow and with its inverse cancel.

@[simp]

theorem Quiver.Total.mk_homOfEq {V : Type u_1} [Quiver V] (a : Total V) {y z : V} (hy : a.left = y) (hz : a.right = z) : { left := y, right := z, hom := homOfEq a.hom hy hz } = a

A total arrow, read as a morphism between objects equal to its endpoints, is again the same total arrow.

theorem Quiver.Total.preimage_left_singleton {V : Type u_1} [Quiver V] (x : V) : left ⁻¹' {x} = Set.range fun (p : (y : V) × (x ⟶ y)) => { left := x, right := p.fst, hom := p.snd }

The total arrows with source x are the arrows x ⟶ y, for all objects y.

theorem Quiver.Total.finsum_mem_preimage_left_singleton {V : Type u_1} [Quiver V] {M : Type u_2} [AddCommMonoid M] (g : Total V → M) (x : V) : ∑ᶠ (a : Total V) (_ : a ∈ left ⁻¹' {x}), g a = ∑ᶠ (p : (y : V) × (x ⟶ y)), g { left := x, right := p.fst, hom := p.snd }

A sum over the total arrows with source x is a sum over the arrows x ⟶ y.

theorem Quiver.Total.finsum_mem_preimage_left_singleton_eq_of_iso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {M : Type u_2} [AddCommMonoid M] (g : C → M) {x y : C} (e : x ≅ y) : ∑ᶠ (a : Total C) (_ : a ∈ left ⁻¹' {x}), g a.right = ∑ᶠ (a : Total C) (_ : a ∈ left ⁻¹' {y}), g a.right

The sum of a function of the target over the total arrows with source x only depends on the isomorphism class of x: an isomorphism x ≅ y identifies the arrows out of x with those out of y, preserving targets.

theorem Quiver.Total.finsum_costar_eq_finsum_mem_preimage_left_singleton {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.IsGroupoid C] {M : Type u_2} [AddCommMonoid M] (g : C → M) (x : C) : ∑ᶠ (b : Costar x), g b.fst = ∑ᶠ (a : Total C) (_ : a ∈ left ⁻¹' {x}), g a.right

In a groupoid, inverting arrows identifies the arrows with target x with those with source x. So the sum of a function of the source over the arrows with target x is the sum of the same function of the target over the total arrows with source x.

def Quiver.Total.comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (a b : Total C) (h : a.right = b.left) : Total C

The composite of total arrows a and b of a category with the target of a equal to the source of b: the first arrow is followed by the second.

theorem Quiver.Total.comp_def {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (a b : Total C) (h : a.right = b.left) : a.comp b h = { left := a.left, right := b.right, hom := CategoryTheory.CategoryStruct.comp a.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) b.hom) }

@[simp]

theorem Quiver.Total.comp_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (a b : Total C) (h : a.right = b.left) : (a.comp b h).left = a.left

@[simp]

theorem Quiver.Total.comp_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (a b : Total C) (h : a.right = b.left) : (a.comp b h).right = b.right

@[simp]

theorem Quiver.Total.mk_comp_mk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {x y z : C} (f : x ⟶ y) (g : y ⟶ z) : { left := x, right := y, hom := f }.comp { left := y, right := z, hom := g } ⋯ = { left := x, right := z, hom := CategoryTheory.CategoryStruct.comp f g }

theorem Quiver.Total.comp_congr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {a a' b b' : Total C} (ha : a = a') (hb : b = b') (h : a.right = b.left) (h' : a'.right = b'.left) : a.comp b h = a'.comp b' h'

The composite of total arrows depends only on the arrows, not on the proof that they are composable.

theorem Quiver.Total.mk_homOfEq_comp_homOfEq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (a b : Total C) {y z w : C} (hy : a.left = y) (hz : a.right = z) (hz' : b.left = z) (hw : b.right = w) : { left := y, right := w, hom := CategoryTheory.CategoryStruct.comp (homOfEq a.hom hy hz) (homOfEq b.hom hz' hw) } = a.comp b ⋯

Composing two total arrows read as morphisms with matching endpoints gives their composite as total arrows.

theorem Quiver.Total.comp_inv_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.IsGroupoid C] (a c : Total C) (h : a.left = c.left) (h' : a.right = ({ left := a.right, right := a.left, hom := CategoryTheory.inv a.hom }.comp c h).left) : a.comp ({ left := a.right, right := a.left, hom := CategoryTheory.inv a.hom }.comp c h) h' = c

Following a by the composite of its inverse with c gives back c.

theorem Quiver.Total.inv_comp_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.IsGroupoid C] (a b : Total C) (h : a.right = b.left) (h' : { left := a.right, right := a.left, hom := CategoryTheory.inv a.hom }.right = (a.comp b h).left) : { left := a.right, right := a.left, hom := CategoryTheory.inv a.hom }.comp (a.comp b h) h' = b

Following the inverse of a by the composite of a with b gives back b.