From 6a75b5307bf398cf60d220d6e1d59a285ea71bf2 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 20 May 2026 22:43:58 +1000 Subject: [PATCH 1/8] feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ --- Mathlib/LinearAlgebra/Projection.lean | 5 +++++ Mathlib/Topology/Algebra/Module/Complement.lean | 6 ++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index d1ceefce5eb79a..cf344131afcc47 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -286,6 +286,11 @@ def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q := (by ext; simp) (by ext; simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem]) +@[simp] +theorem quotientEquivOfIsCompl_comp_mkQ (h : IsCompl p q) : + (quotientEquivOfIsCompl p q h : E ⧸ p →ₗ[R] q) ∘ₗ p.mkQ = q.projectionOnto p h.symm := by + ext; rfl + @[simp] theorem quotientEquivOfIsCompl_apply_mk (h : IsCompl p q) (x : E) : quotientEquivOfIsCompl p q h (Quotient.mk x) = q.projectionOnto p h.symm x := diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 04a11fce870f0f..58f1365dca38a8 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -449,10 +449,8 @@ theorem prodEquivOfIsTopCompl_symm_apply (h : IsTopCompl p q) (x : M) : `Submodule.quotientEquivOfIsCompl` is continuous. -/ theorem IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl (h : IsCompl p q) : IsTopCompl p q ↔ Continuous (p.quotientEquivOfIsCompl q h) := by - have hproj : ⇑(p.quotientEquivOfIsCompl q h) ∘ ⇑p.mkQ = ⇑(q.projectionOnto p h.symm) := by - funext; simp - rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto, - isTopCompl_comm] + rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL] + exact isTopCompl_comm.trans h.symm.isTopCompl_iff_projectionOnto variable (p q) in /-- If two submodules are topological complements, then the linear equivalence From 8b61da2d40266af6f5a27a3aae2d75b6f4c4bb59 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Wed, 20 May 2026 22:52:05 +1000 Subject: [PATCH 2/8] Simplified further --- Mathlib/Topology/Algebra/Module/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 58f1365dca38a8..3863a20a9f9722 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -449,7 +449,7 @@ theorem prodEquivOfIsTopCompl_symm_apply (h : IsTopCompl p q) (x : M) : `Submodule.quotientEquivOfIsCompl` is continuous. -/ theorem IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl (h : IsCompl p q) : IsTopCompl p q ↔ Continuous (p.quotientEquivOfIsCompl q h) := by - rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL] + rw [p.isQuotientMap_mkQL.continuous_iff] exact isTopCompl_comm.trans h.symm.isTopCompl_iff_projectionOnto variable (p q) in From 523c10d7a54676acc5b9838fa43822845759f60e Mon Sep 17 00:00:00 2001 From: sharky564 Date: Thu, 21 May 2026 00:35:50 +1000 Subject: [PATCH 3/8] Fixed simp --- Mathlib/LinearAlgebra/Projection.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index cf344131afcc47..bbdcc706751200 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -286,7 +286,6 @@ def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q := (by ext; simp) (by ext; simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem]) -@[simp] theorem quotientEquivOfIsCompl_comp_mkQ (h : IsCompl p q) : (quotientEquivOfIsCompl p q h : E ⧸ p →ₗ[R] q) ∘ₗ p.mkQ = q.projectionOnto p h.symm := by ext; rfl From 1c00291b9d6d502e8f28ed18a5fd8135248ae805 Mon Sep 17 00:00:00 2001 From: sharky564 Date: Sun, 24 May 2026 12:35:22 +1000 Subject: [PATCH 4/8] PR fixes --- Mathlib/LinearAlgebra/Projection.lean | 4 ++-- Mathlib/Topology/Algebra/Module/Complement.lean | 9 +++++++-- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/Projection.lean b/Mathlib/LinearAlgebra/Projection.lean index bbdcc706751200..0acf6bd2e190d3 100644 --- a/Mathlib/LinearAlgebra/Projection.lean +++ b/Mathlib/LinearAlgebra/Projection.lean @@ -287,8 +287,8 @@ def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q := (by ext; simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem]) theorem quotientEquivOfIsCompl_comp_mkQ (h : IsCompl p q) : - (quotientEquivOfIsCompl p q h : E ⧸ p →ₗ[R] q) ∘ₗ p.mkQ = q.projectionOnto p h.symm := by - ext; rfl + (quotientEquivOfIsCompl p q h : E ⧸ p →ₗ[R] q) ∘ₗ p.mkQ = q.projectionOnto p h.symm := + rfl @[simp] theorem quotientEquivOfIsCompl_apply_mk (h : IsCompl p q) (x : E) : diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 3863a20a9f9722..306963fd9fef37 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -449,8 +449,8 @@ theorem prodEquivOfIsTopCompl_symm_apply (h : IsTopCompl p q) (x : M) : `Submodule.quotientEquivOfIsCompl` is continuous. -/ theorem IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl (h : IsCompl p q) : IsTopCompl p q ↔ Continuous (p.quotientEquivOfIsCompl q h) := by - rw [p.isQuotientMap_mkQL.continuous_iff] - exact isTopCompl_comm.trans h.symm.isTopCompl_iff_projectionOnto + rw [p.isQuotientMap_mkQL.continuous_iff, isTopCompl_comm] + exact h.symm.isTopCompl_iff_projectionOnto variable (p q) in /-- If two submodules are topological complements, then the linear equivalence @@ -466,6 +466,11 @@ theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) : (quotientEquivOfIsTopCompl p q h : (M ⧸ p) ≃ₗ[R] q) = p.quotientEquivOfIsCompl q h.isCompl := rfl +theorem quotientEquivOfIsTopCompl_comp_mkQ (h : IsTopCompl p q) : + (quotientEquivOfIsTopCompl p q h : (M ⧸ p) →ₗ[R] q) ∘ₗ p.mkQ = + q.projectionOnto p h.isCompl.symm := + rfl + @[simp] theorem quotientEquivOfIsTopCompl_apply (h : IsTopCompl p q) (x : M ⧸ p) : quotientEquivOfIsTopCompl p q h x = p.quotientEquivOfIsCompl q h.isCompl x := From 59884824dc641be062c5def3ecc8af71dc60b2a8 Mon Sep 17 00:00:00 2001 From: Sharvil Kesarwani Date: Sun, 24 May 2026 15:29:33 +1000 Subject: [PATCH 5/8] Update Mathlib/Topology/Algebra/Module/Complement.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Topology/Algebra/Module/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 306963fd9fef37..71b88110088d7a 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -468,7 +468,7 @@ theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) : theorem quotientEquivOfIsTopCompl_comp_mkQ (h : IsTopCompl p q) : (quotientEquivOfIsTopCompl p q h : (M ⧸ p) →ₗ[R] q) ∘ₗ p.mkQ = - q.projectionOnto p h.isCompl.symm := + q.projectionOnto p h.isCompl.symm := rfl @[simp] From c16dd598c863f95fb995ecc4b87e76b849bd122e Mon Sep 17 00:00:00 2001 From: Sharvil Kesarwani Date: Thu, 4 Jun 2026 01:12:38 +1000 Subject: [PATCH 6/8] Update Mathlib/Topology/Algebra/Module/Complement.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Topology/Algebra/Module/Complement.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 71b88110088d7a..bc0fb4e659a7b8 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -467,8 +467,8 @@ theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) : rfl theorem quotientEquivOfIsTopCompl_comp_mkQ (h : IsTopCompl p q) : - (quotientEquivOfIsTopCompl p q h : (M ⧸ p) →ₗ[R] q) ∘ₗ p.mkQ = - q.projectionOnto p h.isCompl.symm := + (quotientEquivOfIsTopCompl p q h : (M ⧸ p) →L[R] q) ∘L p.mkQL = + q.projectionOntoL p h.symm := rfl @[simp] From c50106fa4786ceb48f1d4a9a6612e288c856c0bf Mon Sep 17 00:00:00 2001 From: sharky564 Date: Thu, 4 Jun 2026 01:43:16 +1000 Subject: [PATCH 7/8] PR fixes --- Mathlib/Topology/Algebra/Module/Complement.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index bc0fb4e659a7b8..66a662445a252d 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -467,8 +467,7 @@ theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) : rfl theorem quotientEquivOfIsTopCompl_comp_mkQ (h : IsTopCompl p q) : - (quotientEquivOfIsTopCompl p q h : (M ⧸ p) →L[R] q) ∘L p.mkQL = - q.projectionOntoL p h.symm := + (quotientEquivOfIsTopCompl p q h) ∘L p.mkQL = q.projectionOntoL p h.symm := rfl @[simp] From 6e69f7f4a9ee11214f959ef0348e43ad62af5030 Mon Sep 17 00:00:00 2001 From: Sharvil Kesarwani Date: Thu, 4 Jun 2026 02:31:48 +1000 Subject: [PATCH 8/8] Update Mathlib/Topology/Algebra/Module/Complement.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Topology/Algebra/Module/Complement.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Algebra/Module/Complement.lean b/Mathlib/Topology/Algebra/Module/Complement.lean index 92c328a3dc9703..dcf163220e1a39 100644 --- a/Mathlib/Topology/Algebra/Module/Complement.lean +++ b/Mathlib/Topology/Algebra/Module/Complement.lean @@ -467,7 +467,7 @@ theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) : (quotientEquivOfIsTopCompl p q h : (M ⧸ p) ≃ₗ[R] q) = p.quotientEquivOfIsCompl q h.isCompl := rfl -theorem quotientEquivOfIsTopCompl_comp_mkQ (h : IsTopCompl p q) : +theorem quotientEquivOfIsTopCompl_comp_mkQL (h : IsTopCompl p q) : (quotientEquivOfIsTopCompl p q h) ∘L p.mkQL = q.projectionOntoL p h.symm := rfl