[Merged by Bors] - feat(CategoryTheory/Galois): definition and characterisation of Galois objects #10215
Conversation
… chrisflav/galois-galois
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
chrisflav
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
blocked-by-math-PR
leanprover-community-mathlib4-bot
removed
the
blocked-by-math-PR
|
This PR/issue depends on: |
| /-- A `PreGaloisCategory` is a `GaloisCategory` if it admits a fibre functor. -/ | ||
| class GaloisCategory (C : Type u₁) [Category.{u₂, u₁} C] | ||
| extends PreGaloisCategory C : Prop where | ||
| hasFibreFunctor : ∃ F : C ⥤ FintypeCat.{w}, Nonempty (PreGaloisCategory.FibreFunctor F) |
There was a problem hiding this comment.
With this definition, GaloisCategory C depends on a universe w that is unrelated to C. I think it would be advisable to replace w by u₂ in this definition. (Hopefully, with this definition, the example of finite G-sets would be a GaloisCategory. Then, in future developments of the API, it could be shown that the existence of a fiber functor C ⥤ FintypeCat.{w} is independent of the universe w.)
There was a problem hiding this comment.
I suppose, we can't write there exists a universe w and a fibre functor F : C ⥤ FintypeCat.{w}? Finite G-sets is a GaloisCategory anyway:
/-- The category of finite `G`-sets is a `GaloisCategory`. -/
instance : GaloisCategory (Action FintypeCat (MonCat.of G)) where
hasFibreFunctor := ⟨Action.forget FintypeCat (MonCat.of G), ⟨inferInstance⟩⟩compiles. I will add it to the other PR, to avoid conflicts.
There was a problem hiding this comment.
Shouldn't all the FintypeCat categories be equivalent? One could add the lemma that a functor F : C ⥤ FintypeCat.{w} is a FibreFunctor if and only if it is so after composing with an equivalence to some other FintypeCat.{w'}.
There was a problem hiding this comment.
I will add it to the other PR, to avoid conflicts.
I accidentally pushed it to this branch and now realized that on the other one, GaloisCategory is not defined yet. So I'll now keep the instance here and when this one is merged, merge master in the other one.
There was a problem hiding this comment.
Shouldn't all the FintypeCat categories be equivalent?
Yes, of course, but this would require a proof, following the pattern you suggested. In this future API, we could introduce the fact that fibre functors behave well with pre/post-composition with an equivalence. (Only the preservesQuotientsByFiniteGroups should require some work as we would may have to change the universes of G.) We would presumably also need a definition like FibreFunctor.ofIso: if F and G are isomorphic functors, and F is a fibre functor, then G also is.
|
|
||
| /-- For a connected object `X` of `C`, the quotient `X / Aut X` is terminal if and only if | ||
| the quotient `F.obj X / Aut X` has exactly one element. -/ | ||
| noncomputable def quotientByAutTerminalEquivUniqueQuotient [GaloisCategory C] |
There was a problem hiding this comment.
There is an issue with the inclusion of variables here as both PreGaloisCategory C and GaloisCategory C are included. Then, I would think that depending on the situation, only PreGaloisCategory or GaloisCategory should be explicitly included in the various definitions in this file.
There was a problem hiding this comment.
I agree, please check if its better now. In theory it would be best if Lean could infer GaloisCategory C from the line [PreGaloisCategory C] (F : C ⥤ FintypeCat.{w}) [FibreFunctor F], but since GaloisCategory C does not depend on F, this won't work I think.
joelriou
removed
the
awaiting-review
joelriou
added
awaiting-author
chrisflav
added
awaiting-review
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
…s objects (#10215) Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor. To allow for a definition that only depends on `C`, contrary to what was said earlier, we introduce a `GaloisCategory` typeclass extending `PreGaloisCategory` that additionally asserts the existence of a fibre functor.
|
Build failed (retrying...): |
…s objects (#10215) Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor. To allow for a definition that only depends on `C`, contrary to what was said earlier, we introduce a `GaloisCategory` typeclass extending `PreGaloisCategory` that additionally asserts the existence of a fibre functor.
|
Build failed (retrying...):
|
|
Canceled. |
|
retrying bors merge |
…s objects (#10215) Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor. To allow for a definition that only depends on `C`, contrary to what was said earlier, we introduce a `GaloisCategory` typeclass extending `PreGaloisCategory` that additionally asserts the existence of a fibre functor. Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…s objects (#10215) Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor. To allow for a definition that only depends on `C`, contrary to what was said earlier, we introduce a `GaloisCategory` typeclass extending `PreGaloisCategory` that additionally asserts the existence of a fibre functor. Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
…s objects (#10215) Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor. To allow for a definition that only depends on `C`, contrary to what was said earlier, we introduce a `GaloisCategory` typeclass extending `PreGaloisCategory` that additionally asserts the existence of a fibre functor. Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Defines Galois objects in a Galois category in a fibre functor independent way, also gives an equivalent characterisation in terms of a fibre functor.
To allow for a definition that only depends on
C, contrary to what was said earlier, we introduce aGaloisCategorytypeclass extendingPreGaloisCategorythat additionally asserts the existence of a fibre functor.SingleObj Min types #10213