Commit 2024-09-03 13:17 351bb940

View on Github →

feat(CategoryTheory): Characterization of Structured Arrows of Diagonal and Projections (#15838)

Estimated changes

Modified Mathlib/CategoryTheory/Comma/Over.lean

added def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.functor

added def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence.inverse

added def CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence

added def CategoryTheory.CostructuredArrow.ofDiagEquivalence'

added def CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor

added def CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse

added def CategoryTheory.CostructuredArrow.ofDiagEquivalence

added def CategoryTheory.StructuredArrow.ofDiagEquivalence'

added def CategoryTheory.StructuredArrow.ofDiagEquivalence.functor

added def CategoryTheory.StructuredArrow.ofDiagEquivalence.inverse

added def CategoryTheory.StructuredArrow.ofDiagEquivalence

added def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor

added def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.inverse

added def CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence