Skip to content

[Merged by Bors] - feat(CategoryTheory/Final): improve assumptions for final_fst#30655

Closed
joelriou wants to merge 5 commits intoleanprover-community:masterfrom
joelriou:final-connected
Closed

[Merged by Bors] - feat(CategoryTheory/Final): improve assumptions for final_fst#30655
joelriou wants to merge 5 commits intoleanprover-community:masterfrom
joelriou:final-connected

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Oct 18, 2025

We show that the projection C × D ⥤ C is a final (or initial) functor when D is connected. (Before this PR, it was proven under the stronger assumption that D was (co)filtered.)

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Oct 18, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 18, 2025 •
edited
Loading

PR summary aa78411076

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
68 files Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicTopology.RelativeCellComplex.Basic Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Comma.Final Mathlib.CategoryTheory.Filtered.Final Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Limits.Constructions.Over.Basic Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.FinallySmall Mathlib.CategoryTheory.Limits.Indization.Category Mathlib.CategoryTheory.Limits.Indization.Equalizers Mathlib.CategoryTheory.Limits.Indization.FilteredColimits Mathlib.CategoryTheory.Limits.Indization.IndObject Mathlib.CategoryTheory.Limits.Indization.LocallySmall Mathlib.CategoryTheory.Limits.Indization.ParallelPair Mathlib.CategoryTheory.Limits.Indization.Products Mathlib.CategoryTheory.Limits.MorphismProperty Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition Mathlib.CategoryTheory.MorphismProperty.FunctorCategory Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.SmallObject.Basic Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting Mathlib.CategoryTheory.SmallObject.TransfiniteIteration Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Order.Interval.Set.Final Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.Profinite.Extend
 2
Mathlib.CategoryTheory.Discrete.StructuredArrow (new file) 426
Mathlib.CategoryTheory.Limits.Final.Connected (new file) 640

Declarations diff

+ costructuredArrowEquivalenceOfUnique
+ instance (F : C ⥤ Discrete T) [IsConnected C] : F.Final := by
+ instance (F : C ⥤ Discrete T) [IsConnected C] : F.Initial := by
+ instance [F.Initial] [G.Initial] : (F.prod G).Initial
+ isConnected_iff_final_of_unique
+ isConnected_iff_initial_of_unique
+ structuredArrowEquivalenceOfUnique
++- final_fst
++- final_snd
+-+ initial_fst
+-+ initial_snd

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).

kim-em
kim-em reviewed Oct 29, 2025
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Oct 29, 2025

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 29, 2025
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 29, 2025

Thanks very much @kim-em for the reviews!

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Oct 29, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 29, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@joelriou
feat(CategoryTheory/Final): improve assumptions for final_fst (#30655)
6f28114 
We show that the projection `C × D ⥤ C` is a final (or initial) functor when `D` is connected. (Before this PR, it was proven under the stronger assumption that `D` was (co)filtered.)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Final): improve assumptions for final_fst [Merged by Bors] - feat(CategoryTheory/Final): improve assumptions for final_fst Oct 29, 2025
@mathlib-bors mathlib-bors bot closed this Oct 29, 2025
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@joelriou @BeibeiX0
feat(CategoryTheory/Final): improve assumptions for final_fst (lean…
d7f012b 
…prover-community#30655)

We show that the projection `C × D ⥤ C` is a final (or initial) functor when `D` is connected. (Before this PR, it was proven under the stronger assumption that `D` was (co)filtered.)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

@adamtopaz adamtopaz

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @kim-em @adamtopaz