GLn functor

Stream: general

[ZHAO Jinxiang]

import linear_algebra.general_linear_group
import category_theory.functor.category
import algebra.category.Ring.basic

namespace playground
open category_theory

universes u

variables (n : Type u) [decidable_eq n] [fintype n]

def GLn_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (GL n R.α),
  map := λ (A B : CommRing) (f: A.α →+* B.α), (
  begin
    -- TODO: help me here
    sorry
  end : Group.of (GL n A.α) ⟶ Group.of (GL n B.α)),
  map_id' := begin
    sorry
  end,
  map_comp' := begin
    sorry
  end,
}

def unit_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (Rˣ),
  map := λ (A B : CommRing) (f: A.α →+* B.α), (
  begin
    -- TODO: help me here
    sorry
  end : Group.of (↥A)ˣ ⟶ Group.of (↥B)ˣ),
  map_id' := begin
    sorry
  end,
  map_comp' := begin
    sorry
  end,
}

end playground

I don't know how to fix the sorry here. Can you help me? :flushed:

[Junyan Xu]

docs#Group.of_hom, docs#units.map

[Junyan Xu]

You have to write the analogue of docs#units.map for GL n by yourself, it seems.

[Junyan Xu]

You may use docs#matrix.map and docs#ring_hom.map_det

[Junyan Xu]

It's a pity that docs#matrix.general_linear_group doesn't work for noncommutative rings like the quaternions currently. (The determinant definition can't be generalized to noncommutative rings, so maybe we should just work with the unit group in the matrix ring if we want that.)

[Eric Wieser]

Isn't docs#matrix.general_linear_group just an alias for units?

[Kevin Buzzard]

Probably in some sense, but in the same sense that the complexes is just an alias for R x R

[Junyan Xu]

Eric Wieser said:

Isn't docs#matrix.general_linear_group just an alias for units?

Indeed! I was misguided by the docstring saying it's the matrices with determinant a unit. So the current definition can be generalized to noncommutative rings without problem.

[Reid Barton]

That docstring is also misleading in that I think most people would interpret "matrix with unit determinant" as "matrix with determinant 1".

[Eric Wieser]

Also "defined as a subtype of matrices" in that docstring is a lie

[ZHAO Jinxiang]

import linear_algebra.general_linear_group
import category_theory.functor.category
import algebra.category.Ring.basic
import linear_algebra.special_linear_group

namespace playground
open category_theory

universes u

variables (n : Type u) [decidable_eq n] [fintype n]

def GLn_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (GL n R.α),
  map := λ (A B : CommRing) (f: A.α →+* B.α), (
  begin
    apply Group.of_hom,
    have f1 := @ring_hom.map_det n _ _ A.α _ B.α _ f,
    have := @monoid_hom.mk' (GL n A.α) (GL n B.α) _ _ (λ X, begin
      refine matrix.general_linear_group.mk' _ _,
      exact matrix.map X f,
    -- TODO: help me here
      sorry,
    end),
    apply this,
    -- TODO: help me here
    sorry,
  end : Group.of (GL n A.α) ⟶ Group.of (GL n B.α)),
  map_id' := begin
    sorry
  end,
  map_comp' := begin
    sorry
  end,
}

def unit_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (Rˣ),
  map := λ (A B : CommRing) (f: A.α →+* B.α), units.map f,
  map_id' := λ A, units.map_id A,
  map_comp' := λ A B C (f: A.α →+* B.α) (g: B.α →+* C.α), by fconstructor,
}

end playground

Thank you @Junyan Xu . But I still don't know how to fix this.

[Yaël Dillies]

Can you not reuse what you did in unit_functor?

[Junyan Xu]

@ZHAO Jinxiang This works:

def GLn_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (GL n R.α),
  map := λ (A B : CommRing) (f: A.α →+* B.α), (
  begin
    apply Group.of_hom,
    apply units.map,
    exact f.map_matrix.to_monoid_hom, /- ring_hom.map_matrix -/
  end : Group.of (GL n A.α) ⟶ Group.of (GL n B.α)),
  map_id' := begin
    sorry
  end,
  map_comp' := begin
    sorry
  end,
}

Since we discovered that general_linear_group is actually defined to be the units, we apply units.map again.

[Junyan Xu]

In term mode you can just do map := λ _ _ f, Group.of_hom (units.map f.map_matrix.to_monoid_hom), or even omit the Group.of_hom (not necessarily good practice).

[Yaël Dillies]

Can you not get GLn_functor as the composition of some functor and unit_functor?

[Yaël Dillies]

Btw, unit_functor already exists as docs#Mon.units composed with the appropriate sequence of forgetful functors.

[Chris Birkbeck]

Yeah the doc strings are my fault I forgot to change them after the PR review changes

[ZHAO Jinxiang]

Thanks for all your helps.
But it seems that I also need help here. :joy:

import linear_algebra.general_linear_group
import category_theory.functor.category
import algebra.category.Ring.basic

open category_theory

universes u

variables (n : Type u) [decidable_eq n] [fintype n]

def GLn_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (GL n R.α),
  map := λ A B (f: A.α →+* B.α),
    (units.map f.map_matrix.to_monoid_hom :
      Group.of (GL n A.α) ⟶ Group.of (GL n B.α)),
  map_id' := λ A, begin
    dunfold CommRing category.to_category_struct SemiRing.assoc_ring_hom bundled_hom.map_hom bundled_hom.bundled_hom_of_parent_projection comm_ring.to_ring bundled_hom.map,
    dunfold SemiRing.bundled_hom,
    dsimp,
    convert_to units.map ↑((ring_hom.id A.α).map_matrix) = _,
    dunfold ring_hom.id id coe lift_t has_lift_t.lift coe_t has_coe_t.coe ring_hom.map_matrix units.map monoid_hom.mk',
    simp,
    dunfold group.to_monoid div_inv_monoid.to_monoid bundled_hom.id,
    dsimp,
    dunfold monoid_hom.id,
    simp,
  end,
  map_comp' := λ A B C (f: A.α →+* B.α) (g: B.α →+* C.α), begin
    -- TODO: help me here
    sorry,
  end,
}

def units_functor : CommRing ⥤ Group := {
  obj := λ R, Group.of (Rˣ),
  map := λ (A B : CommRing) (f: A.α →+* B.α), units.map f,
  map_id' := λ A, units.map_id A,
  map_comp' := λ A B C (f: A.α →+* B.α) (g: B.α →+* C.α), by fconstructor,
}

def det_nat_trans : (GLn_functor n) ⟶ units_functor :=
{ app := λ R, matrix.general_linear_group.det,
  naturality' := λ R R' (f: R.α →+* R'.α), begin
    dunfold GLn_functor units_functor,
    dsimp,
    dunfold coe lift_t has_lift_t.lift coe_t has_coe_t.coe coe_fn fun_like.has_coe_to_fun ,
    simp,
    -- TODO: help me here
    sorry,
  end
}

[Eric Wieser]

I imagine docs#units.map_comp and docs#ring_hom.map_matrix_comp will do most of the work

[Reid Barton]

The first sorry is refl

[Damiano Testa]

In fact, the two first definitions can be compressed to

def GLn_functor : CommRing ⥤ Group :=
{ obj       := λ R, Group.of (GL n R.α),
  map       := λ A B f, units.map f.map_matrix.to_monoid_hom,
  map_id'   := λ A, by { ext, simp },
  map_comp' := λ A B C f g, rfl }

def units_functor : CommRing ⥤ Group :=
{ obj       := λ R, Group.of Rˣ,
  map       := λ A B f , units.map f,
  map_id'   := λ A, units.map_id A,
  map_comp' := λ A B C f g, rfl }

[Damiano Testa]

I find that most of the proofs in the category theory side of mathlib are obtained by some combination of ext, simp, dsimp, refl. However, since they usually take a long time to play out, trying out all combinations is usually not a viable option. :upside_down:

[Johan Commelin]

I guess tidy can do them. So you can even leave out the last two fields in both defs.

[Damiano Testa]

Ah, this is another proof strategy: not even proving lemmas!

[Adam Topaz]

What's the correct abstract category theory nonsense that makes $X \mapsto End(X)$ into a functor?

[Adam Topaz]

(taking values in Mon, say)

[Kevin Buzzard]

Are you sure this is a functor?

[Adam Topaz]

It's not.

[Adam Topaz]

But the functor $k \mapsto End_k(k^n)$ is, and the functor $k \mapsto GL_n(k)$ is the composition of that with the units functor. I'm just wondering if there is a categorical abstraction of this.

[Kevin Buzzard]

The End in that example is a representable functor taking values in rings so maybe it has something to do with Hopf algebras rather than a general category thing

[Adam Topaz]

oh yeah that's a good point

[Adam Topaz]

I guess the general thing is to take a monoid object in some monoidal category and to look at its units.

[Adam Topaz]

then take the functor these things represent

[Junyan Xu]

My viewpoint is that M : R ↦ R^n defines a "dependent functor" from Ring to Module over the ring, and you can view it as a sheaf of modules. Usually $\text{Hom}_R(M(R), N(R))$ don't form a (pre)sheaf (so it's not the way to define sheaf Hom), but here M is "quasi-coherent" so we're OK; to define $S^n\to S^n$ from $f : R^n\to R^n$ and a ring hom ϕ : R →+* S you compose the isomorphism $S^n\cong R^n\otimes_S S$ with $R^n\otimes_S S\to S^n$ induced by $f$ composed with the dependent "functor.map ϕ": $R^n\to S^n$ (as R-modules). Of course when M=N the sheaf Hom from M to itself is a sheaf of rings by composition.

By the way I think we should define presheaves of modules (on ringed spaces) in terms of dependent functors, and build the API to connect with other useful definitions afterwards. Even though Cat is a 1-category and the (restriction of scalars) functor taking a Ring to its category of modules is a strict functor, we may want to define functors dependent on an arbitrary (op)lax functor into Cat, now that we have the framework (and notice that extension of scalars isn't a strict functor). However, it seems that a theory of dependent functors isn't present in the literature.

[Kevin Buzzard]

@Junyan Xu what do you mean by dependent functors? I would love to see a definition of presheaves of modules in mathlib! It's been missing for far too long. I would really like to see the sheaf of Kaehler differentials, which would be a great test case.

[Adam Topaz]

Dependent functor are the functorial analogue of a dependent function ;)

[Adam Topaz]

So $R \mapsto R^n$ is a dependent functor because $R^n : Mod_R$, and $Mod_R$ is a category which depends on $R$

[Adam Topaz]

And when you have a morphism $R \to S$ you relate $R^n$ and $S^n$ by base-change

[Adam Topaz]

This is all possible to make precise with pseudofunctors and/or Grothendieck constructions

[Junyan Xu]

It's basically the definition of a sheaf of modules and I made the definition here; it's a functor dependent on a oplax_functor (locally_discrete C) Cat, which in the case of sheaf of modules you take it to be the sheaf of rings (which is a functor from opens to Ring) composed with the functor from Ring to Cat.
variables {C : Type u} [category.{v} C] (F : oplax_functor (locally_discrete C) Cat.{v' u'})

[Kevin Buzzard]

I'd encourage you to PR it! I think it's time we started experimenting with this.

[Adam Topaz]

Kevin Buzzard said:

I'd encourage you to PR it! I think it's time we started experimenting with this.

I'll second this!

[Junyan Xu]

I haven't developed much (if any) APIs for it; as you can see it's been abandoned for months with lots of sorries. Maybe someone can take it up!

[Kevin Buzzard]

I don't see sorries...

[Kevin Buzzard]

I see merge conflicts, and I also see that I no longer understand how VS Code deals with them :-/

[Junyan Xu]

Yeah, it seems I haven't even written down the sorries, but I did have a TODO list that I just pushed. I've also defined dependent nat_trans and shown that dependent functors form a category. The latest commit in that branch changed functors to prefunctors, because I wanted to understand which conditions are essential. The branch does a lot of other stuff and the dependent functor portion is very much under construction; I don't think a single defintion could make a PR ...

[Kevin Buzzard]

I have made PRs with just definitions eg projective modules and elliptic curves

[Junyan Xu]

Adam Topaz said:

Dependent functor are the functorial analogue of a dependent function ;)

This analogy actually makes a lot of sense. If categories are types and functors are functions, then functor categories are function types, functors to Cat are type families, and Grothendieck constructions are sigma types; what's missing are pi types (i.e. dependent function types), and introducing a category of dependent functors would fill in this gap.

The paper https://arxiv.org/abs/2109.04239 feels very relevant, but I find the notation hard to decipher. I'm unaware of any other reference.

In the context of sheaves of modules we have the following:

1. We have the functor Module : Ring ⥤ Cat with functor.map given by restriction of scalars, and we consider it as a type family F : β → Type*.

2. We can form the Grothendieck category of the functor Module, i.e. the category BundledModule, which corresponds to the sigma type Σ b, F b.

3. Whenever we have a presheaf of rings, i.e. a functor f : opens X ⥤ Ring (omitting the op), composing with Module gives a functor opens X ⥤ Cat, corresponding to the function F ∘ f : α → Type*.

4. Composition is functorial, resulting in a functor (opens X ⥤ Ring) ⥤ (opens X ⥤ Cat) from presheaves of rings to presheaves of Cats, corresponding to the fact that λ f, F ∘ f : (α → β) → (α → Type*) is a function.

5. Now for every opens X ⥤ Cat we introduce a dependent functor category; this association is functorial and corresponds to the function λ ι, Π a, ι a : (α → Type*) → Type*.

6. Composing with the functor in 4, we arrive at a functor (opens X ⥤ Ring) ⥤ Cat, sending a presheaf of rings O_X to the category of presheaves of modules over O_X, and we may take its Grothendieck construction, which corresponds to the type Σ f, Π a, F (f a).

7. This category should be equivalent (or isomorphic?) to the category of presheaves of bundled modules over X, i.e. opens X ⥤ BundledModule, corresponding to the type α → Σ b, F b. This looks similar to Theorem 3.6 in the paper.

Interestingly, the functoriality of the Grothendieck construction is not used in the argument above.

In Type* the construction of the equivalence is very simple:

def fun_to_sigma_equiv' {α β : Type*} (F : β → Type*) :
  (α → Σ b, F b) ≃ (Σ f : α → β, Π a, F (f a)) :=
{ to_fun := λ g, ⟨sigma.fst ∘ g, λ a, sigma.snd (g a)⟩,
  inv_fun := λ g a, ⟨g.fst a, g.snd a⟩,
  left_inv := λ g, funext $ λ a, sigma.eta _,
  right_inv := sigma.eta }

The special case F := id yields (α → Σ b, b) ≃ (Σ f : α → Type*, Π a, f a) but the construction isn't simpler.

However, a lot needs to be done to flesh out the category version; for example, it's not totally clear which functors mentioned above should be strict (if any) and which are allowed to be (op)lax. To deal with sheaves of modules, it suffices to restrict to strict functors, since Module : Ring ⥤ Cat is strict, but we may not want to exploit this strictness since it involves equality of functors. If that's the case, then the first thing to do is probably generalizing the Grothendieck construction to any oplax functor, which I have done in the branch and should be ready to PR after some cleanup.