Skip to content

[Merged by Bors] - chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas #33341

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

Closed
themathqueen wants to merge 6 commits into from
Closed

[Merged by Bors] - chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas #33341

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
16b7cea
deprecate
themathqueen Dec 27, 2025
3d0dc57
fix
themathqueen Dec 27, 2025
b16dbda
tiny refactor
themathqueen Dec 27, 2025
f5a602e
one more deprecation
themathqueen Dec 28, 2025
3854aea
add 1 version
themathqueen Dec 31, 2025
3154e21
Apply suggestions from code review
themathqueen Jan 1, 2026
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: 1 addition & 1 deletion Mathlib/Analysis/InnerProductSpace/Positive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -490,7 +490,7 @@ theorem IsIdempotentElem.TFAE [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIde
tfae_have 2 ↔ 3 := hp.isSelfAdjoint_iff_isStarNormal.symm
tfae_have 3 ↔ 4 := hp.isPositive_iff_isSelfAdjoint.symm
tfae_have 3 ↔ 1 := p.isSelfAdjoint_iff_isSymmetric.eq ▸
(ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp)
(LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp.toLinearMap)
tfae_finish

end ContinuousLinearMap
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -332,8 +332,8 @@ open ContinuousLinearMap in
@[simp]
lemma ker_starProjection (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
U.starProjection.ker = Uᗮ := by
rw [(isIdempotentElem_starProjection U).ker_eq_range, ← starProjection_orthogonal',
range_starProjection]
rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
Copy link
Collaborator

@Ruben-VandeVelde Ruben-VandeVelde Jan 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does dot notation not work?

Copy link
Collaborator Author

@themathqueen themathqueen Jan 1, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not here because both ContinuousLinearMap and LinearMap namespaces are opened, so Lean gets confused which ker_eq_range to use. We would be able to use dot notation after removing the deprecation in 6 months.

← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]

theorem _root_.LinearIsometry.map_starProjection {E E' : Type*} [NormedAddCommGroup E]
[NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E')
Expand Down
9 changes: 3 additions & 6 deletions Mathlib/Analysis/InnerProductSpace/Symmetric.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -343,11 +343,8 @@ theorem IsSymmetric.isSymmetric_smul_iff {f : E →ₗ[𝕜] E} (hf : f.IsSymmet

end LinearMap

open ContinuousLinearMap in
/-- An idempotent operator `T` is symmetric iff `(range T)ᗮ = ker T`. -/
theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range
{T : E →L[𝕜] E} (h : IsIdempotentElem T) :
T.IsSymmetric ↔ T.rangeᗮ = T.ker :=
LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range h.toLinearMap
@[deprecated (since := "2025-12-28")] alias
ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range :=
LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range

end Normed
17 changes: 12 additions & 5 deletions Mathlib/LinearAlgebra/Projection.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -637,22 +637,29 @@ lemma IsIdempotentElem.ext_iff {p q : E →ₗ[R] E}
alias ⟨_, IsIdempotentElem.ext⟩ := IsIdempotentElem.ext_iff

theorem IsIdempotentElem.range_eq_ker {E : Type*} [AddCommGroup E] [Module S E]
{p : E →ₗ[S] E} (hp : IsIdempotentElem p) : LinearMap.range p = LinearMap.ker (1 - p) :=
{p : E →ₗ[S] E} (hp : IsIdempotentElem p) : LinearMap.range p = LinearMap.ker (id - p) :=
le_antisymm
(LinearMap.range_le_ker_iff.mpr hp.one_sub_mul_self)
fun x hx ↦ ⟨x, by simpa [sub_eq_zero, eq_comm (a := x)] using hx⟩

theorem IsIdempotentElem.range_eq_ker_one_sub {E : Type*} [AddCommGroup E] [Module S E]
{p : E →ₗ[S] E} (hp : IsIdempotentElem p) : LinearMap.range p = LinearMap.ker (1 - p) :=
range_eq_ker hp

open LinearMap in
theorem IsIdempotentElem.ker_eq_range {E : Type*} [AddCommGroup E] [Module S E]
{p : E →ₗ[S] E} (hp : IsIdempotentElem p) : LinearMap.ker p = LinearMap.range (1 - p) := by
simpa using hp.one_sub.range_eq_ker.symm
{p : E →ₗ[S] E} (hp : IsIdempotentElem p) : LinearMap.ker p = LinearMap.range (id - p) := by
simpa using hp.one_sub.range_eq_ker_one_sub.symm

theorem IsIdempotentElem.ker_eq_range_one_sub {E : Type*} [AddCommGroup E] [Module S E]
{p : E →ₗ[S] E} (hp : IsIdempotentElem p) : LinearMap.ker p = LinearMap.range (1 - p) :=
ker_eq_range hp

open LinearMap in
theorem IsIdempotentElem.comp_eq_left_iff {M : Type*} [AddCommGroup M] [Module S M] {q : M →ₗ[S] M}
(hq : IsIdempotentElem q) {E : Type*} [AddCommGroup E] [Module S E] (p : M →ₗ[S] E) :
p ∘ₗ q = p ↔ ker q ≤ ker p := by
simp [hq.ker_eq_range, range_le_ker_iff, comp_sub, Module.End.one_eq_id, sub_eq_zero,
eq_comm (a := p)]
simp [hq.ker_eq_range, range_le_ker_iff, comp_sub, sub_eq_zero, eq_comm]

end LinearMap

Expand Down
14 changes: 5 additions & 9 deletions Mathlib/Topology/Algebra/Module/LinearMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1261,18 +1261,14 @@ theorem IsIdempotentElem.commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit
simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using
LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap

theorem IsIdempotentElem.range_eq_ker {p : M →L[R] M} (hp : IsIdempotentElem p) :
p.range = (1 - p).ker :=
LinearMap.IsIdempotentElem.range_eq_ker hp.toLinearMap
@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.range_eq_ker :=
LinearMap.IsIdempotentElem.range_eq_ker
@[deprecated (since := "2025-12-27")] alias IsIdempotentElem.ker_eq_range :=
LinearMap.IsIdempotentElem.ker_eq_range

theorem IsIdempotentElem.ker_eq_range {p : M →L[R] M} (hp : IsIdempotentElem p) :
p.ker = (1 - p).range :=
LinearMap.IsIdempotentElem.ker_eq_range hp.toLinearMap

open ContinuousLinearMap in
theorem IsIdempotentElem.isClosed_range [T1Space M] {p : M →L[R] M}
(hp : IsIdempotentElem p) : IsClosed (p.range : Set M) :=
hp.range_eq_ker ▸ isClosed_ker (1 - p)
LinearMap.IsIdempotentElem.range_eq_ker hp.toLinearMap ▸ isClosed_ker (.id R M - p)

end ContinuousLinearMap

Expand Down