Commit 2023-06-17 05:17 d063ef50

View on Github →

feat: port CategoryTheory.Enriched.Basic (#5154)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Enriched/Basic.lean

added def CategoryTheory.EnrichedFunctor.comp

added def CategoryTheory.EnrichedFunctor.forget

added def CategoryTheory.EnrichedFunctor.id

added structure CategoryTheory.EnrichedFunctor

added def CategoryTheory.ForgetEnrichment.homOf

added theorem CategoryTheory.ForgetEnrichment.homOf_homTo

added def CategoryTheory.ForgetEnrichment.homTo

added theorem CategoryTheory.ForgetEnrichment.homTo_homOf

added def CategoryTheory.ForgetEnrichment.of

added theorem CategoryTheory.ForgetEnrichment.of_to

added def CategoryTheory.ForgetEnrichment.to

added theorem CategoryTheory.ForgetEnrichment.to_of

added def CategoryTheory.ForgetEnrichment

added structure CategoryTheory.GradedNatTrans

added def CategoryTheory.TransportEnrichment

added def CategoryTheory.categoryOfEnrichedCategoryType

added def CategoryTheory.eComp

added def CategoryTheory.eId

added theorem CategoryTheory.e_assoc

added theorem CategoryTheory.e_comp_id

added theorem CategoryTheory.e_id_comp

added def CategoryTheory.enrichedCategoryTypeEquivCategory

added def CategoryTheory.enrichedCategoryTypeOfCategory

added def CategoryTheory.enrichedFunctorTypeEquivFunctor

added def CategoryTheory.enrichedNatTransYoneda

added def CategoryTheory.enrichedNatTransYonedaTypeIsoYonedaNatTrans

added theorem CategoryTheory.forgetEnrichment_comp

added theorem CategoryTheory.forgetEnrichment_id'

added theorem CategoryTheory.forgetEnrichment_id