## Stream: general

### Topic: Stricklandization of biproduct

#### Kenny Lau (Mar 10 2019 at 00:17):

import linear_algebra.basic

universes u v w u₁ v₁

variables (R : Type u) [ring R]

class biproduct (M : Type v) [add_comm_group M] [module R M]
(N : Type w) [add_comm_group N] [module R N]
(P : Type u₁) [add_comm_group P] [module R P] :=
(inl : M →ₗ[R] P)
(inr : N →ₗ[R] P)
(fst : P →ₗ[R] M)
(snd : P →ₗ[R] N)
(fst_inl : fst.comp inl = 1)
(snd_inr : snd.comp inr = 1)
(fst_inl_fst : fst.comp (inl.comp fst) = fst)
(snd_inr_snd : snd.comp (inr.comp snd) = snd)
(inl_fst_add_inr_snd : inl.comp fst + inr.comp snd = 1)

variables (M : Type v) [add_comm_group M] [module R M]
variables (N : Type w) [add_comm_group N] [module R N]

instance biproduct_prod : biproduct R M N (M × N) :=
{ inl := linear_map.inl R M N,
inr := linear_map.inr R M N,
fst := linear_map.fst R M N,
snd := linear_map.snd R M N,
fst_inl := linear_map.ext $λ x, rfl, snd_inr := linear_map.ext$ λ x, rfl,
fst_inl_fst := linear_map.ext $λ x, rfl, snd_inr_snd := linear_map.ext$ λ x, rfl,
inl_fst_add_inr_snd := linear_map.ext $λ ⟨m, n⟩, prod.ext (add_zero m) (zero_add n) } instance biproduct_prod_swap : biproduct R M N (N × M) := { inl := linear_map.inr R N M, inr := linear_map.inl R N M, fst := linear_map.snd R N M, snd := linear_map.fst R N M, fst_inl := linear_map.ext$ λ x, rfl,
snd_inr := linear_map.ext $λ x, rfl, fst_inl_fst := linear_map.ext$ λ x, rfl,
snd_inr_snd := linear_map.ext $λ x, rfl, inl_fst_add_inr_snd := linear_map.ext$ λ ⟨m, n⟩, prod.ext (zero_add m) (add_zero n) }

variables {P : Type u₁} [add_comm_group P] [module R P] [biproduct R M N P]
variables {Q : Type v₁} [add_comm_group Q] [module R Q]

def biproduct.rec' (f : M →ₗ[R] Q) (g : N →ₗ[R] Q) : P →ₗ[R] Q :=
f.comp (biproduct.fst R M N P) + g.comp (biproduct.snd R M N P)

def biproduct.corec' (f : Q →ₗ[R] M) (g : Q →ₗ[R] N) : Q →ₗ[R] P :=
(biproduct.inl R M N P).comp f + (biproduct.inr R M N P).comp g

theorem biproduct.eq_rec (f : P →ₗ[R] Q) : f = biproduct.rec' R M N (f.comp (biproduct.inl R M N P)) (f.comp (biproduct.inr R M N P)) :=
by rw [biproduct.rec', linear_map.comp_assoc, linear_map.comp_assoc]; sorry -- missing comp_add

theorem biproduct.eq_corec (f : Q →ₗ[R] P) : f = biproduct.corec' R M N ((biproduct.fst R M N P).comp f) ((biproduct.snd R M N P).comp f) :=
by rw [biproduct.corec', ← linear_map.comp_assoc, ← linear_map.comp_assoc]; sorry -- missing add_comp

def biproduct.equiv_prod : P ≃ₗ[R] M × N :=
linear_equiv.of_linear
(biproduct.rec' R M N (biproduct.inl R M N _) (biproduct.inr R M N _))
(biproduct.corec' R M N (biproduct.fst R M N _) (biproduct.snd R M N _))
sorry
sorry


#### Kenny Lau (Mar 10 2019 at 00:17):

anyone wanna continue?

#### Kenny Lau (Mar 10 2019 at 00:18):

goal: a functor F:R-Mod=>S-Mod is additive iff it preserves biproduct

#### Kevin Buzzard (Mar 10 2019 at 00:19):

There's some cool endomorphism of A + B that you get from a map from A to B, presumably.

#### Kenny Lau (Mar 10 2019 at 00:20):

the "cone", i.e. the matrix $\begin{bmatrix}1&0\\f&1\end{bmatrix}$ right

#### Kenny Lau (Mar 10 2019 at 00:20):

Weibel was all for it

#### Kenny Lau (Mar 10 2019 at 00:24):

def biproduct.mk_end (a : M →ₗ[R] M) (b : N →ₗ[R] M) (c : M →ₗ[R] N) (d : N →ₗ[R] N) : P →ₗ[R] P :=
biproduct.corec' R M N (biproduct.rec' R M N a b) (biproduct.rec' R M N c d)


#### Mario Carneiro (Mar 10 2019 at 00:30):

(fst_inl : fst.comp inl = 1)
(snd_inr : snd.comp inr = 1)
(fst_inl_fst : fst.comp (inl.comp fst) = fst)
(snd_inr_snd : snd.comp (inr.comp snd) = snd)


Don't the last two follow from the first two? I guess 1 is id

#### Kenny Lau (Mar 10 2019 at 00:33):

there is something wrong with me

#### Kenny Lau (Mar 10 2019 at 00:34):

you're right

Last updated: May 14 2021 at 03:27 UTC