Structure CategoryTheory.PreGaloisCategory.PointedGaloisObject

Modification history

2024-09-12 17:39

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

feat(CategoryTheory/Galois): generalize transitivity to arbitrary universes (#16664) …

Modified CategoryTheory.PreGaloisCategory.PointedGaloisObject View on Github →

2024-05-14 10:23

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

feat(CategoryTheory/Galois): prorepresentability of fiber functors (#12839) …

Added CategoryTheory.PreGaloisCategory.PointedGaloisObject View on Github →