Commit 2023-12-07 16:10 243f4027

View on Github →

feat(CategoryTheory): more API for product categories (#8865) This PR develops notions about product categories (natural isomorphisms, equivalences) in order to fill the prerequisites of PR #8864 about the localization of product categories.

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.pi

added def CategoryTheory.MorphismProperty.pi

Modified Mathlib/CategoryTheory/Pi/Basic.lean

added def CategoryTheory.Equivalence.pi

added def CategoryTheory.Functor.pi'CompEval

added def CategoryTheory.NatIso.pi'

added def CategoryTheory.NatIso.pi

added def CategoryTheory.NatTrans.pi'

added def CategoryTheory.Pi.eqToEquivalence

added def CategoryTheory.Pi.eqToEquivalenceFunctorIso

added def CategoryTheory.Pi.evalCompEqToEquivalenceFunctor

added def CategoryTheory.Pi.optionEquivalence

added theorem CategoryTheory.isIso_pi_iff