feat(CategoryTheory/Enriched/Limits): add HasConicalProducts

[joneugster]

Add the definition CategoryTheory.Enriched.Limits.HasConicalProducts.

Co-authored-by: Emily Riehl [email protected]
Co-authored-by: Dagur Asgeirsson [email protected]

---

• depends on: feat(CategoryTheory/Enriched/Limits): add HasConicalLimit #20907
• next PR: feat(CategoryTheory.Enriched.Limits): add HasConicalTerminal #20964
• full content: tracking(CategoryTheory/Enriched/Limits): add conical limits #20967
• source: feat: generalise conical limits emilyriehl/infinity-cosmos#78

[github-actions]

PR summary f10631f68c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Enriched.Limits.IsConicalLimit (new file)	602
Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits (new file)	603
Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts (new file)	604

---

Declarations diff

+ ConicalLimitCone
+ HasConicalLimit
+ HasConicalLimits
+ HasConicalLimitsOfShape
+ HasConicalLimitsOfSize
+ HasConicalProduct
+ HasConicalProducts
+ IsConicalLimit
+ conicalLimit
+ conicalLimitCone
+ eCoyoneda
+ getConicalLimitCone
+ hasConicalLimitEquivalenceComp
+ hasConicalLimitOfEquivalenceComp
+ hasConicalLimitsOfSize_of_univLE
+ hasLimit
+ hasLimitsOfSize
+ hasProducts
+ instance (priority := 100) : HasConicalLimit V F
+ instance (priority := 100) [HasConicalLimitsOfSize.{v₁, u₁} V C] : HasConicalLimitsOfShape J V C
+ instance (priority := 100) hasSmallestConicalLimitsOfHasConicalLimits :
+ instance : HasConicalLimitsOfShape J V C := HasConicalLimitsOfSize.hasConicalLimitsOfShape J
+ instance : HasLimitsOfShape J C
+ isConicalLimit
+ isIso_limitComparison
+ lift
+ lift_π
+ limitComparison
+ limitComparisonIso
+ limitComparison_eq_conePointUniqueUpToIso
+ mk
+ nonempty_isConicalLimit_iff
+ ofIsIsoLimitComparison
+ of_equiv
+ shrink
+ w
+ π
++ ofIso

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mo271]

Suggested change

	((h.isConicalLimit X).conePointUniqueUpToIso (limit.isLimit _)).hom := by
	apply limit.hom_ext
	simp [limitComparison]
	((h.isConicalLimit X).conePointUniqueUpToIso (limit.isLimit _)).hom := rfl

also seems to work

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(CategoryTheory/Enriched/Limits): add HasConicalLimit #20907
  By Dependent Issues (🤖). Happy coding!