Skip to content

Commit 46c2efe

Browse files
VierkantorVierkantor
committed
chore: small splits of RingTheory.Ideal.Operations; clean imports (#12090)
This is based on seeing the import `RingTheory.Ideal.Operations` → `LinearAlgebra.Basis` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` is a bit of a chokepoint for compiling Mathlib since it imports many files and is imported by many files. So splitting out a few obvious parts should help with compile times. Moreover, there are a bunch of imports that I could remove and have the file still compile: presumably these are (were) transitive dependencies that shake does not remove. The following results and their corollaries were split off: * `Ideal.basisSpanSingleton` * `Basis.mem_ideal_iff` * `Ideal.colon` In particular, now `Ideal.Operations` should no longer need to know about `Basis` or submodule quotients.
1 parent c641f2b commit 46c2efe

File tree

12 files changed

+175
-135
lines changed

12 files changed

+175
-135
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3370,6 +3370,8 @@ import Mathlib.RingTheory.Henselian
33703370
import Mathlib.RingTheory.HopfAlgebra
33713371
import Mathlib.RingTheory.Ideal.AssociatedPrime
33723372
import Mathlib.RingTheory.Ideal.Basic
3373+
import Mathlib.RingTheory.Ideal.Basis
3374+
import Mathlib.RingTheory.Ideal.Colon
33733375
import Mathlib.RingTheory.Ideal.Cotangent
33743376
import Mathlib.RingTheory.Ideal.IdempotentFG
33753377
import Mathlib.RingTheory.Ideal.LocalRing

‎Mathlib/Algebra/Algebra/Subalgebra/Basic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Yury Kudryashov
55
-/
66
import Mathlib.Algebra.Algebra.Basic
7+
import Mathlib.Algebra.Algebra.Prod
78
import Mathlib.Data.Set.UnionLift
89
import Mathlib.LinearAlgebra.Finsupp
910
import Mathlib.RingTheory.Ideal.Operations

‎Mathlib/LinearAlgebra/FreeModule/IdealQuotient.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
77
import Mathlib.LinearAlgebra.FreeModule.PID
88
import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
99
import Mathlib.LinearAlgebra.QuotientPi
10+
import Mathlib.RingTheory.Ideal.Basis
1011

1112
#align_import linear_algebra.free_module.ideal_quotient from "leanprover-community/mathlib"@"90b0d53ee6ffa910e5c2a977ce7e2fc704647974"
1213

‎Mathlib/RingTheory/Adjoin/Basic.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Kenny Lau
55
-/
66
import Mathlib.Algebra.Algebra.Operations
77
import Mathlib.Algebra.Algebra.Subalgebra.Tower
8+
import Mathlib.LinearAlgebra.Basis
89
import Mathlib.LinearAlgebra.Prod
910
import Mathlib.LinearAlgebra.Finsupp
1011

‎Mathlib/RingTheory/HahnSeries/Multiplication.lean‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ Copyright (c) 2021 Aaron Anderson. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Aaron Anderson, Scott Carnahan
55
-/
6-
import Mathlib.Algebra.BigOperators.Finprod
76
import Mathlib.RingTheory.HahnSeries.Addition
87
import Mathlib.Algebra.Algebra.Subalgebra.Basic
98
import Mathlib.Data.Finset.MulAntidiagonal

‎Mathlib/RingTheory/HahnSeries/Summable.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Copyright (c) 2021 Aaron Anderson. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Aaron Anderson
55
-/
6-
import Mathlib.RingTheory.HahnSeries.Multiplication
6+
import Mathlib.Algebra.BigOperators.Finprod
77
import Mathlib.Algebra.EuclideanDomain.Instances
88
import Mathlib.Algebra.Order.Group.WithTop
9+
import Mathlib.RingTheory.HahnSeries.Multiplication
910
import Mathlib.RingTheory.Valuation.Basic
1011

1112
#align_import ring_theory.hahn_series from "leanprover-community/mathlib"@"a484a7d0eade4e1268f4fb402859b6686037f965"

‎Mathlib/RingTheory/Ideal/Basis.lean‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
/-
2+
Copyright (c) 2018 Kenny Lau. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Anne Baanen
5+
-/
6+
import Mathlib.Algebra.Algebra.Bilinear
7+
import Mathlib.LinearAlgebra.Basis
8+
import Mathlib.RingTheory.Ideal.Basic
9+
10+
#align_import ring_theory.ideal.operations from "leanprover-community/mathlib"@"e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74"
11+
12+
/-!
13+
# The basis of ideals
14+
15+
Some results involving `Ideal` and `Basis`.
16+
-/
17+
18+
open BigOperators
19+
20+
namespace Ideal
21+
22+
variable {ι R S : Type*} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S]
23+
24+
/-- A basis on `S` gives a basis on `Ideal.span {x}`, by multiplying everything by `x`. -/
25+
noncomputable def basisSpanSingleton (b : Basis ι R S) {x : S} (hx : x ≠ 0) :
26+
Basis ι R (span ({x} : Set S)) :=
27+
b.map <|
28+
LinearEquiv.ofInjective (Algebra.lmul R S x) (LinearMap.mul_injective hx) ≪≫ₗ
29+
LinearEquiv.ofEq _ _
30+
(by
31+
ext
32+
simp [mem_span_singleton', mul_comm]) ≪≫ₗ
33+
(Submodule.restrictScalarsEquiv R S S (Ideal.span ({x} : Set S))).restrictScalars R
34+
#align ideal.basis_span_singleton Ideal.basisSpanSingleton
35+
36+
@[simp]
37+
theorem basisSpanSingleton_apply (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι) :
38+
(basisSpanSingleton b hx i : S) = x * b i := by
39+
simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply,
40+
Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply,
41+
LinearEquiv.restrictScalars_apply, Algebra.coe_lmul_eq_mul, LinearMap.mul_apply']
42+
-- This used to be the end of the proof before leanprover/lean4#2644
43+
erw [LinearEquiv.coe_ofEq_apply, LinearEquiv.ofInjective_apply, Algebra.coe_lmul_eq_mul,
44+
LinearMap.mul_apply']
45+
#align ideal.basis_span_singleton_apply Ideal.basisSpanSingleton_apply
46+
47+
@[simp]
48+
theorem constr_basisSpanSingleton {N : Type*} [Semiring N] [Module N S] [SMulCommClass R N S]
49+
(b : Basis ι R S) {x : S} (hx : x ≠ 0) :
50+
(b.constr N).toFun (((↑) : _ → S) ∘ (basisSpanSingleton b hx)) = Algebra.lmul R S x :=
51+
b.ext fun i => by
52+
erw [Basis.constr_basis, Function.comp_apply, basisSpanSingleton_apply, LinearMap.mul_apply']
53+
#align ideal.constr_basis_span_singleton Ideal.constr_basisSpanSingleton
54+
55+
end Ideal
56+
57+
-- Porting note: added explicit coercion `(b i : S)`
58+
/-- If `I : Ideal S` has a basis over `R`,
59+
`x ∈ I` iff it is a linear combination of basis vectors. -/
60+
theorem Basis.mem_ideal_iff {ι R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal S}
61+
(b : Basis ι R I) {x : S} : x ∈ I ↔ ∃ c : ι →₀ R, x = Finsupp.sum c fun i x => x • (b i : S) :=
62+
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff
63+
#align basis.mem_ideal_iff Basis.mem_ideal_iff
64+
65+
/-- If `I : Ideal S` has a finite basis over `R`,
66+
`x ∈ I` iff it is a linear combination of basis vectors. -/
67+
theorem Basis.mem_ideal_iff' {ι R S : Type*} [Fintype ι] [CommRing R] [CommRing S] [Algebra R S]
68+
{I : Ideal S} (b : Basis ι R I) {x : S} : x ∈ I ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : S) :=
69+
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff'
70+
#align basis.mem_ideal_iff' Basis.mem_ideal_iff'

‎Mathlib/RingTheory/Ideal/Colon.lean‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
/-
2+
Copyright (c) 2018 Kenny Lau. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Kenny Lau
5+
-/
6+
import Mathlib.LinearAlgebra.Quotient
7+
import Mathlib.RingTheory.Ideal.Operations
8+
9+
/-!
10+
# The colon ideal
11+
12+
This file defines `Submodule.colon N P` as the ideal of all elements `r : R` such that `r • P ⊆ N`.
13+
The normal notation for this would be `N : P` which has already been taken by type theory.
14+
15+
-/
16+
17+
namespace Submodule
18+
19+
open BigOperators Pointwise
20+
21+
variable {R M M' F G : Type*} [CommRing R] [AddCommGroup M] [Module R M]
22+
variable {N N₁ N₂ P P₁ P₂ : Submodule R M}
23+
24+
/-- `N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`. -/
25+
def colon (N P : Submodule R M) : Ideal R :=
26+
annihilator (P.map N.mkQ)
27+
#align submodule.colon Submodule.colon
28+
29+
theorem mem_colon {r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N :=
30+
mem_annihilator.trans
31+
⟨fun H p hp => (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
32+
fun H _ ⟨p, hp, hpm⟩ => hpm ▸ (N.mkQ.map_smul r p ▸ (Quotient.mk_eq_zero N).2 <| H p hp)⟩
33+
#align submodule.mem_colon Submodule.mem_colon
34+
35+
theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N :=
36+
mem_colon
37+
#align submodule.mem_colon' Submodule.mem_colon'
38+
39+
@[simp]
40+
theorem colon_top {I : Ideal R} : I.colon ⊤ = I := by
41+
simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
42+
exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩
43+
44+
@[simp]
45+
theorem colon_bot : colon ⊥ N = N.annihilator := by
46+
simp_rw [SetLike.ext_iff, mem_colon, mem_annihilator, mem_bot, forall_const]
47+
48+
theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ := fun _ hrnp =>
49+
mem_colon.2 fun p₁ hp₁ => hn <| mem_colon.1 hrnp p₁ <| hp hp₁
50+
#align submodule.colon_mono Submodule.colon_mono
51+
52+
theorem iInf_colon_iSup (ι₁ : Sort*) (f : ι₁ → Submodule R M) (ι₂ : Sort*)
53+
(g : ι₂ → Submodule R M) : (⨅ i, f i).colon (⨆ j, g j) = ⨅ (i) (j), (f i).colon (g j) :=
54+
le_antisymm (le_iInf fun _ => le_iInf fun _ => colon_mono (iInf_le _ _) (le_iSup _ _)) fun _ H =>
55+
mem_colon'.2 <|
56+
iSup_le fun j =>
57+
map_le_iff_le_comap.1 <|
58+
le_iInf fun i =>
59+
map_le_iff_le_comap.2 <|
60+
mem_colon'.1 <|
61+
have := (mem_iInf _).1 H i
62+
have := (mem_iInf _).1 this j
63+
this
64+
#align submodule.infi_colon_supr Submodule.iInf_colon_iSup
65+
66+
@[simp]
67+
theorem mem_colon_singleton {N : Submodule R M} {x : M} {r : R} :
68+
r ∈ N.colon (Submodule.span R {x}) ↔ r • x ∈ N :=
69+
calc
70+
r ∈ N.colon (Submodule.span R {x}) ↔ ∀ a : R, r • a • x ∈ N := by
71+
simp [Submodule.mem_colon, Submodule.mem_span_singleton]
72+
_ ↔ r • x ∈ N := by simp_rw [fun (a : R) ↦ smul_comm r a x]; exact SetLike.forall_smul_mem_iff
73+
#align submodule.mem_colon_singleton Submodule.mem_colon_singleton
74+
75+
@[simp]
76+
theorem _root_.Ideal.mem_colon_singleton {I : Ideal R} {x r : R} :
77+
r ∈ I.colon (Ideal.span {x}) ↔ r * x ∈ I := by
78+
simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]
79+
#align ideal.mem_colon_singleton Ideal.mem_colon_singleton
80+
81+
theorem annihilator_quotient {N : Submodule R M} :
82+
Module.annihilator R (M ⧸ N) = N.colon ⊤ := by
83+
simp_rw [SetLike.ext_iff, Module.mem_annihilator, colon, mem_annihilator, map_top,
84+
LinearMap.range_eq_top.mpr (mkQ_surjective N), mem_top, forall_true_left, forall_const]
85+
86+
theorem _root_.Ideal.annihilator_quotient {I : Ideal R} : Module.annihilator R (R ⧸ I) = I := by
87+
rw [Submodule.annihilator_quotient, colon_top]
88+
89+
end Submodule

‎Mathlib/RingTheory/Ideal/Norm.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ import Mathlib.Data.Int.Associated
1111
import Mathlib.LinearAlgebra.FreeModule.Determinant
1212
import Mathlib.LinearAlgebra.FreeModule.IdealQuotient
1313
import Mathlib.RingTheory.DedekindDomain.PID
14+
import Mathlib.RingTheory.Ideal.Basis
1415
import Mathlib.RingTheory.LocalProperties
1516
import Mathlib.RingTheory.Localization.NormTrace
1617

‎Mathlib/RingTheory/Ideal/Operations.lean‎

Lines changed: 3 additions & 130 deletions
Original file line numberDiff line numberDiff line change
@@ -5,22 +5,19 @@ Authors: Kenny Lau
55
-/
66
import Mathlib.Algebra.Algebra.Operations
77
import Mathlib.Algebra.Ring.Equiv
8-
import Mathlib.Data.Nat.Choose.Sum
9-
import Mathlib.Data.Nat.Interval
108
import Mathlib.Data.Fintype.Lattice
119
import Mathlib.RingTheory.Coprime.Lemmas
1210
import Mathlib.RingTheory.Ideal.Basic
13-
import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
14-
import Mathlib.LinearAlgebra.Basis
15-
import Mathlib.LinearAlgebra.Quotient
16-
import Mathlib.Algebra.Order.Group.Action
1711

1812
#align_import ring_theory.ideal.operations from "leanprover-community/mathlib"@"e7f0ddbf65bd7181a85edb74b64bdc35ba4bdc74"
1913

2014
/-!
2115
# More operations on modules and ideals
2216
-/
2317

18+
assert_not_exists Basis -- See `RingTheory.Ideal.Basis`
19+
assert_not_exists Submodule.hasQuotient -- See `RingTheory.Ideal.QuotientOperations`
20+
2421
universe u v w x
2522

2623
open BigOperators Pointwise
@@ -386,78 +383,6 @@ theorem smul_comap_le_comap_smul (f : M →ₗ[R] M') (S : Submodule R M') (I :
386383

387384
end CommSemiring
388385

389-
section CommRing
390-
391-
variable [CommRing R] [AddCommGroup M] [Module R M]
392-
variable {N N₁ N₂ P P₁ P₂ : Submodule R M}
393-
394-
/-- `N.colon P` is the ideal of all elements `r : R` such that `r • P ⊆ N`. -/
395-
def colon (N P : Submodule R M) : Ideal R :=
396-
annihilator (P.map N.mkQ)
397-
#align submodule.colon Submodule.colon
398-
399-
theorem mem_colon {r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N :=
400-
mem_annihilator.trans
401-
⟨fun H p hp => (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
402-
fun H _ ⟨p, hp, hpm⟩ => hpm ▸ (N.mkQ.map_smul r p ▸ (Quotient.mk_eq_zero N).2 <| H p hp)⟩
403-
#align submodule.mem_colon Submodule.mem_colon
404-
405-
theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N :=
406-
mem_colon
407-
#align submodule.mem_colon' Submodule.mem_colon'
408-
409-
@[simp]
410-
theorem colon_top {I : Ideal R} : I.colon ⊤ = I := by
411-
simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
412-
exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩
413-
414-
@[simp]
415-
theorem colon_bot : colon ⊥ N = N.annihilator := by
416-
simp_rw [SetLike.ext_iff, mem_colon, mem_annihilator, mem_bot, forall_const]
417-
418-
theorem colon_mono (hn : N₁ ≤ N₂) (hp : P₁ ≤ P₂) : N₁.colon P₂ ≤ N₂.colon P₁ := fun _ hrnp =>
419-
mem_colon.2 fun p₁ hp₁ => hn <| mem_colon.1 hrnp p₁ <| hp hp₁
420-
#align submodule.colon_mono Submodule.colon_mono
421-
422-
theorem iInf_colon_iSup (ι₁ : Sort w) (f : ι₁ → Submodule R M) (ι₂ : Sort x)
423-
(g : ι₂ → Submodule R M) : (⨅ i, f i).colon (⨆ j, g j) = ⨅ (i) (j), (f i).colon (g j) :=
424-
le_antisymm (le_iInf fun _ => le_iInf fun _ => colon_mono (iInf_le _ _) (le_iSup _ _)) fun _ H =>
425-
mem_colon'.2 <|
426-
iSup_le fun j =>
427-
map_le_iff_le_comap.1 <|
428-
le_iInf fun i =>
429-
map_le_iff_le_comap.2 <|
430-
mem_colon'.1 <|
431-
have := (mem_iInf _).1 H i
432-
have := (mem_iInf _).1 this j
433-
this
434-
#align submodule.infi_colon_supr Submodule.iInf_colon_iSup
435-
436-
@[simp]
437-
theorem mem_colon_singleton {N : Submodule R M} {x : M} {r : R} :
438-
r ∈ N.colon (Submodule.span R {x}) ↔ r • x ∈ N :=
439-
calc
440-
r ∈ N.colon (Submodule.span R {x}) ↔ ∀ a : R, r • a • x ∈ N := by
441-
simp [Submodule.mem_colon, Submodule.mem_span_singleton]
442-
_ ↔ r • x ∈ N := by simp_rw [fun (a : R) ↦ smul_comm r a x]; exact SetLike.forall_smul_mem_iff
443-
#align submodule.mem_colon_singleton Submodule.mem_colon_singleton
444-
445-
@[simp]
446-
theorem _root_.Ideal.mem_colon_singleton {I : Ideal R} {x r : R} :
447-
r ∈ I.colon (Ideal.span {x}) ↔ r * x ∈ I := by
448-
simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]
449-
#align ideal.mem_colon_singleton Ideal.mem_colon_singleton
450-
451-
theorem annihilator_quotient {N : Submodule R M} :
452-
Module.annihilator R (M ⧸ N) = N.colon ⊤ := by
453-
simp_rw [SetLike.ext_iff, Module.mem_annihilator, colon, mem_annihilator, map_top,
454-
LinearMap.range_eq_top.mpr (mkQ_surjective N), mem_top, forall_true_left, forall_const]
455-
456-
theorem _root_.Ideal.annihilator_quotient {I : Ideal R} : Module.annihilator R (R ⧸ I) = I := by
457-
rw [Submodule.annihilator_quotient, colon_top]
458-
459-
end CommRing
460-
461386
end Submodule
462387

463388
namespace Ideal
@@ -2030,43 +1955,6 @@ theorem range_finsuppTotal :
20301955

20311956
end Total
20321957

2033-
section Basis
2034-
2035-
variable {ι R S : Type*} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S]
2036-
2037-
/-- A basis on `S` gives a basis on `Ideal.span {x}`, by multiplying everything by `x`. -/
2038-
noncomputable def basisSpanSingleton (b : Basis ι R S) {x : S} (hx : x ≠ 0) :
2039-
Basis ι R (span ({x} : Set S)) :=
2040-
b.map <|
2041-
LinearEquiv.ofInjective (Algebra.lmul R S x) (LinearMap.mul_injective hx) ≪≫ₗ
2042-
LinearEquiv.ofEq _ _
2043-
(by
2044-
ext
2045-
simp [mem_span_singleton', mul_comm]) ≪≫ₗ
2046-
(Submodule.restrictScalarsEquiv R S S (Ideal.span ({x} : Set S))).restrictScalars R
2047-
#align ideal.basis_span_singleton Ideal.basisSpanSingleton
2048-
2049-
@[simp]
2050-
theorem basisSpanSingleton_apply (b : Basis ι R S) {x : S} (hx : x ≠ 0) (i : ι) :
2051-
(basisSpanSingleton b hx i : S) = x * b i := by
2052-
simp only [basisSpanSingleton, Basis.map_apply, LinearEquiv.trans_apply,
2053-
Submodule.restrictScalarsEquiv_apply, LinearEquiv.ofInjective_apply, LinearEquiv.coe_ofEq_apply,
2054-
LinearEquiv.restrictScalars_apply, Algebra.coe_lmul_eq_mul, LinearMap.mul_apply']
2055-
-- This used to be the end of the proof before leanprover/lean4#2644
2056-
erw [LinearEquiv.coe_ofEq_apply, LinearEquiv.ofInjective_apply, Algebra.coe_lmul_eq_mul,
2057-
LinearMap.mul_apply']
2058-
#align ideal.basis_span_singleton_apply Ideal.basisSpanSingleton_apply
2059-
2060-
@[simp]
2061-
theorem constr_basisSpanSingleton {N : Type*} [Semiring N] [Module N S] [SMulCommClass R N S]
2062-
(b : Basis ι R S) {x : S} (hx : x ≠ 0) :
2063-
(b.constr N).toFun (((↑) : _ → S) ∘ (basisSpanSingleton b hx)) = Algebra.lmul R S x :=
2064-
b.ext fun i => by
2065-
erw [Basis.constr_basis, Function.comp_apply, basisSpanSingleton_apply, LinearMap.mul_apply']
2066-
#align ideal.constr_basis_span_singleton Ideal.constr_basisSpanSingleton
2067-
2068-
end Basis
2069-
20701958
end Ideal
20711959

20721960
section span_range
@@ -2089,21 +1977,6 @@ theorem Associates.mk_ne_zero' {R : Type*} [CommSemiring R] {r : R} :
20891977
rw [Associates.mk_ne_zero, Ideal.zero_eq_bot, Ne, Ideal.span_singleton_eq_bot]
20901978
#align associates.mk_ne_zero' Associates.mk_ne_zero'
20911979

2092-
-- Porting note: added explicit coercion `(b i : S)`
2093-
/-- If `I : Ideal S` has a basis over `R`,
2094-
`x ∈ I` iff it is a linear combination of basis vectors. -/
2095-
theorem Basis.mem_ideal_iff {ι R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal S}
2096-
(b : Basis ι R I) {x : S} : x ∈ I ↔ ∃ c : ι →₀ R, x = Finsupp.sum c fun i x => x • (b i : S) :=
2097-
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff
2098-
#align basis.mem_ideal_iff Basis.mem_ideal_iff
2099-
2100-
/-- If `I : Ideal S` has a finite basis over `R`,
2101-
`x ∈ I` iff it is a linear combination of basis vectors. -/
2102-
theorem Basis.mem_ideal_iff' {ι R S : Type*} [Fintype ι] [CommRing R] [CommRing S] [Algebra R S]
2103-
{I : Ideal S} (b : Basis ι R I) {x : S} : x ∈ I ↔ ∃ c : ι → R, x = ∑ i, c i • (b i : S) :=
2104-
(b.map ((I.restrictScalarsEquiv R _ _).restrictScalars R).symm).mem_submodule_iff'
2105-
#align basis.mem_ideal_iff' Basis.mem_ideal_iff'
2106-
21071980
namespace RingHom
21081981

21091982
variable {R : Type u} {S : Type v} {T : Type w}

0 commit comments

Comments
 (0)