Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-14 14:48 d5c58eb8

View on Github →

chore(category_theory/*): make all forgetful functors use explicit arguments (#4139) As suggested as https://github.com/leanprover-community/mathlib/pull/4131#discussion_r487527599, for the sake of more uniform API.

Estimated changes

Modified src/algebra/homology/chain_complex.lean

Modified src/algebraic_geometry/presheafed_space.lean

Modified src/algebraic_geometry/sheafed_space.lean

Modified src/category_theory/grothendieck.lean

Modified src/category_theory/limits/over.lean

modified def category_theory.functor.to_cocone

modified def category_theory.functor.to_cone

modified def category_theory.over.colimit

modified def category_theory.over.forget_colimit_is_colimit

modified def category_theory.under.forget_limit_is_limit

modified def category_theory.under.limit

Modified src/category_theory/limits/shapes/constructions/over/connected.lean

modified def category_theory.over.creates_connected.raise_cone

modified def category_theory.over.creates_connected.raised_cone_is_limit

Modified src/category_theory/monad/bundled.lean

Modified src/category_theory/monoidal/internal.lean

added def Mod.forget

Modified src/category_theory/over.lean

modified theorem category_theory.over.forget_map

modified theorem category_theory.over.forget_obj

modified theorem category_theory.under.forget_map

modified theorem category_theory.under.forget_obj