Skip to content
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

Jump to bottom

[Merged by Bors] - chore(Module/Torsion): drop DecidableEq assumptions #10253

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - chore(Module/Torsion): drop DecidableEq assumptions #10253

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0809e96
chore(LinearAlgebra,BigOperators): drop some decidability assumptions
urkud Feb 4, 2024
0e5ccc1
Fix
urkud Feb 4, 2024
02a8489
chore(Module/Torsion): drop `DecidableEq` assumption
urkud Feb 4, 2024
0509950
Merge branch 'YK-linalg-dec' into YK-module-torsion
urkud Feb 4, 2024
7c2dd1d
Merge branch 'master' into YK-module-torsion
urkud Feb 5, 2024
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
9 changes: 4 additions & 5 deletions Mathlib/Algebra/Module/Torsion.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -392,7 +392,7 @@ variable {ι : Type*} {p : ι → Ideal R} {S : Finset ι}
variable (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤)

-- Porting note: mem_iSup_finset_iff_exists_sum now requires DecidableEq ι
theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf [DecidableEq ι] :
theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf :
⨆ i ∈ S, torsionBySet R M (p i) = torsionBySet R M ↑(⨅ i ∈ S, p i) := by
rcases S.eq_empty_or_nonempty with h | h
· simp only [h]
Expand Down Expand Up @@ -430,7 +430,7 @@ theorem iSup_torsionBySet_ideal_eq_torsionBySet_iInf [DecidableEq ι] :
#align submodule.supr_torsion_by_ideal_eq_torsion_by_infi Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf

-- Porting note: iSup_torsionBySet_ideal_eq_torsionBySet_iInf now requires DecidableEq ι
theorem supIndep_torsionBySet_ideal [DecidableEq ι] : S.SupIndep fun i => torsionBySet R M <| p i :=
theorem supIndep_torsionBySet_ideal : S.SupIndep fun i => torsionBySet R M <| p i :=
fun T hT i hi hiT => by
rw [disjoint_iff, Finset.sup_eq_iSup,
iSup_torsionBySet_ideal_eq_torsionBySet_iInf fun i hi j hj ij => hp (hT hi) (hT hj) ij]
Expand All @@ -443,7 +443,7 @@ theorem supIndep_torsionBySet_ideal [DecidableEq ι] : S.SupIndep fun i => torsi

variable {q : ι → R} (hq : (S : Set ι).Pairwise <| (IsCoprime on q))

theorem iSup_torsionBy_eq_torsionBy_prod [DecidableEq ι] :
theorem iSup_torsionBy_eq_torsionBy_prod :
⨆ i ∈ S, torsionBy R M (q i) = torsionBy R M (∏ i in S, q i) := by
rw [← torsionBySet_span_singleton_eq, Ideal.submodule_span_eq, ←
Ideal.finset_inf_span_singleton _ _ hq, Finset.inf_eq_iInf, ←
Expand All @@ -456,8 +456,7 @@ theorem iSup_torsionBy_eq_torsionBy_prod [DecidableEq ι] :
exact fun i hi j hj ij => (Ideal.sup_eq_top_iff_isCoprime _ _).mpr (hq hi hj ij)
#align submodule.supr_torsion_by_eq_torsion_by_prod Submodule.iSup_torsionBy_eq_torsionBy_prod

-- Porting note: supIndep_torsionBySet_ideal now requires DecidableEq ι
theorem supIndep_torsionBy [DecidableEq ι] : S.SupIndep fun i => torsionBy R M <| q i := by
theorem supIndep_torsionBy : S.SupIndep fun i => torsionBy R M <| q i := by
convert supIndep_torsionBySet_ideal (M := M) fun i hi j hj ij =>
(Ideal.sup_eq_top_iff_isCoprime (q i) _).mpr <| hq hi hj ij
exact (torsionBySet_span_singleton_eq (R := R) (M := M) _).symm
Expand Down
Loading