leanprover-community/mathlib

Pull Requests Commits

a little bit of progress

jjaassoonn committed 3 years ago

85cfbb4b

backward direction associator

jjaassoonn committed 3 years ago

bcecd58c

make progress on associator

jjaassoonn committed 3 years ago

63784e1a

finish internal sheaf hom adjunction

jjaassoonn committed 3 years ago

3f85662d

hom_equiv between tensor_left and ihom in category of sheaves of abelian groups

jjaassoonn committed 3 years ago

fe27e720

start working on sheaves

jjaassoonn committed 3 years ago

05d9b552

jjaassoonn committed 3 years ago

93cb3d3b

jjaassoonn committed 3 years ago

7a396d63

defined sheaf of module as presheaf of module that is a sheaf

jjaassoonn committed 3 years ago

6310a4a2

restriction map of presheaves of modules is linear

jjaassoonn committed 3 years ago

90148c5d

Mod over Mon in AddCommGroup is just modules

jjaassoonn committed 3 years ago

e5b870be

presheaf of modules

jjaassoonn committed 3 years ago

e11c0651

presheaves of abelian group are closed monoidal

jjaassoonn committed 3 years ago

2f176357

on proving presheaves are closed monoidal

jjaassoonn committed 3 years ago

f34f40bf

monoidal strcutre of sheaves

jjaassoonn committed 3 years ago

a1514ca8

jjaassoonn committed 3 years ago

9875df08

inverse direction

jjaassoonn committed 3 years ago

6cfdd89b

jjaassoonn committed 3 years ago

c8a80879

delete `equivalence` and add a partial proof that equivalence of category induces equivalence of Mon_

jjaassoonn committed 3 years ago

13046edf

finished that equivalence of category transfers monoidal structure

jjaassoonn committed 3 years ago

f9216640

monoidal structure from equivalence of category partially finished

jjaassoonn committed 3 years ago

015bb41a

finish monoid object in Ab is ring

jjaassoonn committed 3 years ago

bacf19ee

almost finished showing `Mon_ AddCommGroup \iso Ring`

jjaassoonn committed 3 years ago

f24f0161

jjaassoonn committed 3 years ago

4631ed26

change to conrete

jjaassoonn committed 3 years ago

fb7e9fc1

jjaassoonn committed 3 years ago

126cbb7f

Delete Mon_in_Ab.lean

jjaassoonn committed 3 years ago

Verified fbe2900b

jjaassoonn committed 3 years ago

5e2cf635

jjaassoonn committed 3 years ago

1f84813d

jjaassoonn committed 3 years ago

e563b0aa

Older