-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(category_theory): Glue data #10436
Closed
Changes from 2 commits
Commits
Show all changes
11 commits
Select commit
Hold shift + click to select a range
2f634d8
first commit
erdOne 1702057
fix
erdOne dce0742
added `tactic.apply_instance`
erdOne 6bc5041
fix indentation
erdOne f48afaa
Update src/category_theory/glue_data.lean
erdOne 6eb41be
Apply suggestions from code review
erdOne e5e1bd7
address review comments
erdOne c69a258
add simp lemmas
erdOne 14f6be3
remove `all_goals ... try { ... }`
erdOne 054069c
renamed stuff
erdOne a98621b
Update src/category_theory/glue_data.lean
erdOne File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,201 @@ | ||
/- | ||
Copyright (c) 2021 Andrew Yang. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Andrew Yang | ||
-/ | ||
import tactic.elementwise | ||
import category_theory.limits.shapes.multiequalizer | ||
import category_theory.limits.constructions.epi_mono | ||
|
||
/-! | ||
# Gluing data | ||
|
||
We define `glue_data` as a family of data needed to glue topological spaces, schemes, etc. We | ||
provide the API to realize it as a multispan diagram, and also states lemmas about its | ||
interaction with a functor that preserves certain pullbacks. | ||
|
||
-/ | ||
|
||
noncomputable theory | ||
|
||
open category_theory.limits | ||
namespace category_theory | ||
|
||
universes v u₁ u₂ | ||
|
||
variables (C : Type u₁) [category.{v} C] {C' : Type u₂} [category.{v} C'] | ||
|
||
/-- | ||
A family of gluing data consists of | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
1. An index type `ι` | ||
2. An object `U i` for each `i : ι`. | ||
3. An object `V i j` for each `i j : ι`. | ||
4. A monomorphism `f i j : V i j ⟶ U i` for each `i j : ι`. | ||
5. A transition map `t i j : V i j ⟶ V j i` for each `i j : ι`. | ||
such that | ||
6. `f i i` is an isomorphism. | ||
7. `t i i` is the identity. | ||
8. The pullback for `f i j` and `f i k` exists. | ||
8. `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through `V j k ×[U j] V j i ⟶ V j i` via some | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
`t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i`. | ||
9. `t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _`. | ||
-/ | ||
@[nolint has_inhabited_instance] | ||
structure glue_data := | ||
(ι : Type v) | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
(U : ι → C) | ||
(V : ι × ι → C) | ||
(f : Π i j, V (i, j) ⟶ U i) | ||
(f_mono : ∀ i j, mono (f i j) . tactic.apply_instance) | ||
(f_has_pullback : ∀ i j k, has_pullback (f i j) (f i k) . tactic.apply_instance) | ||
jcommelin marked this conversation as resolved.
Show resolved
Hide resolved
|
||
(f_id : ∀ i, is_iso (f i i)) | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
(t : Π i j, V (i, j) ⟶ V (j, i)) | ||
(t_id : ∀ i, t i i = 𝟙 _) | ||
(t' : Π i j k, pullback (f i j) (f i k) ⟶ pullback (f j k) (f j i)) | ||
(t_fac : ∀ i j k, t' i j k ≫ pullback.snd = pullback.fst ≫ t i j) | ||
(cocycle : ∀ i j k , t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _) | ||
|
||
attribute [simp] glue_data.t_id | ||
attribute [instance] glue_data.f_id glue_data.f_mono glue_data.f_has_pullback | ||
attribute [reassoc] glue_data.t_fac glue_data.cocycle | ||
|
||
namespace glue_data | ||
|
||
variables {C} (D : glue_data C) | ||
|
||
@[simp] lemma t'_iij (i j : D.ι) : D.t' i i j = (pullback_symmetry _ _).hom := | ||
begin | ||
have eq₁ := D.t_fac i i j, | ||
have eq₂ := (is_iso.eq_comp_inv (D.f i i)).mpr (@pullback.condition _ _ _ _ _ _ (D.f i j) _), | ||
rw [D.t_id, category.comp_id, eq₂] at eq₁, | ||
have eq₃ := (is_iso.eq_comp_inv (D.f i i)).mp eq₁, | ||
rw [category.assoc, ←pullback.condition, ←category.assoc] at eq₃, | ||
exact mono.right_cancellation _ _ | ||
((mono.right_cancellation _ _ eq₃).trans (pullback_symmetry_hom_comp_fst _ _).symm) | ||
end | ||
|
||
lemma t'_jii (i j : D.ι) : D.t' j i i = pullback.fst ≫ D.t j i ≫ inv pullback.snd := | ||
by { rw [←category.assoc, ←D.t_fac], simp } | ||
|
||
lemma t'_iji (i j : D.ι) : D.t' i j i = pullback.fst ≫ D.t i j ≫ inv pullback.snd := | ||
by { rw [←category.assoc, ←D.t_fac], simp } | ||
|
||
@[simp, reassoc, elementwise] lemma t_inv (i j : D.ι) : | ||
D.t i j ≫ D.t j i = 𝟙 _ := | ||
begin | ||
have eq : (pullback_symmetry (D.f i i) (D.f i j)).hom = pullback.snd ≫ inv pullback.fst, | ||
{ simp }, | ||
have := D.cocycle i j i, | ||
rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this, | ||
simp only [category.assoc, is_iso.inv_hom_id_assoc] at this, | ||
rw [←is_iso.eq_inv_comp, ←category.assoc, is_iso.comp_inv_eq] at this, | ||
simpa using this, | ||
end | ||
|
||
lemma t'_inv (i j k : D.ι) : D.t' i j k ≫ (pullback_symmetry _ _).hom ≫ | ||
D.t' j i k ≫ (pullback_symmetry _ _).hom = 𝟙 _ := | ||
begin | ||
rw ← cancel_mono (pullback.fst : pullback (D.f i j) (D.f i k) ⟶ _), | ||
simp [t_fac, t_fac_assoc] | ||
end | ||
|
||
instance t_is_iso (i j : D.ι) : is_iso (D.t i j) := | ||
⟨⟨D.t j i, D.t_inv _ _, D.t_inv _ _⟩⟩ | ||
|
||
instance t'_is_iso (i j k : D.ι) : is_iso (D.t' i j k) := | ||
⟨⟨D.t' j k i ≫ D.t' k i j, D.cocycle _ _ _, (by simpa using D.cocycle _ _ _)⟩⟩ | ||
|
||
@[reassoc] | ||
lemma t'_comp_eq_pullback_symmetry (i j k : D.ι) : | ||
D.t' j k i ≫ D.t' k i j = (pullback_symmetry _ _).hom ≫ | ||
D.t' j i k ≫ (pullback_symmetry _ _).hom := | ||
begin | ||
transitivity inv (D.t' i j k), | ||
{ exact is_iso.eq_inv_of_hom_inv_id (D.cocycle _ _ _) }, | ||
{ rw ← cancel_mono (pullback.fst : pullback (D.f i j) (D.f i k) ⟶ _), | ||
simp [t_fac, t_fac_assoc] } | ||
end | ||
|
||
/-- (Implementation) The disjoint union of `U i`. -/ | ||
def sigma_opens [has_coproduct D.U] : C := ∐ D.U | ||
|
||
/-- (Implementation) The diagram to take colimit of. -/ | ||
def diagram : multispan_index C := | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
{ L := D.ι × D.ι, R := D.ι, | ||
fst_from := _root_.prod.fst, snd_from := _root_.prod.snd, | ||
left := D.V, right := D.U, | ||
fst := λ ⟨i, j⟩, D.f i j, | ||
snd := λ ⟨i, j⟩, D.t i j ≫ D.f j i } | ||
|
||
section | ||
|
||
variable [has_multicoequalizer D.diagram] | ||
|
||
/-- The glued topological space given a family of gluing data. -/ | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
def glued : C := multicoequalizer D.diagram | ||
|
||
/-- The map `D.U i ⟶ D.glued` for each `i`. -/ | ||
def imm (i : D.ι) : D.U i ⟶ D.glued := | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
multicoequalizer.π D.diagram i | ||
|
||
@[simp, elementwise] | ||
lemma glue_condition (i j : D.ι) : | ||
D.t i j ≫ D.f j i ≫ D.imm j = D.f i j ≫ D.imm i := | ||
(category.assoc _ _ _).symm.trans (multicoequalizer.condition D.diagram ⟨i, j⟩).symm | ||
|
||
variables [has_colimits C] | ||
|
||
/-- The projection `∐ D.U ⟶ D.glued` given by the colimit. -/ | ||
def π : D.sigma_opens ⟶ D.glued := multicoequalizer.sigma_π D.diagram | ||
|
||
instance π_epi : epi D.π := by { unfold π, apply_instance } | ||
|
||
end | ||
|
||
variables (F : C ⥤ C') [H : ∀ i j k, preserves_limit (cospan (D.f i j) (D.f i k)) F] | ||
|
||
include H | ||
|
||
instance (i j k : D.ι) : has_pullback (F.map (D.f i j)) (F.map (D.f i k)) := | ||
⟨⟨⟨_, is_limit_of_has_pullback_of_preserves_limit F (D.f i j) (D.f i k)⟩⟩⟩ | ||
|
||
/-- A functor that preserves the pullbacks of `f i j` and `f i k` can map a family of glue data. -/ | ||
def map_glue_data : | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
glue_data C' := | ||
{ ι := D.ι, | ||
U := λ i, F.obj (D.U i), | ||
V := λ i, F.obj (D.V i), | ||
f := λ i j, F.map (D.f i j), | ||
f_mono := λ i j, category_theory.preserves_mono F (D.f i j), | ||
f_id := λ i, infer_instance, | ||
t := λ i j, F.map (D.t i j), | ||
t_id := λ i, by { rw D.t_id i, simp }, | ||
t' := λ i j k, (preserves_pullback.iso F (D.f i j) (D.f i k)).inv ≫ | ||
F.map (D.t' i j k) ≫ (preserves_pullback.iso F (D.f j k) (D.f j i)).hom, | ||
t_fac := λ i j k, by simpa [iso.inv_comp_eq] using congr_arg (λ f, F.map f) (D.t_fac i j k), | ||
cocycle := λ i j k, by simp only [category.assoc, iso.hom_inv_id_assoc, ← functor.map_comp_assoc, | ||
D.cocycle, iso.inv_hom_id, category_theory.functor.map_id, category.id_comp] } | ||
|
||
/-- | ||
The diagram of the image of a `glue_data` under a functor `F` is naturally isomorphic to the | ||
original diagram of the `glue_data` via `F`. | ||
-/ | ||
def diagram_iso : D.diagram.multispan ⋙ F ≅ (D.map_glue_data F).diagram.multispan := | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
nat_iso.of_components | ||
(λ x, match x with | ||
| walking_multispan.left a := iso.refl _ | ||
| walking_multispan.right b := iso.refl _ | ||
end) | ||
(begin | ||
rintros (⟨_,_⟩|b) _ (_|_|_), | ||
all_goals | ||
{ try { erw category.comp_id }, | ||
try { erw category.id_comp }, | ||
try { erw functor.map_id }, | ||
try { erw functor.map_comp }, | ||
refl }, | ||
erdOne marked this conversation as resolved.
Show resolved
Hide resolved
|
||
end) | ||
|
||
end glue_data | ||
|
||
end category_theory |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have the vague feeling that this should instead be rephrased using coverings in a Grothendieck topology? Does that make sense? I haven't thought hard about this.
Instead of gluing objects in a
glue_data
, isn't the more general theorem something like: if a sheaf for a suitable topology is locally representable, then it is globally representable?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The thing is that we do not have the glued space to take cover of in most of my use cases.
The statement you mentioned seems to me to be closer to the comparison lemma (we can glue sheaves on a cover that is somehow dense enough).