## Stream: general

### Topic: GLn functor

#### ZHAO Jinxiang (Aug 14 2022 at 17:52):

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 (Aug 14 2022 at 18:27):

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

#### Junyan Xu (Aug 14 2022 at 18:33):

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

#### Junyan Xu (Aug 14 2022 at 18:34):

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 (Aug 14 2022 at 20:02):

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

#### Kevin Buzzard (Aug 14 2022 at 21:03):

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

#### Junyan Xu (Aug 14 2022 at 21:58):

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 (Aug 14 2022 at 22:43):

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

#### Eric Wieser (Aug 15 2022 at 04:38):

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

#### ZHAO Jinxiang (Aug 15 2022 at 06:05):

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 (Aug 15 2022 at 06:20):

Can you not reuse what you did in unit_functor?

#### Junyan Xu (Aug 15 2022 at 06:26):

@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 (Aug 15 2022 at 06:29):

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 (Aug 15 2022 at 06:32):

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

#### Yaël Dillies (Aug 15 2022 at 06:39):

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

#### Chris Birkbeck (Aug 15 2022 at 08:15):

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

#### ZHAO Jinxiang (Aug 15 2022 at 14:54):

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 (Aug 15 2022 at 15:06):

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

#### Reid Barton (Aug 15 2022 at 15:12):

The first sorry is refl

#### Damiano Testa (Aug 15 2022 at 17:13):

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 (Aug 15 2022 at 17:15):

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 (Aug 15 2022 at 17:44):

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

#### Damiano Testa (Aug 15 2022 at 17:49):

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

#### Adam Topaz (Aug 15 2022 at 17:52):

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

#### Adam Topaz (Aug 15 2022 at 17:52):

(taking values in Mon, say)

#### Kevin Buzzard (Aug 15 2022 at 19:12):

Are you sure this is a functor?

It's not.

#### Adam Topaz (Aug 15 2022 at 19:21):

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 (Aug 15 2022 at 19:23):

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 (Aug 15 2022 at 19:24):

oh yeah that's a good point

#### Adam Topaz (Aug 15 2022 at 19:26):

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

#### Adam Topaz (Aug 15 2022 at 19:26):

then take the functor these things represent

#### Junyan Xu (Aug 15 2022 at 20:38):

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 (Aug 15 2022 at 20:40):

@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 (Aug 15 2022 at 20:42):

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

#### Adam Topaz (Aug 15 2022 at 20:42):

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 (Aug 15 2022 at 20:43):

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

#### Adam Topaz (Aug 15 2022 at 20:44):

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

#### Junyan Xu (Aug 15 2022 at 20:44):

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 (Aug 15 2022 at 20:46):

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

#### Adam Topaz (Aug 15 2022 at 20:46):

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 (Aug 15 2022 at 20:47):

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 (Aug 15 2022 at 20:51):

I don't see sorries...

#### Kevin Buzzard (Aug 15 2022 at 20:53):

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

#### Junyan Xu (Aug 15 2022 at 21:05):

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 (Aug 15 2022 at 21:52):

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

#### Junyan Xu (Aug 24 2022 at 05:42):

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.

Last updated: Aug 03 2023 at 10:10 UTC