Joël Riou comments

Results 71 comments of


                                            Joël Riou

feat: target of final functor is connected iff source is connected

Thanks! bors merge

feat(AlgebraicGeometry/EllipticCurve/Jacobian): implement group operations on nonsingular rational points for Jacobian coordinates

Thanks! bors merge

feat(CategoryTheory/Action): category of continuous actions

This design seems better to me as compared to #12878

feat(CategoryTheory/Action): category of continuous actions

Thanks! bors merge

feat(CategoryTheory): the localized category is monoidal

> Do I understand that this PR is the next one in line in your epic derived + homology saga? Not exactly, in the future (not very soon), we should...

feat(CategoryTheory): the localized category is monoidal

Thanks! bors merge

feat(FiberedCategory/HomLift): definition of IsHomLift

> One thought I just had, is that maybe it could be a good idea to add the class `IsObjLift`, which would allow type-class inference to infer `domain_eq` and `codomain_eq`....

feat(FiberedCategory/HomLift): definition of IsHomLift

> 1. `IsHomLift p f φ` makes it so that I can leave parameters `p, f, φ` implicit, which makes it slightly more convenient to apply lemmas which has it...

feat(FiberedCategory/HomLift): definition of IsHomLift

Thanks! bors merge

feat(FiberCategory/Fibered): definition of a fibered category

Thanks! bors merge