Commit 2023-02-24 19:54 332c3c9f

View on Github →

feat: port/CategoryTheory.Limits.Cones (#2337)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Cones.lean

added def CategoryTheory.Functor.cocones

added def CategoryTheory.Functor.cones

added def CategoryTheory.Functor.functorialityCompPostcompose

added def CategoryTheory.Functor.functorialityCompPrecompose

added def CategoryTheory.Functor.mapCocone

added def CategoryTheory.Functor.mapCoconeInv

added def CategoryTheory.Functor.mapCoconeInvMapCocone

added def CategoryTheory.Functor.mapCoconeMapCoconeInv

added def CategoryTheory.Functor.mapCoconeMorphism

added def CategoryTheory.Functor.mapCoconeOp

added def CategoryTheory.Functor.mapCoconePrecompose

added def CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor

added def CategoryTheory.Functor.mapCoconeWhisker

added def CategoryTheory.Functor.mapCone

added def CategoryTheory.Functor.mapConeInv

added def CategoryTheory.Functor.mapConeInvMapCone

added def CategoryTheory.Functor.mapConeMapConeInv

added def CategoryTheory.Functor.mapConeMorphism

added def CategoryTheory.Functor.mapConeOp

added def CategoryTheory.Functor.mapConePostcompose

added def CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor

added def CategoryTheory.Functor.mapConeWhisker

added def CategoryTheory.Functor.postcomposeWhiskerLeftMapCone

added def CategoryTheory.Functor.precomposeWhiskerLeftMapCocone

added def CategoryTheory.Limits.Cocone.equiv

added def CategoryTheory.Limits.Cocone.extend

added def CategoryTheory.Limits.Cocone.extensions

added def CategoryTheory.Limits.Cocone.op

added def CategoryTheory.Limits.Cocone.unop

added theorem CategoryTheory.Limits.Cocone.w

added def CategoryTheory.Limits.Cocone.whisker

added structure CategoryTheory.Limits.Cocone

added structure CategoryTheory.Limits.CoconeMorphism

added theorem CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso

added def CategoryTheory.Limits.Cocones.equivalenceOfReindexing

added def CategoryTheory.Limits.Cocones.eta

added def CategoryTheory.Limits.Cocones.ext

added def CategoryTheory.Limits.Cocones.forget

added def CategoryTheory.Limits.Cocones.functoriality

added def CategoryTheory.Limits.Cocones.functorialityEquivalence

added def CategoryTheory.Limits.Cocones.precompose

added def CategoryTheory.Limits.Cocones.precomposeComp

added def CategoryTheory.Limits.Cocones.precomposeEquivalence

added def CategoryTheory.Limits.Cocones.precomposeId

added def CategoryTheory.Limits.Cocones.whiskering

added def CategoryTheory.Limits.Cocones.whiskeringEquivalence

added def CategoryTheory.Limits.Cone.equiv

added def CategoryTheory.Limits.Cone.extend

added def CategoryTheory.Limits.Cone.extensions

added def CategoryTheory.Limits.Cone.op

added def CategoryTheory.Limits.Cone.unop

added theorem CategoryTheory.Limits.Cone.w

added def CategoryTheory.Limits.Cone.whisker

added structure CategoryTheory.Limits.Cone

added structure CategoryTheory.Limits.ConeMorphism

added theorem CategoryTheory.Limits.Cones.cone_iso_of_hom_iso

added def CategoryTheory.Limits.Cones.equivalenceOfReindexing

added def CategoryTheory.Limits.Cones.eta

added def CategoryTheory.Limits.Cones.ext

added def CategoryTheory.Limits.Cones.forget

added def CategoryTheory.Limits.Cones.functoriality

added def CategoryTheory.Limits.Cones.functorialityEquivalence

added def CategoryTheory.Limits.Cones.postcompose

added def CategoryTheory.Limits.Cones.postcomposeComp

added def CategoryTheory.Limits.Cones.postcomposeEquivalence

added def CategoryTheory.Limits.Cones.postcomposeId

added def CategoryTheory.Limits.Cones.whiskering

added def CategoryTheory.Limits.Cones.whiskeringEquivalence

added def CategoryTheory.Limits.coconeEquivalenceOpConeOp

added def CategoryTheory.Limits.coconeLeftOpOfCone

added def CategoryTheory.Limits.coconeOfConeLeftOp

added theorem CategoryTheory.Limits.coconeOfConeLeftOp_ι_app

added def CategoryTheory.Limits.coconeOfConeRightOp

added def CategoryTheory.Limits.coconeOfConeUnop

added def CategoryTheory.Limits.coconeRightOpOfCone

added def CategoryTheory.Limits.coconeUnopOfCone

added def CategoryTheory.Limits.coneLeftOpOfCocone

added def CategoryTheory.Limits.coneOfCoconeLeftOp

added def CategoryTheory.Limits.coneOfCoconeRightOp

added def CategoryTheory.Limits.coneOfCoconeUnop

added def CategoryTheory.Limits.coneRightOpOfCocone

added def CategoryTheory.Limits.coneUnopOfCocone

added def CategoryTheory.cocones

added def CategoryTheory.cones