Commit 2023-04-15 00:49 85848f29

View on Github →

feat: port CategoryTheory.Subobject.MonoOver (#3423)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subobject/MonoOver.lean

added def CategoryTheory.MonoOver.congr

added def CategoryTheory.MonoOver.existsIsoMap

added def CategoryTheory.MonoOver.existsPullbackAdj

added def CategoryTheory.MonoOver.exists_

added def CategoryTheory.MonoOver.forget

added def CategoryTheory.MonoOver.forgetImage

added theorem CategoryTheory.MonoOver.forget_obj_hom

added theorem CategoryTheory.MonoOver.forget_obj_left

added def CategoryTheory.MonoOver.image

added def CategoryTheory.MonoOver.imageForgetAdj

added def CategoryTheory.MonoOver.imageMonoOver

added theorem CategoryTheory.MonoOver.imageMonoOver_arrow

added def CategoryTheory.MonoOver.isoMk

added def CategoryTheory.MonoOver.lift

added def CategoryTheory.MonoOver.liftComp

added def CategoryTheory.MonoOver.liftId

added def CategoryTheory.MonoOver.liftIso

added theorem CategoryTheory.MonoOver.lift_comm

added theorem CategoryTheory.MonoOver.lift_obj_arrow

added def CategoryTheory.MonoOver.map

added def CategoryTheory.MonoOver.mapComp

added def CategoryTheory.MonoOver.mapId

added def CategoryTheory.MonoOver.mapIso

added def CategoryTheory.MonoOver.mapPullbackAdj

added theorem CategoryTheory.MonoOver.map_obj_arrow

added theorem CategoryTheory.MonoOver.map_obj_left

added def CategoryTheory.MonoOver.mk'

added def CategoryTheory.MonoOver.mk'ArrowIso

added theorem CategoryTheory.MonoOver.mk'_arrow

added theorem CategoryTheory.MonoOver.mk'_coe'

added def CategoryTheory.MonoOver.pullback

added def CategoryTheory.MonoOver.pullbackComp

added def CategoryTheory.MonoOver.pullbackId

added def CategoryTheory.MonoOver.pullbackMapSelf

added theorem CategoryTheory.MonoOver.pullback_obj_arrow

added theorem CategoryTheory.MonoOver.pullback_obj_left

added def CategoryTheory.MonoOver.slice

added theorem CategoryTheory.MonoOver.w

added def CategoryTheory.MonoOver