mathlib3
feat(category_theory/*): Monoid objects in Abelian group are rings
#17006
Open
Open
feat(category_theory/*): Monoid objects in Abelian group are rings #17006
jjaassoonn
wants to merge
31 commits into
master
from
jjaassoonn/Mon_Ab
need cache
426622ec
cache
e563b0aa
cache
1f84813d
fix
5e2cf635
Delete Mon_in_Ab.lean
fbe2900b
c
126cbb7f
change to conrete
fb7e9fc1
jjaassoonn
commented
on 2022-10-16
ring instance
4631ed26
almost finished showing `Mon_ AddCommGroup \iso Ring`
f24f0161
finish monoid object in Ab is ring
bacf19ee
monoidal structure from equivalence of category partially finished
015bb41a
finished that equivalence of category transfers monoidal structure
f9216640
kim-em
commented
on 2022-10-19
delete `equivalence` and add a partial proof that equivalence of cate…
13046edf
change name
c8a80879
inverse direction
6cfdd89b
need cache
9875df08
monoidal strcutre of sheaves
a1514ca8
on proving presheaves are closed monoidal
f34f40bf
presheaves of abelian group are closed monoidal
2f176357
presheaf of modules
e11c0651
Mod over Mon in AddCommGroup is just modules
e5b870be
restriction map of presheaves of modules is linear
90148c5d
defined sheaf of module as presheaf of module that is a sheaf
6310a4a2
fix
7a396d63
commit
93cb3d3b
start working on sheaves
05d9b552
hom_equiv between tensor_left and ihom in category of sheaves of abel…
fe27e720
finish internal sheaf hom adjunction
3f85662d
make progress on associator
63784e1a
backward direction associator
bcecd58c
a little bit of progress
85cfbb4b
Reviewers
Assignees
No one assigned
Labels
WIP
awaiting-CI
t-algebra
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub