Commit 2023-04-25 06:01 44cdd3a0

View on Github →

feat: port CategoryTheory.Subobject.Comma (#3502)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subobject/Comma.lean

added def CategoryTheory.CostructuredArrow.liftQuotient

added theorem CategoryTheory.CostructuredArrow.lift_projectQuotient

added def CategoryTheory.CostructuredArrow.projectQuotient

added theorem CategoryTheory.CostructuredArrow.projectQuotient_factors

added theorem CategoryTheory.CostructuredArrow.projectQuotient_mk

added def CategoryTheory.CostructuredArrow.quotientEquiv

added theorem CategoryTheory.CostructuredArrow.unop_left_comp_ofMkLEMk_unop

added theorem CategoryTheory.CostructuredArrow.unop_left_comp_underlyingIso_hom_unop

added def CategoryTheory.StructuredArrow.liftSubobject

added theorem CategoryTheory.StructuredArrow.lift_projectSubobject

added def CategoryTheory.StructuredArrow.projectSubobject

added theorem CategoryTheory.StructuredArrow.projectSubobject_factors

added theorem CategoryTheory.StructuredArrow.projectSubobject_mk

added def CategoryTheory.StructuredArrow.subobjectEquiv