Skip to content

Commit ca97f19

Browse files
YaelDilliesYaelDillies
committed
Adopt the module system
1 parent 78ecfcd commit ca97f19

File tree

14 files changed

+95
-41
lines changed

14 files changed

+95
-41
lines changed

‎PersistentDecomp.lean‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,15 @@
1-
import PersistentDecomp.BumpFunctor
2-
import PersistentDecomp.DirectSumDecomposition
3-
import PersistentDecomp.DirectSumDecompositionDual
4-
import PersistentDecomp.EndoRingIsLocal
5-
import PersistentDecomp.Mathlib.Algebra.DirectSum.Basic
6-
import PersistentDecomp.Mathlib.Algebra.Module.Submodule.Map
7-
import PersistentDecomp.Mathlib.Data.DFinsupp.BigOperators
8-
import PersistentDecomp.Mathlib.Order.Disjoint
9-
import PersistentDecomp.Mathlib.Order.Interval.Basic
10-
import PersistentDecomp.Mathlib.Order.SupIndep
11-
import PersistentDecomp.MaximalDecompExists
12-
import PersistentDecomp.Prereqs.Indecomposable
13-
import PersistentDecomp.Prereqs.PersistenceSubmodule
1+
module
2+
3+
public import PersistentDecomp.BumpFunctor
4+
public import PersistentDecomp.DirectSumDecomposition
5+
public import PersistentDecomp.DirectSumDecompositionDual
6+
public import PersistentDecomp.EndoRingIsLocal
7+
public import PersistentDecomp.Mathlib.Algebra.DirectSum.Basic
8+
public import PersistentDecomp.Mathlib.Algebra.Module.Submodule.Map
9+
public import PersistentDecomp.Mathlib.Data.DFinsupp.BigOperators
10+
public import PersistentDecomp.Mathlib.Order.Disjoint
11+
public import PersistentDecomp.Mathlib.Order.Interval.Basic
12+
public import PersistentDecomp.Mathlib.Order.SupIndep
13+
public import PersistentDecomp.MaximalDecompExists
14+
public import PersistentDecomp.Prereqs.Indecomposable
15+
public import PersistentDecomp.Prereqs.PersistenceSubmodule

‎PersistentDecomp/BumpFunctor.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
1-
import Mathlib.Algebra.Category.ModuleCat.Basic
2-
import Mathlib.Data.Real.Basic
3-
import PersistentDecomp.Mathlib.Order.Interval.Basic
1+
module
2+
3+
public import Mathlib.Algebra.Category.ModuleCat.Basic
4+
public import Mathlib.Data.Real.Basic
5+
public import PersistentDecomp.Mathlib.Order.Interval.Basic
46

57
/-!
68
# Bump Functors and Interval Modules
@@ -10,6 +12,8 @@ sends a subset `I` of `C` to some constant `d : D` and the complement of `I` to
1012
We then use this to construct interval modules.
1113
-/
1214

15+
@[expose] public section
16+
1317
open CategoryTheory CategoryTheory.Limits
1418

1519
universe u v

‎PersistentDecomp/DirectSumDecomposition.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
1-
import Mathlib.Algebra.DirectSum.Module
2-
import PersistentDecomp.Mathlib.Order.Disjoint
3-
import PersistentDecomp.Prereqs.Indecomposable
4-
import PersistentDecomp.Prereqs.PersistenceSubmodule
1+
module
2+
3+
public import Mathlib.Algebra.DirectSum.Module
4+
public import PersistentDecomp.Mathlib.Order.Disjoint
5+
public import PersistentDecomp.Prereqs.Indecomposable
6+
public import PersistentDecomp.Prereqs.PersistenceSubmodule
57

68
/-!
79
@@ -11,6 +13,8 @@ In this file, we define the type of direct sum decompositions of a persistence m
1113
This has a natural order given by refinements.
1214
-/
1315

16+
@[expose] public section
17+
1418
open CategoryTheory CategoryTheory.Limits DirectSum
1519
open CompleteLattice hiding sSup_le -- TODO: Fix in mathlib
1620

‎PersistentDecomp/DirectSumDecompositionDual.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
1-
import Mathlib.Algebra.DirectSum.Module
2-
import PersistentDecomp.Mathlib.Order.Disjoint
3-
import PersistentDecomp.Prereqs.Indecomposable
4-
import PersistentDecomp.Prereqs.PersistenceSubmodule
1+
module
2+
3+
public import Mathlib.Algebra.DirectSum.Module
4+
public import PersistentDecomp.Mathlib.Order.Disjoint
5+
public import PersistentDecomp.Prereqs.Indecomposable
6+
public import PersistentDecomp.Prereqs.PersistenceSubmodule
57

68
/-!
79
@@ -15,6 +17,8 @@ here, we are considering the *dual order* of the one constructed in the other fi
1517
1618
-/
1719

20+
@[expose] public section
21+
1822
open CategoryTheory CategoryTheory.Limits DirectSum
1923
open CompleteLattice hiding sSup_le -- TODO: Fix in mathlib
2024

‎PersistentDecomp/EndoRingIsLocal.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1-
import Mathlib.Algebra.Category.ModuleCat.Abelian
2-
import Mathlib.RingTheory.Artinian.Module
1+
module
2+
3+
public import Mathlib.Algebra.Category.ModuleCat.Abelian
4+
public import Mathlib.RingTheory.Artinian.Module
35

46
/-!
57
Work left to do
@@ -30,6 +32,8 @@ exact definition of large products of persistence modules. However, we will need
3032
look into this at some point - it's required to finish the proof of step 2.
3133
-/
3234

35+
public section
36+
3337
open CategoryTheory Filter
3438

3539
universe u

‎PersistentDecomp/Mathlib/Algebra/DirectSum/Basic.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
import Mathlib.Algebra.DirectSum.Decomposition
2-
import Mathlib.Algebra.Group.Subgroup.Basic
1+
module
2+
3+
public import Mathlib.Algebra.DirectSum.Decomposition
4+
public import Mathlib.Algebra.Group.Subgroup.Basic
5+
6+
public section
37

48
namespace DirectSum
59
variable {ι M S : Type*} [DecidableEq ι] [AddCommGroup M] [SetLike S M] [AddSubgroupClass S M]

‎PersistentDecomp/Mathlib/Algebra/Module/Submodule/Map.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1-
import Mathlib.Algebra.Module.Submodule.Map
1+
module
2+
3+
public import Mathlib.Algebra.Module.Submodule.Map
4+
5+
public section
26

37
variable {R : Type*} {R₂ : Type*}
48
variable {M : Type*} {M₂ : Type*}

‎PersistentDecomp/Mathlib/Data/DFinsupp/BigOperators.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1-
import Mathlib.Data.DFinsupp.BigOperators
1+
module
2+
3+
public import Mathlib.Data.DFinsupp.BigOperators
4+
5+
public section
26

37
@[to_additive (attr := simp)]
48
lemma SubmonoidClass.coe_dfinsuppProd {B ι N : Type*} {M : ι → Type*} [DecidableEq ι]

‎PersistentDecomp/Mathlib/Order/Disjoint.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1-
import Mathlib.Order.Disjoint
1+
module
2+
3+
public import Mathlib.Order.Disjoint
4+
5+
public section
26

37
theorem right_lt_sup_of_left_ne_bot {α : Type*} [SemilatticeSup α] [OrderBot α] {a b : α}
48
(h : Disjoint a b) (ha : a ≠ ⊥) : b < a ⊔ b :=

‎PersistentDecomp/Mathlib/Order/Interval/Basic.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
1-
import Mathlib.Order.Interval.Basic
2-
import Mathlib.Order.Interval.Set.OrdConnected
1+
module
2+
3+
public import Mathlib.Order.Interval.Basic
4+
public import Mathlib.Order.Interval.Set.OrdConnected
5+
6+
public section
37

48
open Set
59

0 commit comments

Comments
 (0)