Commit 2024-07-07 14:27 2aeb41c5

View on Github →

feat: API for multiequalizers in the category of types (#14340) In this PR, we give a concrete characterization of limit multiforks in the category of types. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

added structure CategoryTheory.Limits.Types.MulticospanIndex.sections

added def CategoryTheory.Limits.Types.MulticospanIndex.sectionsEquiv

added theorem CategoryTheory.Limits.Types.Multifork.IsLimit.sectionsEquiv_apply_val

added theorem CategoryTheory.Limits.Types.Multifork.IsLimit.sectionsEquiv_symm_apply_val

added theorem CategoryTheory.Limits.Types.Multifork.isLimit_types_iff

added def CategoryTheory.Limits.Types.Multifork.toSections

added theorem CategoryTheory.Limits.Types.Multifork.toSections_fac