Galois categories

Stream: Is there code for X?

[Christian Merten]

Are there Galois categories (in the sense of SGA1) in mathlib4?

[Adam Topaz]

No

[Christian Merten]

What do you think would be the best approach defininig them? I was thinking of going the stacks project way, i.e. defining a galois category to be a pair of a category C and a functor F from C to Sets satisfiying some axioms and then show the fundamental theorem. The SGA1 way would be to define a galois category as a category equivalent to Finite-G-Sets for some profinite group G.

[Kevin Buzzard]

The definition should be the category and functor (the "constructive definition") and then you should make a definition of the profinite group attached to the Galois category and then prove the theorem that it's isomorphic to the reps of that group.

One nice extra twist which you don't see in set theory is that in Lean you will be able to let C be in Type u and the target of the functor being Type v and then you can see whether universes always match up in your equivalence.

[Kevin Buzzard]

I agree that this would be a really cool project. Please feel free to post some tentative definitions before you leap into proving theorems -- if you get the definitions right then the theorems get easier to prove.

[Christian Merten]

I suppose the advantage of the SGA1 definition is, that it does not fix a fundamental functor. So in the notation of SGA1 a galois category is a category satisfying some axioms (G1)-(G3) such that there exists a fundemantal functor satisfying some more axioms (G4)-(G6). This lets you naturally speak of different fundamental functors of one galois category. The stacks project definition (and if I understand you correctly also your suggestion) says a galois category is a category satisfying axioms with a fixed fundamental functor.

[Adam Topaz]

But it does...

[Adam Topaz]

I mean the SGA definition does implicitly fix a fibre functor, namely the composition of the equivalence with the forgetful functor from G-FSet to FSet.

[Adam Topaz]

I don't know of a definition in the literature that does not somehow fix a fibre functor (the only variant I can think of that does this is more sophisticated involving some ideas from etale homotopy theory which are beyond what's currently possible to formalize)

[Adam Topaz]

wait I'm confused. What's the SGA definition?

[Adam Topaz]

above you said that it uses an equivalence with G-sets.

[Christian Merten]

The SGA definition is the following: A galois category is a category C equivalent to the category of Finite-G-Sets where G is a profinite group. I interpret this in the sense that the equivalence is not fixed, i.e. it is just an existence claim.

[Christian Merten]

They say: (ad hoc translation from french) "a category C is galois if and only if it satisfies axioms (G1) - (G3) and if there exists a functor from C to finite Sets satisfying axioms (G4)-(G6)"

[Adam Topaz]

Ok I see what you meant.

[Adam Topaz]

But then you can just claim the existence of a fibre functor with the Stack's definition.

[Christian Merten]

Yes, I was just asking you on your opinion whether a galois category should be a pair of a category and a fibre functor or just a category for which a fibre functor exists.

[Adam Topaz]

I think what Kevin says makes good sense. Take a category C with a functor F satisfying some axioms. Then define G as Aut(F), show that G is profinite, and then assert that the canonical functor is an equivalence.

[Adam Topaz]

I guess there is a canonical functor from C to Aut(F)-FSets.

[Adam Topaz]

And the assertion that this is an equivalence is actually a Prop if you use the fully-faithful essentially surjective approach.

[Christian Merten]

Adam Topaz said:

I guess there is a canonical functor from C to Aut(F)-FSets.

Yes, induced by F.

[Christian Merten]

Adam Topaz said:

And the assertion that this is an equivalence is actually a Prop if you use the fully-faithful essentially surjective approach.

I'll see, SGA1 constructs an actual quasi-inverse.

[Christian Merten]

Are there continuous group actions somewhere, i.e. G actions on a category C where for every X : C the canonical map G × X → X is continuous when X is equipped with the discrete topology?

[Kevin Buzzard]

@Amelia Livingston did you run into this with Galois cohomology?

[Christian Merten]

Searching for Galois cohomology was also my first idea, but that is not in mathlib right?

[Kevin Buzzard]

That's right -- Amelia has not yet begun to PR her work in that area.

[Adam Topaz]

We have docs#ContinuousSMul

[Adam Topaz]

I think that's about all we have right now.

[Joël Riou]

I would say that the most important mathematical result to formalize is not the definition of Galois categories, but it is proving the main result in SGA 1 V 4 Conditions axiomatiques d'une théorie de Galois which are axioms in order to turn a functor to finite sets into an equivalence of categories with finite G-sets (as it was mentionned above). Then, eventually, we may have a debate about whether Galois categories should be equipped with a fibre functor or not...

[Christian Merten]

I'll wait then if Amelia answers, because I suppose she probably has then already defined the category of continuous actions. So my current (wrong) definition (without the continuity) is the following:

import Mathlib.CategoryTheory.Functor.Hom
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
import Mathlib.CategoryTheory.Limits.Shapes.Products
import Mathlib.CategoryTheory.Limits.Preserves.Finite
import Mathlib.Topology.Algebra.Group.Basic
import Mathlib.RepresentationTheory.Action
import Mathlib.CategoryTheory.FintypeCat

universe w v₁ u₁ u₂

open CategoryTheory Limits

class ConnectedObject (C : Type u₁) [Category.{v₁} C] (X : C) where
  notInitial : IsInitial X → False
  noTrivialComponent (Y : C) (i : Y ⟶ X) [Mono i] : ¬ IsIso i → IsInitial Y

/- Stacks Project Definition 0BMY -/
class GaloisCategory (C : Type u₁) [Category.{v₁} C] (F : C ⥤ Type v₁) where
  -- properties of C
  hasFiniteLimits : HasFiniteLimits C
  hasFiniteColimits : HasFiniteColimits C
  asFiniteCoproductOfConnected (X : C) :
    ∃ (ι : Type w) (_ : Fintype ι) (f : ι → C) (_ : ∀ i, ConnectedObject C (f i)),
    IsIsomorphic X (∐ f)

  -- properties of F
  imageFinite (X : C) : Fintype (F.obj X)
  reflectsIsos : ReflectsIsomorphisms F
  leftExact : PreservesFiniteLimits F
  rightExact : PreservesFiniteColimits F

variable {C : Type v₁} [Category.{v₁} C] (F : C ⥤ Type v₁) [GaloisCategory C F]

instance (X : C) : Fintype (F.obj X) := GaloisCategory.imageFinite X

def fundamentalGroup (F : C ⥤ Type v₁) : Type (max v₁ v₁) := Aut F

-- inherit group instance from automorphism group
instance : Group (fundamentalGroup F) := by
  show Group (Aut F)
  exact inferInstance

-- the fundamental group is a profinite group
instance : TopologicalSpace (fundamentalGroup F) := sorry
instance : TopologicalGroup (fundamentalGroup F) := sorry
instance : CompactSpace (fundamentalGroup F) := sorry
instance : TotallyDisconnectedSpace (fundamentalGroup F) := sorry
instance : T2Space (fundamentalGroup F) := sorry

abbrev πTypes := (Action (FintypeCat.{v₁}) (MonCat.of (fundamentalGroup F)))

def fibreFunctor : C ⥤ πTypes F where
  obj X := {
    V := FintypeCat.of (F.obj X)
    ρ := MonCat.ofHom {
      toFun := fun (g : fundamentalGroup F) ↦ g.hom.app X
      map_one' := rfl
      map_mul' := by aesop
    }
  }
  map f := {
    hom := F.map f
    comm := by
      intro g
      exact symm <| g.hom.naturality f
  }

example : fibreFunctor F ⋙ forget (πTypes F) = F := rfl

theorem fundamental : IsEquivalence (fibreFunctor F) := sorry

[Christian Merten]

I adopted the stronger definition of Galois categories of the stacks project, because this makes it simpler to state (in the end, the definition is equivalent to the SGA definition). In particular I ask for all finite limits and finite colimits instead of only asking for fibre products, finite sums and quotients by finite automorphism groups. Do you think this is fine or should we go with the SGA definition (Lenstra in Galois theory for schemes also follows the SGA definition)?

[Joël Riou]

There is a comment at the end of SGA 1 V 4 saying that the proof of the main theorm is easier assuming stronger axioms. However, In the case of the étale fundamental group, the verification of the weaker axioms is much easier. I think it would be a problem if we end up with a formalization of Galois categories that cannot eventually be applied to the étale fundamental group, then I think that the formalization should rely on the weaker axioms. (Eventually, we may also have an alternate constructor taking stronger axioms as assumptions...)

[Christian Merten]

I agree, but the stacks project also shows that the category of finite etale morphisms of a connected scheme form a galois category in the stronger sense (0BNB), so I don't know if this is actually a big restriction.

[Joël Riou]

I prefer the SGA 1 axioms because there are slightly more geometric (with the stress of the action of a finite group G on a scheme X and the study of the quotient X/G), but the proof in the stacks project does not seem to use too much material, so that both ways should be ok.

[Christian Merten]

I typed the SGA definition (actually the one in Lenstra which is slightly different since it does not talk about strict epimorphisms):

def quotientDiagram {C : Type u} [Category.{v, u} C] (X : C) (G : Subgroup (Aut X)) : C ⥤ Type v where
  obj Y := { f : X ⟶ Y | ∀ σ : G, f = (σ : Aut X).hom ≫ f }
  map ϕ := by
    intro ⟨f, hf⟩
    have h (σ : G) : f ≫ ϕ = (σ : Aut X).hom ≫ f ≫ ϕ := by rw [←Category.assoc, ←hf σ]
    exact ⟨f ≫ ϕ, h⟩

noncomputable def quotientByAutGroup {C : Type u} [Category.{v, u} C] (X : C) (G : Subgroup (Aut X))
    [Corepresentable (quotientDiagram X G)] : C :=
  coreprX (quotientDiagram X G)

def coyonedaOfFofQuot {C : Type u} [Category.{v, u} C] (X : C) (F : C ⥤ Type w) (G : Subgroup (Aut X))
    [Corepresentable (quotientDiagram X G)] : Type w ⥤ Type w :=
  coyoneda.obj (Opposite.op <| F.obj <| quotientByAutGroup X G)

/- Lenstra -/
class GaloisCategory (C : Type u) [Category.{v, u} C] (F : C ⥤ Type w) where
  -- (G0)
  imageFinite (X : C) : Fintype (F.obj X)

  -- (G1)
  hasTerminalObject : HasTerminal C
  hasPullbacks : HasPullbacks C
  -- (G2)
  hasFiniteCoproducts : HasFiniteCoproducts C
  -- quotient by finite group of automorphisms
  hasQuotientsByFiniteAutGroups {X : C} (G : Subgroup (Aut X)) [Finite G] :
    Corepresentable (quotientDiagram X G)

  -- (G3)
  epiMonoFactorisation {X Z : C} (f : X ⟶ Z) : ∃ (Y : C) (p : X ⟶ Y) (i : Y ⟶ Z),
    Epi p ∧ Mono i ∧ p ≫ i = f
  monoInducesIsoOnDirectSummand {X Y : C} (i : X ⟶ Y) [Mono i] : ∃ (Z : C) (u : Z ⟶ Y)
    (_ : IsColimit (BinaryCofan.mk i u)), True

  -- (G4)
  preservesTerminalObjects: PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F
  preservesPullbacks : PreservesLimitsOfShape WalkingCospan F
  -- (G5)
  preservesFiniteCoproducts : PreservesFiniteCoproducts F
  preservesEpis : Functor.PreservesEpimorphisms F
  preservesQuotientsByFiniteAutGroups {X : C} (G : Subgroup (Aut X)) [Finite G] :
    ∃ (t : coyoneda.obj (Opposite.op <| F.obj <| quotientByAutGroup X G)
           ⟶ quotientDiagram (F.obj X) (Subgroup.map (mapAut X F) G)),
    IsIso t
  -- (G6)
  reflectsIsos : ReflectsIsomorphisms F

I am very unsure about the way I asked for quotients by finite subgroups of the automorphism group. I first wanted to define this as as some HasColimitsOfShape and PreservesColimitsOfShape, but defining the correct index category for this colimit seemed annoying. So I went with the Corepresentable approach. Do you have any thoughts on this?

[Christian Merten]

Also the monoInducesIsoOnDirectSummand seems ugly, is there a better way to formulate this? The issue here is that IsColimit is not a Prop.

[Joël Riou]

I think that Has/PreservesColimitsOfShape would be ok, if you consider colimits indexed by the category BG (I am not sure we have it in mathlib?) for any group G : Type v. (Also, I am not sure these fields absolutely need to be Props: for example PreservesFiniteCoproducts is not a Prop!) It seems that even Grothendieck was not happy with monoInducesIsoOnDirectSummand and was wondering whether this assumption could be removed...

[Christian Merten]

What is the definition of BG?

[Joël Riou]

BG is the category with one object whose endomorphisms identify to G (this also makes sense for a monoid instead of a group). Then, a functor from BG to a category corresponds to an action of G on an object X, and the colimit of this functor is the quotient by the action of G (here, we do not need to assume G injects in the automorphisms of X).

[Christian Merten]

I suppose this: docs#CategoryTheory.SingleObj and docs#CategoryTheory.SingleObj.groupoid is sufficient then?

[Joël Riou]

Yes.

[Scott Morrison]

If someone wants to write the string "BG" into the doc-string for SingleObj that would be great. :-)

[Amelia Livingston]

Christian Merten said:

Are there continuous group actions somewhere, i.e. G actions on a category C where for every X : C the canonical map G × X → X is continuous when X is equipped with the discrete topology?

Sorry for my slow reply - I have defined these but only in Lean 3. I can start porting & tidying it up for PR.

[Christian Merten]

That would be great!

[Christian Merten]

So I decided to go the harder way, i.e. using the SGA definition.

[Christian Merten]

I started to be worried that the typeclasses are not Prop valued, because it makes type class instance inference annoying (I always have to explicitly pass inst : GaloisCategory C F). I suppose making GaloisCategory C F Prop valued is a nightmare, because the only solution I can imagine is formulating everything indirectly, e.g.

preservesFiniteCoproducts : (PreservesFiniteCoproducts F → False) → False

Alternatively I could state the explicit isomorphisms, e.g.

preservesTerminalObjects : IsIsomorphic (F.obj (⊤_ C)) PUnit

But doing this for preservesFiniteCoproducts would mean that deriving things like preservesInitialObject (O : C) (_ : IsInitial O) : IsInitial (F.obj O) is tedious.

Can I somehow circumvent this by helping the typeclass inference algorithm by stating somewhere in the beginning of files that every instance of GaloisCategory C F should just be the one fixed in the beginning?

[Christian Merten]

The same problem arises for ConnectedObject which I initially defined as:

class ConnectedObject {C : Type u} [Category.{v, u} C] (X : C) where
  notInitial : IsInitial X → False
  noTrivialComponent (Y : C) (i : Y ⟶ X) [Mono i] : ¬ IsIso i → IsInitial Y

At some point I need to define the subtype ConnectedObjects of C, which with this definition is:

def ConnectedObjects (C : Type u) [Category{.v, u} C] :=
  { A : C | ∃ (_ : ConnectedObject A), True }

and which "should be"

def ConnectedObjects (C : Type u) [Category.{v, u} C] :=
  { A : C | ConnectedObject A }

So I changed this to:

class ConnectedObject {C : Type u} [Category.{v, u} C] (X : C) : Prop where
  notInitial : IsInitial X → False
  noTrivialComponent (Y : C) (i : Y ⟶ X) [Mono i] :
    ¬ IsIso i → (IsInitial Y → False) → False

which again feels a bit silly. Do you have any suggestions on this? I currently prefer the second version, but I am happy to hear your opinions on this.

[Joël Riou]

Why not the following?

class IsConnectedObject {C : Type*} [Category C] (X : C) : Prop where
  notInitial : ¬ Nonempty (IsInitial X)
  noTrivialComponent (Y : C) (i : Y ⟶ X) [Mono i] (hY : ¬ (Nonempty (IsInitial Y))) : IsIso i

[Christian Merten]

Does the first one actually make the usage easier? ¬ Nonempty (IsInitial X) is just Nonempty (IsInitial X) → False which seems less simple than IsInitial X → False. The second one is certainly an improvement, I think I would still rewrite it as:

noTrivialComponent (Y : C) (i : Y ⟶ X) [Mono i]
  (hY : IsInitial → False) : IsIso i

[Christian Merten]

Christian Merten said:

I started to be worried that the typeclasses are not Prop valued, because it makes type class instance inference annoying (I always have to explicitly pass inst : GaloisCategory C F). I suppose making GaloisCategory C F Prop valued is a nightmare, because the only solution I can imagine is formulating everything indirectly, e.g.

preservesFiniteCoproducts : (PreservesFiniteCoproducts F → False) → False

Alternatively I could state the explicit isomorphisms, e.g.

preservesTerminalObjects : IsIsomorphic (F.obj (⊤_ C)) PUnit

But doing this for preservesFiniteCoproducts would mean that deriving things like preservesInitialObject (O : C) (_ : IsInitial O) : IsInitial (F.obj O) is tedious.

Can I somehow circumvent this by helping the typeclass inference algorithm by stating somewhere in the beginning of files that every instance of GaloisCategory C F should just be the one fixed in the beginning?

I think the main issue preventing instance inference from working properly here is that the first three axioms of GaloisCategory C F don't depend on F, so it can't infer the instance GaloisCategory C F in any statement that does not explicitly involve F. My suggestions is thus to split the definition in two typeclasses:

import Mathlib

open CategoryTheory Limits Functor

/- Lenstra (G1)-(G3) -/
class PreGaloisCategory (C : Type u) [Category.{v, u} C] where
  -- (G1)
  hasTerminalObject : HasTerminal C
  hasPullbacks : HasPullbacks C
  -- (G2)
  hasFiniteCoproducts : HasFiniteCoproducts C
  hasQuotientsByFiniteGroups (G : Type w) [Group G] [Finite G] : HasColimitsOfShape C (SingleObj G ⥤ C)
  -- (G3)
  epiMonoFactorisation {X Z : C} (f : X ⟶ Z) : ∃ (Y : C) (p : X ⟶ Y) (i : Y ⟶ Z),
    Epi p ∧ Mono i ∧ p ≫ i = f
  monoInducesIsoOnDirectSummand {X Y : C} (i : X ⟶ Y) [Mono i] : ∃ (Z : C) (u : Z ⟶ Y)
    (_ : IsColimit (BinaryCofan.mk i u)), True

/- Lenstra (G4)-(G6) -/
class FundamentalFunctor {C : Type u} [Category.{v, u} C] [PreGaloisCategory C] (F : C ⥤ Type w) where
  -- (G0)
  imageFinite (X : C) : Fintype (F.obj X)
  -- (G4)
  preservesTerminalObjects : PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F
  --preservesTerminalObjects : IsIsomorphic (F.obj (⊤_ C)) PUnit
  preservesPullbacks : PreservesLimitsOfShape WalkingCospan F
  -- (G5)
  preservesFiniteCoproducts : PreservesFiniteCoproducts F
  preservesEpis : Functor.PreservesEpimorphisms F
  preservesQuotientsByFiniteGroups (G : Type w) [Group G] [Finite G] :
    PreservesColimitsOfShape (SingleObj G) F
 -- (G6)
  reflectsIsos : ReflectsIsomorphisms F

class ConnectedObject {C : Type u} [Category.{v, u} C] (X : C) : Prop where
  notInitial : IsInitial X → False
  noTrivialComponent (Y : C) (i : Y ⟶ X) [Mono i] : ¬ IsIso i → (IsInitial Y → False) → False

variable {C : Type u} [Category.{v, u} C] [PreGaloisCategory C]

instance hasTerminal : HasTerminal C := PreGaloisCategory.hasTerminalObject
instance hasPullbacks : HasPullbacks C := PreGaloisCategory.hasPullbacks
instance hasFiniteLimits : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
instance hasBinaryProducts  : HasBinaryProducts C := hasBinaryProducts_of_hasTerminal_and_pullbacks C
instance hasEqualizers : HasEqualizers C := hasEqualizers_of_hasPullbacks_and_binary_products

variable {C : Type u} [Category.{v, u} C] {F : C ⥤ Type w} [PreGaloisCategory C] [FundamentalFunctor F]

instance (X : C) : Fintype (F.obj X) := FundamentalFunctor.imageFinite X

instance : PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) F :=
  FundamentalFunctor.preservesTerminalObjects
instance : PreservesLimitsOfShape WalkingCospan F :=
  FundamentalFunctor.preservesPullbacks
instance : PreservesFiniteCoproducts F :=
  FundamentalFunctor.preservesFiniteCoproducts
instance : PreservesColimitsOfShape (Discrete PEmpty.{1}) F :=
  FundamentalFunctor.preservesFiniteCoproducts.preserves PEmpty
instance : ReflectsIsomorphisms F :=
  FundamentalFunctor.reflectsIsos

noncomputable instance preservesFiniteLimits : PreservesFiniteLimits F :=
  preservesFiniteLimitsOfPreservesTerminalAndPullbacks F

def preservesInitialObject (O : C) : IsInitial O → IsInitial (F.obj O) :=
  IsInitial.isInitialObj F O

instance preservesMonomorphisms : PreservesMonomorphisms F :=
  preservesMonomorphisms_of_preservesLimitsOfShape F

As you can see instance inference now works properly and subsequent proofs become way cleaner, because all instances are automatically inferred. What do you think about the split?

[Kevin Buzzard]

FundamentalFunctor presumably isn't a Prop because you used constructive finiteness (Fintype) instead of Finite. I don't know what is best.

[Christian Merten]

I think FundamentalFunctor can't reasonably become a Prop because all the PreservesFiniteCoproducts F etc. are no Props.

[Adam Topaz]

You know that we have the category of finite types, right? docs#FintypeCat I think?

[Adam Topaz]

So you should probably just take your fibre functor to take values in this category

[Adam Topaz]

Also, I think Fib(re/er)Functor (for some choice of re or er) is the standard name, as opposed to FundamentalFunctor.

[Adam Topaz]

Christian Merten said:

I think FundamentalFunctor can't reasonably become a Prop because all the PreservesFiniteCoproducts F etc. are no Props.

This should be refactored at some point...

[Christian Merten]

Adam Topaz said:

You know that we have the category of finite types, right? docs#FintypeCat I think?

I thought about this, but decided against it, because I assumed there was more solid API for the category of types, e.g. docs#CategoryTheory.injective_of_mono works in Type w but not in FintypeCat and I was afraid that there are more of these.

[Adam Topaz]

That's strange... we should have something for concrete categories where the forgetful functor reflects monos. If we don't have such an API, then it should be added anyway

[Adam Topaz]

Anyway, I would very strongly suggest that you use FintypeCat. If some API is missing, we should add it.

[Adam Topaz]

For example, what if at some point you want to compose your fibre functor with the inclusion from FSet to Profinite? That doesn't seem unreasonable, and making the fibre functor land in Type _ would make this very difficult, but it would be trivial if instead it landed in FintypeCat.

[Matthew Ballard]

Can you say docs#SplitMonoCategory + docs#IsIdempotentComplete in place of the mono splitting condition?

[Christian Merten]

Matthew Ballard said:

Can you say docs#SplitMonoCategory + docs#IsIdempotentComplete in place of the mono splitting condition?

Sorry, why is this equivalent? At least docs#CategoryTheory.IsIdempotentComplete is already implied by the rest, since C has finite limits (since it has a terminal object and pullbacks).

[Matthew Ballard]

If every mono is the composition of an isomorphism and the inclusion of a summand, then you have your splitting from the splitting of the summand and the inverse. If every mono is split, then you get a summand from idempotent completeness.

[Christian Merten]

I still can't follow: why is the inclusion of a summand split?

[Christian Merten]

The category of finite sets with the identity as fibre functor is Galois but the inclusion of the empty set into a singleton is a monomorphism that does not split, since there simply is no map in the other direction.

[Matthew Ballard]

Ah ok. I didn't read carefully terminal \neq initial here.

[Matthew Ballard]

Also why I phrased it as a question :)

[Matthew Ballard]

But there should be something cleaner than ∃ (Z : C) (u : Z ⟶ Y) (_ : IsColimit (BinaryCofan.mk i u)), True

[Christian Merten]

I agree, one could say ∃ (Z : C) (f : coprod X Z ≅ Y), f.hom ≫ coprod.inl = i instead, but the current statement is closer to "there is some object Z and some map u : Z ⟶ Y such that (Y,i,u) is the coproduct of X and Z" (which seems to me the better formulation)

[Matthew Ballard]

You don't want to use Nonempty?

[Christian Merten]

I have collected most of the arguments to show that a fibre functor F is pro-corepresentable. Now I don't really know how to say this. There does not seem to be a notion of pro category or pro-corepresentability yet. I suppose that approach would be the most elegant?

That is the current setup (I left out some implementations, since that is not releveant to my question)

variable {C : Type u} [Category.{u, u} C] (F : C ⥤ FintypeCat.{u}) [PreGaloisCategory C] [FibreFunctor F]

def ConnectedObjects := { A : C | ConnectedObject A }

def Idx : Type (max u u) := (A : @ConnectedObjects C _) × F.obj (A : C)

instance : Category (Idx F) where
  sorry

def diag (X : C) : (Idx F)ᵒᵖ ⥤ Type u where
  obj := by
    intro ⟨A, _⟩
    exact (A : C) ⟶ X
  map := by
    intro ⟨A, _⟩ ⟨B, _⟩ ⟨f, _⟩ (g : (A : C) ⟶ X)
    exact f ≫ g

Then the statement would be

example (X : C) : colimit (diag F X) ≅ (FintypeCat.incl.obj <| F.obj X) :=
  sorry

(from this I can then of course deduce that the left hand side is actually finite and that therefore the colimit already exists in FintypeCat and that we obtain the iso in FintypeCat )

Do you have any suggestions on this? Is someone working on pro-categories / pro-corepresentability?

[Kevin Buzzard]

@David Wärn has a rather elegant formalisation in lean 3 which was never PRed of ind-categories, so it would be just a case of (a) remembering where it was (b) porting it (manually, should be straightforward) and (c) changing the direction of the arrows (d) PRing it. My guess is that this is a viable approach which will work well if we can get past (a,)

[Christian Merten]

I suggest something along the lines of:

import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.HasLimits

universe u v w

open CategoryTheory Limits Functor

section Constructions

variable {C : Type u} [Category.{u, u} C] {J : Type u} [SmallCategory J]

def D (X : Jᵒᵖ ⥤ C) (Y : C) : J ⥤ Type u where
  obj i := X.obj ⟨i⟩ ⟶ Y
  map {i j} f := by
    intro g
    show X.obj { unop := j }  ⟶ Y
    exact X.map ⟨f⟩ ≫ g
  map_id {i} := by
    ext (g : X.obj ⟨i⟩ ⟶ Y)
    show X.map (𝟙 ⟨i⟩) ≫ g = g
    simp only [CategoryTheory.Functor.map_id, Category.id_comp]
  map_comp {i j k} f g := by
    ext (h : X.obj ⟨i⟩ ⟶ Y)
    show X.map (⟨g⟩ ≫ ⟨f⟩) ≫ h = X.map ⟨g⟩ ≫ (X.map ⟨f⟩ ≫ h)
    simp only [map_comp, Category.assoc]

@[simp]
lemma D_obj_eq (X : Jᵒᵖ ⥤ C) {Y : C} (i : J) : (D X Y).obj i = (X.obj ⟨i⟩ ⟶ Y) :=
  rfl

def Dtrans (X : Jᵒᵖ ⥤ C) {Y Z : C} (f : Y ⟶ Z) : D X Y ⟶ D X Z where
  app i g := g ≫ f
  naturality i j u := by
    ext (g : X.obj ⟨i⟩ ⟶ Y)
    show (X.map ⟨u⟩ ≫ g) ≫ f = X.map ⟨u⟩ ≫ (g ≫ f)
    simp only [Category.assoc]

@[simp]
lemma Dtrans_app_eq (X : Jᵒᵖ ⥤ C) {Y Z : C} (f : Y ⟶ Z) (i : J) (g : (D X Y).obj i) :
    (Dtrans X f).app i g = g ≫ f :=
  rfl

@[simp]
lemma Dtrans_id_eq (X : Jᵒᵖ ⥤ C) (Y : C) : Dtrans X (𝟙 Y) = 𝟙 (D X Y) := by
  ext i (f : X.obj ⟨i⟩ ⟶ Y)
  show f ≫ 𝟙 Y = f
  simp only [Category.comp_id]

@[simp]
lemma Dtrans_comp_eq (X : Jᵒᵖ ⥤ C) {Y Z W : C} (f : Y ⟶ Z) (g : Z ⟶ W) :
    Dtrans X (f ≫ g) = Dtrans X f ≫ Dtrans X g := by
  ext i (u : X.obj ⟨i⟩ ⟶ Y)
  show u ≫ (f ≫ g) = (u ≫ f) ≫  g
  simp only [Category.assoc]

@[simp]
lemma colimMapIdentity {J C : Type*} [Category C] [Category J] (F : J ⥤ C) [HasColimit F]
    : colimMap (𝟙 F) = 𝟙 (colimit F) := by
  aesop

@[simp]
lemma colimMapComp {J C : Type*} [Category C] [Category J] {F G H : J ⥤ C} [HasColimit F]
    [HasColimit G] [HasColimit H] (t : F ⟶ G) (s : G ⟶ H)
    : colimMap (t ≫ s) = colimMap t ≫ colimMap s := by
  aesop

noncomputable def h (X : Jᵒᵖ ⥤ C) : C ⥤ Type u where
  obj Y := colimit (D X Y)
  map {Y Z} f := by
    show colimit (D X Y) → colimit (D X Z)
    exact colim.map (Dtrans X f)
  map_id Y := by
    simp only [colim_map, Dtrans_id_eq, colimMapIdentity]
  map_comp {Y Z W} f g := by
    simp only [colim_map, Dtrans_comp_eq, colimMapComp]

@[simp]
lemma h_map_eq (X : Jᵒᵖ ⥤ C) {Y Z : C} (f : Y ⟶ Z) (i : J)
    (u : (X.obj ⟨i⟩ ⟶ Y)):
    (h X).map f (colimit.ι (D X Y) i u) = colimit.ι (D X Z) i (u ≫ f) :=
  sorry

noncomputable def procoyonedaLemma [IsFiltered J] (X : Jᵒᵖ ⥤ C) (F : C ⥤ Type u) :
    (h X ⟶ F) ≃ limit (X ⋙ F) where
  toFun t := by
    refine Types.Limit.mk (X ⋙ F) ?_ ?_
    intro i
    exact t.app (X.obj i) (colimit.ι (D X (X.obj i)) i.unop (𝟙 (X.obj i)))
    intro i j u
    have := congrFun (t.naturality (X.map u)) (colimit.ι (D X (X.obj i)) i.unop (𝟙 (X.obj i)))
    simp
    simp at this
    rw [←this]
    have h : colimit.ι (D X (X.obj j)) i.unop (X.map u) =
        colimit.ι (D X (X.obj j)) j.unop (𝟙 (X.obj j)) := by
      --apply (Types.FilteredColimit.colimit_eq_iff (D X (X.obj j))).mpr
      admit
    rw [h]
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

end Constructions

structure Proobject (C : Type u) [Category.{v, u} C] : Type _ where
  {J : Type w}
  [Jcategory : SmallCategory J]
  [Jfiltered : IsFiltered J]
  (X : Jᵒᵖ ⥤ C)

instance {C : Type u} [Category.{v, u} C] (X : Proobject C) : SmallCategory X.J := X.Jcategory

instance {C : Type u} [Category.{v, u} C] (X : Proobject C) : IsFiltered X.J := X.Jfiltered

noncomputable instance {C : Type u} [Category.{u, u} C] : Category (Proobject C) where
  Hom X Y := limit (Y.X ⋙ h X.X)
  id X := procoyonedaLemma X.X (h X.X) (𝟙 (h X.X))
  comp {X Y Z} f g := by
    let s : h Z.X ⟶ h Y.X := (procoyonedaLemma Z.X (h Y.X)).symm g
    let t : h Y.X ⟶ h X.X := (procoyonedaLemma Y.X (h X.X)).symm f
    exact procoyonedaLemma Z.X (h X.X) (s ≫ t)

class Procorepresentable {C : Type u} [Category.{u, u} C] (F : C ⥤ Type u) : Prop where
  has_procorepresentation : ∃ (X : Proobject C), Nonempty (h X.X ≅ F)

I defined a proobject as an inverse system instead of the associated covariant functor to Type u, the category instance by construction makes the procoyoneda embedding fully faithful.

[Christian Merten]

The universes need to be generalised, some universe problem also currently prevents me from using Types.FilteredColimit.colimit_eq_iff in one of the sorried helpers.

[David Wärn]

Kevin Buzzard said:

David Wärn has a rather elegant formalisation in lean 3 which was never PRed of ind-categories, so it would be just a case of (a) remembering where it was (b) porting it (manually, should be straightforward) and (c) changing the direction of the arrows (d) PRing it. My guess is that this is a viable approach which will work well if we can get past (a,)

I don't remember formalising ind-categories. Perhaps you were thinking about this small formalisation of the poset version? https://gist.github.com/dwarn/038887d7a9d5d7d6147fbbada2571f63

[Kevin Buzzard]

Ok I'll do some hunting because I was definitely not thinking of that :-) Maybe my mind is playing tricks on me but I'm still half confident

[Adam Topaz]

I remember @Bhavik Mehta working on ind categories

[Kevin Buzzard]

OK Apologies for summoning you David, I've now looked back at some DMs and I am instead going to summon @Markus Himmel with the claim that _they_ wrote ind-categories in Lean 3. How am I doing this time?

[Christian Merten]

Are you referencing this commit? https://github.com/leanprover-community/mathlib/compare/master...ind_object

[Markus Himmel]

I have this: https://github.com/leanprover-community/mathlib4/blob/coyoneda-extended/Mathlib/CategoryTheory/Limits/Indization/IndObject.lean It follows Kashiwara-Schapira. I am planning to develop this much further, my goal is to show that Pro(C) (or was it Ind(C)? Not sure) is Grothendieck if C is abelian. I am expecting to (finally) get back to this in December.

[Christian Merten]

Do you plan to define Ind C as the full subcategory of indrepresentable presheafs? Or as inductive systems, i.e. (J : Type w) [IsFiltered J] (X : J ⥤ C) as in FGA?

[Markus Himmel]

I still have a bunch of things that I want to do before I even get to defining the category structure, but an argument against defining it as a full subcategory is that the universes for morphisms are too large and you would have to work with LocallySmall everywhere. So I'm leaning towards your more explicit definition above.

[Christian Merten]

I wrote (because I needed this direction) a category instance on Pro C using a procoyonedaLemma (I posted a preliminary version above, that I have worked out in the meantime). Is this similar to what you had in mind for defining the category instance?

[Markus Himmel]

I was thinking of the 'as diagrams' definition in https://ncatlab.org/nlab/show/ind-object, which at least looks similar to what you have

[Kevin Buzzard]

Oh great to see it's in Lean 4 now! :D

[Christian Merten]

Markus Himmel said:

I was thinking of the 'as diagrams' definition in https://ncatlab.org/nlab/show/ind-object, which at least looks similar to what you have

That should be the dual of what I did: the composition law is then just composing the corresponding natural transformations via (ind/pro) yoneda.

[Joël Riou]

For the formalization of ind/pro-objects, I would prefer we follow @Markus Himmel definition as a full subcategory of the category of presheaves of sets, and that we provide a constructor which would take as an input a functor from a filtered category.

[Christian Merten]

You mean the definition as in https://github.com/leanprover-community/mathlib/compare/master...ind_object? Not the one Markus mentioned earlier in this thread.

[Joël Riou]

Yes, this one.

[Adam Topaz]

Certainly for stating that a presheaf is pro-representable one does not need pro-categories, but rather just state that there is a cofiltered diagram in C and a cone in presheaves with cone point the given presheaf over the functor composing the diagram with the yoneda embedding, then assert that this cone is a limit.

[Adam Topaz]

Something like this:

import Mathlib

namespace CategoryTheory

universe v u
variable {C : Type u} [Category.{v} C]

class IsProRepresentable (F : Cᵒᵖ ⥤ Type v) where
  cond : ∃ (J : Type v) (_h : SmallCategory J) (_ : IsCofiltered J)
    (E : J ⥤ C) (app : (Functor.const _).obj F ⟶ E ⋙ yoneda),
    Nonempty (Limits.IsLimit ⟨_, app⟩)

end CategoryTheory

[Christian Merten]

Thanks Adam. I think I'll go for some variant of this. Since I need this for covariant functors: Given J : Type w with [IsFiltered J], a diagram X : Jᵒᵖ ⥤ C does not compose with coyoneda. Should I put the ᵒᵖ on the C then?

[Adam Topaz]

I'm confused... why do you need covariant functors?

[Christian Merten]

Because the fibre functor is covariant.

[Adam Topaz]

Ok in that case I would use coyoneda and interchange C and Cop.

[Adam Topaz]

class IsProRepresentable (F : C ⥤ Type v) where
  cond : ∃ (J : Type v) (_h : SmallCategory J) (_ : IsCofiltered J)
    (E : J ⥤ Cᵒᵖ) (app : (Functor.const _).obj F ⟶ E ⋙ coyoneda),
    Nonempty (Limits.IsLimit ⟨_, app⟩)

[Adam Topaz]

Oh but I guess in this case one should indeed assume Filtered as opposed to `Cofiltered

[Adam Topaz]

So something like this:

class IsProRepresentable (F : C ⥤ Type v) where
  cond : ∃ (J : Type v) (_h : SmallCategory J) (_ : IsFiltered J)
    (E : J ⥤ Cᵒᵖ) (app : (Functor.const _).obj F ⟶ E ⋙ coyoneda),
    Nonempty (Limits.IsLimit ⟨_, app⟩)

[Christian Merten]

I was just going to ask about this :D But I am not sure, too many reversals of arrows at the same time.

[Adam Topaz]

yeah I'm confused too :)

[Christian Merten]

Ah and doesn't app need to go in the other direction as well? When I plug in a Y : C, I want colim Hom(X_i, Y) ≅ F(Y) (in mixed lean paper notation).

[Adam Topaz]

yeah you're right, and IsLimit should be IsColimit.

[Christian Merten]

Thank you :)

[Bhavik Mehta]

I did work on ind- and pro-objects, but I don't remember enough of the details off the top of my head to be that helpful here. I mostly just worked off nlab and its references, and I trust Markus to have good definitions!