Skip to content

feat(Condensed): the free light condensed module on ℕ∪∞ is internally projective#37449

Open
dagurtomas wants to merge 4 commits intoleanprover-community:masterfrom
dagurtomas:n-infty-internally-projective
Open

feat(Condensed): the free light condensed module on ℕ∪∞ is internally projective#37449
dagurtomas wants to merge 4 commits intoleanprover-community:masterfrom
dagurtomas:n-infty-internally-projective

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Mar 31, 2026 •
edited
Loading

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 31, 2026 •
edited
Loading

PR summary 69cbc416b3

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Condensed.Light.Epi 1966 2003 +37 (+1.88%)
Import changes for all files
Files Import difference
Mathlib.CategoryTheory.EffectiveEpi.Preserves 1
Mathlib.Condensed.Light.AB 27
Mathlib.Condensed.Light.Epi 37
Mathlib.Condensed.Light.Sequence (new file) 2054

Declarations diff

+ S'
+ S'_compactSpace
+ aux
+ cocone
+ cover
+ coverToFun
+ coverToFun_apply
+ coverToFun_surjective
+ factorsThru_lightProfinite_epi_of_epi
+ fibre
+ fibreIncl
+ fibreInclGeneral
+ fibreIncl_apply
+ fibre_incl
+ fibres
+ fibres_closed
+ fibres_compl_eq_iUnion
+ fibres_surjective
+ instance : (LightCondensed.forget R).IsRightAdjoint := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩
+ instance : (LightCondensed.free R).IsLeftAdjoint := ⟨_, ⟨LightCondensed.freeForgetAdjunction R⟩⟩
+ instance : Countable ℕ∪{∞} := (inferInstance : Countable <| Option _)
+ instance {X Y Z : LightProfinite} (f : X ⟶ Z) (g : Y ⟶ Z) [h : Epi f] :
+ mem_S'_iff
+ mem_fibres_iff
+ regularEpiOfPreserves
+ sectionOfFibreIncl
+ y
+ y_apply
+ y_continuous
+ y_surjective
+ π_r
+ π_r_apply

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

Increase in tech debt: (relative, absolute) = (6.00, 0.00)
Current number Change Type
6902 6 backward.isDefEq

Current commit 5f502f1e50
Reference commit 69cbc416b3

You can run this locally as

./scripts/reporting/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).

dagurtomas
dagurtomas commented Mar 31, 2026
View reviewed changes
dagurtomas
dagurtomas commented Mar 31, 2026
View reviewed changes
dagurtomas
dagurtomas commented Mar 31, 2026
View reviewed changes
dagurtomas
dagurtomas commented Mar 31, 2026
View reviewed changes
This was referenced Mar 31, 2026
Open
Open
Closed
Open
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 31, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 31, 2026 •
edited
Loading

This PR/issue depends on:

@dagurtomas dagurtomas changed the title feat(Condensed): the free light condensed module on ℕ∪∞ is internally projective feat(Condensed): the free light condensed module on `ℕ∪∞ is internally projective Apr 1, 2026
@dagurtomas dagurtomas changed the title feat(Condensed): the free light condensed module on `ℕ∪∞ is internally projective feat(Condensed): the free light condensed module on ℕ∪∞ is internally projective Apr 1, 2026
mathlib-bors bot pushed a commit that referenced this pull request Apr 2, 2026
@mathlib-splicebot @dagurtomas
chore(Mathlib/Condensed/Light/Module.lean): automated extraction (#37453
8db507d 
)

This PR was automatically created from PR #37449 by @dagurtomas via a [review comment](#37449 (comment)) by @dagurtomas.

Co-authored-by: dagurtomas <[email protected]>
Co-authored-by: Dagur Asgeirsson <[email protected]>
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Apr 2, 2026

This pull request has conflicts, please merge master and resolve them.

xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 3, 2026
@mathlib-splicebot @dagurtomas @xroblot
chore(Mathlib/Condensed/Light/Module.lean): automated extraction (lea…
f9315d3 
…nprover-community#37453)

This PR was automatically created from PR leanprover-community#37449 by @dagurtomas via a [review comment](leanprover-community#37449 (comment)) by @dagurtomas.

Co-authored-by: dagurtomas <[email protected]>
Co-authored-by: Dagur Asgeirsson <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

1 more reviewer

@mathlib-splicebot mathlib-splicebot[bot] mathlib-splicebot[bot] left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@dagurtomas