Skip to content

Commit ce0c89b

Browse files
joelrioujoelriou
committed
feat: port CategoryTheory.GradedObject (#3342)
1 parent d462f81 commit ce0c89b

File tree

4 files changed

+256
-5
lines changed

4 files changed

+256
-5
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -380,6 +380,7 @@ import Mathlib.CategoryTheory.Functor.Hom
380380
import Mathlib.CategoryTheory.Functor.InvIsos
381381
import Mathlib.CategoryTheory.Functor.ReflectsIso
382382
import Mathlib.CategoryTheory.GlueData
383+
import Mathlib.CategoryTheory.GradedObject
383384
import Mathlib.CategoryTheory.Grothendieck
384385
import Mathlib.CategoryTheory.Groupoid
385386
import Mathlib.CategoryTheory.Groupoid.Basic

‎Mathlib/CategoryTheory/GradedObject.lean‎

Lines changed: 250 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,250 @@
1+
/-
2+
Copyright (c) 2020 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
6+
! This file was ported from Lean 3 source module category_theory.graded_object
7+
! leanprover-community/mathlib commit 6876fa15e3158ff3e4a4e2af1fb6e1945c6e8803
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Algebra.GroupPower.Lemmas
12+
import Mathlib.CategoryTheory.Pi.Basic
13+
import Mathlib.CategoryTheory.Shift.Basic
14+
import Mathlib.CategoryTheory.ConcreteCategory.Basic
15+
16+
/-!
17+
# The category of graded objects
18+
19+
For any type `β`, a `β`-graded object over some category `C` is just
20+
a function `β → C` into the objects of `C`.
21+
We put the "pointwise" category structure on these, as the non-dependent specialization of
22+
`CategoryTheory.Pi`.
23+
24+
We describe the `comap` functors obtained by precomposing with functions `β → γ`.
25+
26+
As a consequence a fixed element (e.g. `1`) in an additive group `β` provides a shift
27+
functor on `β`-graded objects
28+
29+
When `C` has coproducts we construct the `total` functor `GradedObject β C ⥤ C`,
30+
show that it is faithful, and deduce that when `C` is concrete so is `GradedObject β C`.
31+
-/
32+
33+
34+
open CategoryTheory.Limits
35+
36+
namespace CategoryTheory
37+
38+
universe w v u
39+
40+
/-- A type synonym for `β → C`, used for `β`-graded objects in a category `C`. -/
41+
def GradedObject (β : Type w) (C : Type u) : Type max w u :=
42+
β → C
43+
#align category_theory.graded_object CategoryTheory.GradedObject
44+
45+
-- Satisfying the inhabited linter...
46+
instance inhabitedGradedObject (β : Type w) (C : Type u) [Inhabited C] :
47+
Inhabited (GradedObject β C) :=
48+
⟨fun _ => Inhabited.default⟩
49+
#align category_theory.inhabited_graded_object CategoryTheory.inhabitedGradedObject
50+
51+
-- `s` is here to distinguish type synonyms asking for different shifts
52+
/-- A type synonym for `β → C`, used for `β`-graded objects in a category `C`
53+
with a shift functor given by translation by `s`.
54+
-/
55+
@[nolint unusedArguments]
56+
abbrev GradedObjectWithShift {β : Type w} [AddCommGroup β] (_ : β) (C : Type u) : Type max w u :=
57+
GradedObject β C
58+
#align category_theory.graded_object_with_shift CategoryTheory.GradedObjectWithShift
59+
60+
namespace GradedObject
61+
62+
variable {C : Type u} [Category.{v} C]
63+
64+
@[simps!]
65+
instance categoryOfGradedObjects (β : Type w) : Category.{max w v} (GradedObject β C) :=
66+
CategoryTheory.pi fun _ => C
67+
#align category_theory.graded_object.category_of_graded_objects CategoryTheory.GradedObject.categoryOfGradedObjects
68+
69+
-- porting note: added to ease automation
70+
@[ext]
71+
lemma hom_ext {X Y : GradedObject β C} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g := by
72+
funext
73+
apply h
74+
75+
/-- The projection of a graded object to its `i`-th component. -/
76+
@[simps]
77+
def eval {β : Type w} (b : β) : GradedObject β C ⥤ C where
78+
obj X := X b
79+
map f := f b
80+
#align category_theory.graded_object.eval CategoryTheory.GradedObject.eval
81+
82+
section
83+
84+
variable (C)
85+
86+
-- porting note: added to ease the port
87+
/-- Pull back an `I`-graded object in `C` to a `J`-graded object along a function `J → I`. -/
88+
abbrev comap {I J : Type _} (h : J → I) : GradedObject I C ⥤ GradedObject J C :=
89+
Pi.comap (fun _ => C) h
90+
91+
-- porting note: added to ease the port, this is a special case of `Functor.eqToHom_proj`
92+
@[simp]
93+
theorem eqToHom_proj {x x' : GradedObject I C} (h : x = x') (i : I) :
94+
(eqToHom h : x ⟶ x') i = eqToHom (Function.funext_iff.mp h i) := by
95+
subst h
96+
rfl
97+
98+
/-- The natural isomorphism comparing between
99+
pulling back along two propositionally equal functions.
100+
-/
101+
@[simps]
102+
def comapEq {β γ : Type w} {f g : β → γ} (h : f = g) : comap C f ≅ comap C g where
103+
hom := { app := fun X b => eqToHom (by dsimp ; simp only [h]) }
104+
inv := { app := fun X b => eqToHom (by dsimp ; simp only [h]) }
105+
#align category_theory.graded_object.comap_eq CategoryTheory.GradedObject.comapEq
106+
107+
theorem comapEq_symm {β γ : Type w} {f g : β → γ} (h : f = g) :
108+
comapEq C h.symm = (comapEq C h).symm := by aesop_cat
109+
#align category_theory.graded_object.comap_eq_symm CategoryTheory.GradedObject.comapEq_symm
110+
111+
theorem comapEq_trans {β γ : Type w} {f g h : β → γ} (k : f = g) (l : g = h) :
112+
comapEq C (k.trans l) = comapEq C k ≪≫ comapEq C l := by aesop_cat
113+
#align category_theory.graded_object.comap_eq_trans CategoryTheory.GradedObject.comapEq_trans
114+
115+
@[simp]
116+
theorem eqToHom_apply {β : Type w} {X Y : ∀ _ : β, C} (h : X = Y) (b : β) :
117+
(eqToHom h : X ⟶ Y) b = eqToHom (by rw [h]) := by
118+
subst h
119+
rfl
120+
#align category_theory.graded_object.eq_to_hom_apply CategoryTheory.GradedObject.eqToHom_apply
121+
122+
/-- The equivalence between β-graded objects and γ-graded objects,
123+
given an equivalence between β and γ.
124+
-/
125+
@[simps]
126+
def comapEquiv {β γ : Type w} (e : β ≃ γ) : GradedObject β C ≌ GradedObject γ C where
127+
functor := comap C (e.symm : γ → β)
128+
inverse := comap C (e : β → γ)
129+
counitIso :=
130+
(Pi.comapComp (fun _ => C) _ _).trans (comapEq C (by ext ; simp))
131+
unitIso :=
132+
(comapEq C (by ext ; simp)).trans (Pi.comapComp _ _ _).symm
133+
functor_unitIso_comp X := by aesop_cat
134+
#align category_theory.graded_object.comap_equiv CategoryTheory.GradedObject.comapEquiv
135+
136+
-- See note [dsimp, simp].
137+
end
138+
139+
instance hasShift {β : Type _} [AddCommGroup β] (s : β) : HasShift (GradedObjectWithShift s C) ℤ :=
140+
hasShiftMk _ _
141+
{ F := fun n => comap C fun b : β => b + n • s
142+
zero := comapEq C (by aesop_cat) ≪≫ Pi.comapId β fun _ => C
143+
add := fun m n => comapEq C (by ext ; dsimp ; rw [add_comm m n, add_zsmul, add_assoc]) ≪≫
144+
(Pi.comapComp _ _ _).symm }
145+
#align category_theory.graded_object.has_shift CategoryTheory.GradedObject.hasShift
146+
147+
@[simp]
148+
theorem shiftFunctor_obj_apply {β : Type _} [AddCommGroup β] (s : β) (X : β → C) (t : β) (n : ℤ) :
149+
(shiftFunctor (GradedObjectWithShift s C) n).obj X t = X (t + n • s) :=
150+
rfl
151+
#align category_theory.graded_object.shift_functor_obj_apply CategoryTheory.GradedObject.shiftFunctor_obj_apply
152+
153+
@[simp]
154+
theorem shiftFunctor_map_apply {β : Type _} [AddCommGroup β] (s : β)
155+
{X Y : GradedObjectWithShift s C} (f : X ⟶ Y) (t : β) (n : ℤ) :
156+
(shiftFunctor (GradedObjectWithShift s C) n).map f t = f (t + n • s) :=
157+
rfl
158+
#align category_theory.graded_object.shift_functor_map_apply CategoryTheory.GradedObject.shiftFunctor_map_apply
159+
160+
instance [HasZeroMorphisms C] (β : Type w) (X Y : GradedObject β C) :
161+
Zero (X ⟶ Y) := ⟨fun _ => 0⟩
162+
163+
@[simp]
164+
theorem zero_apply [HasZeroMorphisms C] (β : Type w) (X Y : GradedObject β C) (b : β) :
165+
(0 : X ⟶ Y) b = 0 :=
166+
rfl
167+
#align category_theory.graded_object.zero_apply CategoryTheory.GradedObject.zero_apply
168+
169+
instance hasZeroMorphisms [HasZeroMorphisms C] (β : Type w) :
170+
HasZeroMorphisms.{max w v} (GradedObject β C) where
171+
#align category_theory.graded_object.has_zero_morphisms CategoryTheory.GradedObject.hasZeroMorphisms
172+
173+
section
174+
175+
open ZeroObject
176+
177+
instance hasZeroObject [HasZeroObject C] [HasZeroMorphisms C] (β : Type w) :
178+
HasZeroObject.{max w v} (GradedObject β C) := by
179+
refine' ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => _⟩⟩, fun X =>
180+
⟨⟨⟨fun b => 0⟩, fun f => _⟩⟩⟩⟩ <;> aesop_cat
181+
#align category_theory.graded_object.has_zero_object CategoryTheory.GradedObject.hasZeroObject
182+
183+
end
184+
185+
end GradedObject
186+
187+
namespace GradedObject
188+
189+
-- The universes get a little hairy here, so we restrict the universe level for the grading to 0.
190+
-- Since we're typically interested in grading by ℤ or a finite group, this should be okay.
191+
-- If you're grading by things in higher universes, have fun!
192+
variable (β : Type)
193+
194+
variable (C : Type u) [Category.{v} C]
195+
196+
variable [HasCoproducts.{0} C]
197+
198+
section
199+
200+
--attribute [local tidy] tactic.discrete_cases
201+
202+
/-- The total object of a graded object is the coproduct of the graded components.
203+
-/
204+
noncomputable def total : GradedObject β C ⥤ C where
205+
obj X := ∐ fun i : β => X i
206+
map f := Limits.Sigma.map fun i => f i
207+
map_id := fun X => by
208+
dsimp
209+
ext
210+
simp only [ι_colimMap, Discrete.natTrans_app, Category.comp_id]
211+
apply Category.id_comp
212+
#align category_theory.graded_object.total CategoryTheory.GradedObject.total
213+
214+
end
215+
216+
variable [HasZeroMorphisms C]
217+
218+
/--
219+
The `total` functor taking a graded object to the coproduct of its graded components is faithful.
220+
To prove this, we need to know that the coprojections into the coproduct are monomorphisms,
221+
which follows from the fact we have zero morphisms and decidable equality for the grading.
222+
-/
223+
instance : Faithful (total β C) where
224+
map_injective {X Y} f g w := by
225+
ext i
226+
replace w := Sigma.ι (fun i : β => X i) i ≫= w
227+
erw [colimit.ι_map, colimit.ι_map] at w
228+
simp at *
229+
exact Mono.right_cancellation _ _ w
230+
231+
end GradedObject
232+
233+
namespace GradedObject
234+
235+
noncomputable section
236+
237+
variable (β : Type)
238+
239+
variable (C : Type (u + 1)) [LargeCategory C] [ConcreteCategory C] [HasCoproducts.{0} C]
240+
[HasZeroMorphisms C]
241+
242+
instance : ConcreteCategory (GradedObject β C) where Forget := total β C ⋙ forget C
243+
244+
instance : HasForget₂ (GradedObject β C) C where forget₂ := total β C
245+
246+
end
247+
248+
end GradedObject
249+
250+
end CategoryTheory

‎Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,9 +55,9 @@ class HasZeroMorphisms where
5555
/-- Every morphism space has zero -/
5656
[Zero : ∀ X Y : C, Zero (X ⟶ Y)]
5757
/-- `f` composed with `0` is `0` -/
58-
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) := by aesop
58+
comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) := by aesop_cat
5959
/-- `0` composed with `f` is `0` -/
60-
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) := by aesop
60+
zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) := by aesop_cat
6161
#align category_theory.limits.has_zero_morphisms CategoryTheory.Limits.HasZeroMorphisms
6262
#align category_theory.limits.has_zero_morphisms.comp_zero' CategoryTheory.Limits.HasZeroMorphisms.comp_zero
6363
#align category_theory.limits.has_zero_morphisms.zero_comp' CategoryTheory.Limits.HasZeroMorphisms.zero_comp

‎Mathlib/CategoryTheory/Shift/Basic.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -77,13 +77,13 @@ structure ShiftMkCore where
7777
assoc_hom_app : ∀ (m₁ m₂ m₃ : A) (X : C),
7878
(add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
7979
eqToHom (by dsimp; rw [add_assoc]) ≫ (add m₁ (m₂ + m₃)).hom.app X ≫
80-
(add m₂ m₃).hom.app ((F m₁).obj X)
80+
(add m₂ m₃).hom.app ((F m₁).obj X) := by aesop_cat
8181
/-- compatibility with the left addition with 0 -/
8282
zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X =
83-
eqToHom (by dsimp; rw [zero_add]) ≫ (F n).map (zero.inv.app X)
83+
eqToHom (by dsimp; rw [zero_add]) ≫ (F n).map (zero.inv.app X) := by aesop_cat
8484
/-- compatibility with the right addition with 0 -/
8585
add_zero_hom_app : ∀ (n : A) (X : C), (add n 0).hom.app X =
86-
eqToHom (by dsimp; rw [add_zero]) ≫ zero.inv.app ((F n).obj X)
86+
eqToHom (by dsimp; rw [add_zero]) ≫ zero.inv.app ((F n).obj X) := by aesop_cat
8787
#align category_theory.shift_mk_core CategoryTheory.ShiftMkCore
8888

8989
namespace ShiftMkCore

0 commit comments

Comments
 (0)