Commit 2023-03-07 17:18 db459c59

View on Github →

feat: port CategoryTheory.ConcreteCategory.Basic (#2619)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

added theorem CategoryTheory.ConcreteCategory.bijective_of_isIso

added theorem CategoryTheory.ConcreteCategory.congr_arg

added theorem CategoryTheory.ConcreteCategory.congr_hom

added theorem CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout

added theorem CategoryTheory.ConcreteCategory.epi_of_surjective

added def CategoryTheory.ConcreteCategory.hasCoeToFun

added theorem CategoryTheory.ConcreteCategory.hasCoeToFun_Type

added def CategoryTheory.ConcreteCategory.hasCoeToSort

added theorem CategoryTheory.ConcreteCategory.hom_ext

added theorem CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback

added theorem CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback

added theorem CategoryTheory.ConcreteCategory.mono_of_injective

added theorem CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout

added def CategoryTheory.HasForget₂.mk'

added theorem CategoryTheory.coe_comp

added theorem CategoryTheory.coe_id

added theorem CategoryTheory.comp_apply

added theorem CategoryTheory.congr_hom

added def CategoryTheory.forget

added theorem CategoryTheory.forget_map_eq_coe

added theorem CategoryTheory.forget_obj_eq_coe

added def CategoryTheory.forget₂

added def CategoryTheory.hasForgetToType

added theorem CategoryTheory.id_apply