Commit 2023-06-13 23:55 0f286b04

View on Github →

feat: port CategoryTheory.DifferentialObject (#4020)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/DifferentialObject.lean

added def CategoryTheory.DifferentialObject.Hom.comp

added def CategoryTheory.DifferentialObject.Hom.id

added structure CategoryTheory.DifferentialObject.Hom

added theorem CategoryTheory.DifferentialObject.comp_f

added theorem CategoryTheory.DifferentialObject.eqToHom_f

added theorem CategoryTheory.DifferentialObject.ext

added def CategoryTheory.DifferentialObject.forget

added theorem CategoryTheory.DifferentialObject.id_f

added def CategoryTheory.DifferentialObject.isoApp

added theorem CategoryTheory.DifferentialObject.isoApp_refl

added theorem CategoryTheory.DifferentialObject.isoApp_symm

added theorem CategoryTheory.DifferentialObject.isoApp_trans

added def CategoryTheory.DifferentialObject.mkIso

added def CategoryTheory.DifferentialObject.shiftFunctor

added def CategoryTheory.DifferentialObject.shiftZero

added theorem CategoryTheory.DifferentialObject.zero_f

added structure CategoryTheory.DifferentialObject

added def CategoryTheory.Functor.mapDifferentialObject