Andrew Yang

Results 88 comments of Andrew Yang

refactor(CategoryTheory): the structure Functor.FullyFaithful

Oops, forgot about this. Thanks a lot! maintainer merge

feat(CategoryTheory/Sites): functors which preserves sheafification

Thanks a lot! maintainer merge

Feat(LinearAlgebra/TensorProduct/RightExactness): Tensoring with a quotient of the ring

Also can you provide `_ ∘ₗ TensorProduct.mk R _ M 1 = Submodule.mkQ _`? Just found out that I needed them :D

Feat(LinearAlgebra/TensorProduct/RightExactness): Tensoring with a quotient of the ring

Thanks a lot! maintainer merge

feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot

Thanks! maintainer merge

feat(CategoryTheory): right derived functors

Do we have left derived functors yet? Thanks Joël and Dagur maintainer merge

feat: morphisms of presheaves that are locally injective for a Grothendieck topology

Thanks! maintainer merge

feat(CategoryTheory/Sites): the topology is generated by 1-hypercovers

Is this ready for review?

feat(CategoryTheory/Sites): the topology is generated by 1-hypercovers

Am I correct that @dagurtomas thinks this is good to go?

feat(CategoryTheory/Sites): the topology is generated by 1-hypercovers

Okay just making sure. Thanks Joël and Dagur! maintainer merge