Skip to content

bump mathlib #9

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dagurtomas merged 1 commit into from
Jan 28, 2026
Merged

bump mathlib #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 0 additions & 2 deletions LeanCondensed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,9 @@ import LeanCondensed.Mathlib.CategoryTheory.Sites.DirectImage
import LeanCondensed.Mathlib.Condensed.Adjunctions
import LeanCondensed.Mathlib.Condensed.Light.Limits
import LeanCondensed.Mathlib.Condensed.Light.Monoidal
import LeanCondensed.Mathlib.Topology.Category.CompHausLike.Limits
import LeanCondensed.Projects.Epi
import LeanCondensed.Projects.FreeCondensed
import LeanCondensed.Projects.IsLocalizedMonoidal
import LeanCondensed.Projects.LightProfiniteInjective
import LeanCondensed.Projects.LightSolid
import LeanCondensed.Projects.MonoidalLinear
import LeanCondensed.Projects.PreservesCoprod
Expand Down
29 changes: 0 additions & 29 deletions LeanCondensed/Mathlib/Topology/Category/CompHausLike/Limits.lean
View file
Open in desktop

This file was deleted.

7 changes: 6 additions & 1 deletion LeanCondensed/Projects/Epi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,12 @@ import Mathlib.Combinatorics.Quiver.ReflQuiver
import Mathlib.Condensed.Light.Epi
import Mathlib.Condensed.Light.Explicit
import Mathlib.Condensed.Light.Functors
import Mathlib.Topology.Compactness.PseudometrizableLindelof
import Mathlib.Data.Finset.Attr
import Mathlib.Tactic.Common
import Mathlib.Tactic.Continuity
import Mathlib.Tactic.Finiteness.Attr
import Mathlib.Tactic.SetLike
import Mathlib.Util.CompileInductive
import Mathlib.Topology.Connected.Separation
import Mathlib.Topology.Spectral.Prespectral

Expand Down
4 changes: 3 additions & 1 deletion LeanCondensed/Projects/FreeCondensed.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,9 @@ def profiniteComponent (S : LightProfinite.{0}) (c : ℤ) : LightProfinite :=

def _root_.lightProfiniteToSequential : LightProfinite ⥤ Sequential where
obj X := Sequential.of X
map f := f
map f := ConcreteCategory.ofHom ⟨f, by continuity⟩
map_id := sorry
map_comp := sorry

-- This functor should probably be defined as a right Kan extension of the analogous functor to
-- `FintypeCat`, similarly to `Condensed.profiniteSolid`, defined in `Mathlib.Condensed.Solid`.
Expand Down
Loading