Commit 2019-05-14 20:21 7b579b79

View on Github →

feat(category_theory): adjoint equivalences and limits under equivalences (#986)

  • feat(category_theory): adjoint equivalences and limits
  • Define equivalences to be adjoint equivalences.
    • Show that one triangle law implies the other for equivalences
    • Prove that having a limit of shape J is preserved under an equivalence J ≌ J'.
    • Construct an adjoint equivalence from a (non-adjoint) equivalence
  • Put in the iso namespace, so that we can write α.app for α : F ≅ G.
  • Add some basic lemmas about equivalences, isomorphisms.
  • Move some lemmas from nat_trans to functor_category and state them using F ⟶ G instead of nat_trans F G (maybe these files should just be merged?)
  • Some small tweaks, improvements
  • opposite of discrete is discrete This also shows that C^op has coproducts if C has products and vice versa Also fix rebase errors
  • fix error (I don't know what caused this to break)
  • Use tidy a bit more
  • construct an adjunction from an equivalence add notation for an adjunction. make some arguments of adjunction constructors implicit
  • use adjunction notation
  • formatting
  • do adjointify_η as a natural iso directly, to avoid checking naturality
  • tersifying
  • fix errors, a bit of cleanup
  • fix elements.lean
  • fix error, address comments

Estimated changes