Commit 2023-02-27 06:48 45462379

View on Github →

feat: port/CategoryTheory.Limits.IsLimit (#2354)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/IsLimit.lean

added def CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom

added theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac

added theorem CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone

added theorem CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac

added def CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone

added def CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone

added theorem CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_cooneOfHom

added def CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso

added theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc

added theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc

added def CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence

added def CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso

added theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc

added theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc

added theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom

added theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv

added theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom

added theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv

added def CategoryTheory.Limits.IsColimit.descCoconeMorphism

added theorem CategoryTheory.Limits.IsColimit.desc_self

added def CategoryTheory.Limits.IsColimit.equivIsoColimit

added theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_apply

added theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply

added def CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso

added theorem CategoryTheory.Limits.IsColimit.existsUnique

added def CategoryTheory.Limits.IsColimit.homIso'

added def CategoryTheory.Limits.IsColimit.homIso

added theorem CategoryTheory.Limits.IsColimit.homIso_hom

added theorem CategoryTheory.Limits.IsColimit.hom_desc

added theorem CategoryTheory.Limits.IsColimit.hom_ext

added theorem CategoryTheory.Limits.IsColimit.hom_isIso

added def CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism

added def CategoryTheory.Limits.IsColimit.map

added def CategoryTheory.Limits.IsColimit.mapCoconeEquiv

added def CategoryTheory.Limits.IsColimit.mkCoconeMorphism

added def CategoryTheory.Limits.IsColimit.natIso

added def CategoryTheory.Limits.IsColimit.ofCoconeEquiv

added theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc

added theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc

added def CategoryTheory.Limits.IsColimit.ofExistsUnique

added def CategoryTheory.Limits.IsColimit.ofFaithful

added def CategoryTheory.Limits.IsColimit.ofIsoColimit

added theorem CategoryTheory.Limits.IsColimit.ofIsoColimit_desc

added def CategoryTheory.Limits.IsColimit.ofLeftAdjoint

added def CategoryTheory.Limits.IsColimit.ofNatIso

added def CategoryTheory.Limits.IsColimit.ofPointIso

added def CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence

added def CategoryTheory.Limits.IsColimit.precomposeHomEquiv

added def CategoryTheory.Limits.IsColimit.precomposeInvEquiv

added theorem CategoryTheory.Limits.IsColimit.uniq_cocone_morphism

added def CategoryTheory.Limits.IsColimit.uniqueUpToIso

added def CategoryTheory.Limits.IsColimit.whiskerEquivalence

added def CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv

added theorem CategoryTheory.Limits.IsColimit.ι_map

added structure CategoryTheory.Limits.IsColimit

added def CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom

added theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac

added theorem CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone

added theorem CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac

added def CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone

added theorem CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom

added def CategoryTheory.Limits.IsLimit.OfNatIso.limitCone

added def CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso

added theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp

added theorem CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp

added def CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence

added def CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso

added theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp

added theorem CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp

added def CategoryTheory.Limits.IsLimit.equivIsoLimit

added theorem CategoryTheory.Limits.IsLimit.equivIsoLimit_apply

added theorem CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply

added def CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso

added theorem CategoryTheory.Limits.IsLimit.existsUnique

added def CategoryTheory.Limits.IsLimit.homIso'

added def CategoryTheory.Limits.IsLimit.homIso

added theorem CategoryTheory.Limits.IsLimit.homIso_hom

added theorem CategoryTheory.Limits.IsLimit.hom_ext

added theorem CategoryTheory.Limits.IsLimit.hom_isIso

added theorem CategoryTheory.Limits.IsLimit.hom_lift

added def CategoryTheory.Limits.IsLimit.isoUniqueConeMorphism

added def CategoryTheory.Limits.IsLimit.liftConeMorphism

added theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom

added theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv

added theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom

added theorem CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv

added theorem CategoryTheory.Limits.IsLimit.lift_self

added def CategoryTheory.Limits.IsLimit.map

added def CategoryTheory.Limits.IsLimit.mapConeEquiv

added theorem CategoryTheory.Limits.IsLimit.map_π

added def CategoryTheory.Limits.IsLimit.mkConeMorphism

added def CategoryTheory.Limits.IsLimit.natIso

added def CategoryTheory.Limits.IsLimit.ofConeEquiv

added theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc

added theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc

added def CategoryTheory.Limits.IsLimit.ofExistsUnique

added def CategoryTheory.Limits.IsLimit.ofFaithful

added def CategoryTheory.Limits.IsLimit.ofIsoLimit

added theorem CategoryTheory.Limits.IsLimit.ofIsoLimit_lift

added def CategoryTheory.Limits.IsLimit.ofNatIso

added def CategoryTheory.Limits.IsLimit.ofPointIso

added def CategoryTheory.Limits.IsLimit.ofRightAdjoint

added def CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence

added def CategoryTheory.Limits.IsLimit.postcomposeHomEquiv

added def CategoryTheory.Limits.IsLimit.postcomposeInvEquiv

added theorem CategoryTheory.Limits.IsLimit.uniq_cone_morphism

added def CategoryTheory.Limits.IsLimit.uniqueUpToIso

added def CategoryTheory.Limits.IsLimit.whiskerEquivalence

added def CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv

added structure CategoryTheory.Limits.IsLimit