[Merged by Bors] - feat(CategoryTheory/ObjectProperty): stability unfer finite products#34366
Conversation
PR summary 62a82d6d0aImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| suffices ∀ (J : Type) [Finite J], P.IsClosedUnderLimitsOfShape (Discrete J) from ⟨this⟩ | ||
| intro J _ | ||
| induction J using Finite.induction_empty_option with | ||
| | of_equiv e => | ||
| exact IsClosedUnderLimitsOfShape.of_equivalence (Discrete.equivalence e) | ||
| | h_empty => infer_instance | ||
| | h_option => | ||
| constructor | ||
| rintro X ⟨p⟩ | ||
| have hc : IsLimit | ||
| (BinaryFan.mk (Pi.lift (fun j ↦ p.π.app (.mk (some j)))) (p.π.app (.mk none))) := | ||
| BinaryFan.IsLimit.mk _ | ||
| (fun f₁ f₂ ↦ p.isLimit.lift (Cone.mk _ (Discrete.natTrans (fun ⟨j⟩ ↦ by | ||
| induction j with | ||
| | some j => exact f₁ ≫ Pi.π _ j | ||
| | none => exact f₂)))) | ||
| (fun _ _ ↦ by dsimp; ext; simp [p.isLimit.fac]) | ||
| (fun _ _ ↦ by simp [p.isLimit.fac]) | ||
| (fun f₁ f₂ l hl₁ hl₂ ↦ by | ||
| refine p.isLimit.hom_ext (fun ⟨j⟩ ↦ ?_) | ||
| induction j with | ||
| | some j => simp [p.isLimit.fac, ← hl₁] | ||
| | none => simpa [p.isLimit.fac]) | ||
| refine P.prop_of_isLimit hc ?_ | ||
| rintro ⟨_ | _⟩ | ||
| · exact P.prop_limit _ (fun _ ↦ p.prop_diag_obj _) | ||
| · exact p.prop_diag_obj _ |
There was a problem hiding this comment.
This seems overly complicated, I assume we already have API saying that P.IsClosedUnderLimitsOfShape J if and only if the inclusion functor from the full subcategory corresponding to P preserves limits of shape J. And we already have CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal which could then be used here
There was a problem hiding this comment.
Thanks for the suggestion! I have added the suitable API to make this work. There was an additional intricacy which is that I had to prove that the property of objects was stable under isomorphisms by using the terminal object and binary products https://github.com/joelriou/mathlib4/blob/48fcdc03eda8511de3b025bfb1e033b95609eaed/Mathlib/CategoryTheory/ObjectProperty/FiniteProducts.lean#L47
dagurtomas
added
the
awaiting-author
…3-object-property-finite-products
…3-object-property-finite-products
joelriou
removed
the
awaiting-author
robin-carlier
left a comment
robin-carlier
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by robin-carlier. |
ghost
added
the
maintainer-merge
ghost
added
ready-to-merge
…34366) We introduce typeclasses `IsClosedUnderBinaryProducts` and `IsClosedUnderFiniteProducts` expressing that `P : ObjectProperty C` is closed under binary products or finite products.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…eanprover-community#34366) We introduce typeclasses `IsClosedUnderBinaryProducts` and `IsClosedUnderFiniteProducts` expressing that `P : ObjectProperty C` is closed under binary products or finite products.
…eanprover-community#34366) We introduce typeclasses `IsClosedUnderBinaryProducts` and `IsClosedUnderFiniteProducts` expressing that `P : ObjectProperty C` is closed under binary products or finite products.
…eanprover-community#34366) We introduce typeclasses `IsClosedUnderBinaryProducts` and `IsClosedUnderFiniteProducts` expressing that `P : ObjectProperty C` is closed under binary products or finite products.
…eanprover-community#34366) We introduce typeclasses `IsClosedUnderBinaryProducts` and `IsClosedUnderFiniteProducts` expressing that `P : ObjectProperty C` is closed under binary products or finite products.
4 participants
We introduce typeclasses
IsClosedUnderBinaryProductsandIsClosedUnderFiniteProductsexpressing thatP : ObjectProperty Cis closed under binary products or finite products.