Skip to content

Commit d9996c5

Browse files
themathqueenthemathqueen
committed
feat(Analysis/Normed/Operator): continuous algebra equivalences between continuous endomorphisms are inner (leanprover-community#33017)
This is the continuous version of [AlgEquiv.eq_linearEquivConjAlgEquiv](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.html#AlgEquiv.eq_linearEquivConjAlgEquiv). The proof follows the same idea as the non-continuous version.
1 parent f160a5e commit d9996c5

5 files changed

Lines changed: 123 additions & 12 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1992,6 +1992,7 @@ public import Mathlib.Analysis.Normed.Operator.Compact
19921992
public import Mathlib.Analysis.Normed.Operator.CompleteCodomain
19931993
public import Mathlib.Analysis.Normed.Operator.Completeness
19941994
public import Mathlib.Analysis.Normed.Operator.Conformal
1995+
public import Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
19951996
public import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
19961997
public import Mathlib.Analysis.Normed.Operator.Extend
19971998
public import Mathlib.Analysis.Normed.Operator.LinearIsometry

‎Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
/-
2+
Copyright (c) 2025 Monica Omar. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Monica Omar
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.LocallyConvex.SeparatingDual
9+
public import Mathlib.Analysis.Normed.Operator.Banach
10+
public import Mathlib.Topology.Algebra.Algebra.Equiv
11+
12+
/-!
13+
# Continuous algebra equivalences between continuous endomorphisms are inner
14+
15+
This file shows that continuous algebra equivalences between continuous endomorphisms are inner.
16+
See `Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean` for the non-continuous version.
17+
The proof follows the same idea as the non-continuous version.
18+
19+
# TODO:
20+
- when `V = W`, we can state that the group homomorphism
21+
`(V →L[𝕜] V)ˣ →* ((V →L[𝕜] V) ≃A[𝕜] (V →L[𝕜] V))` is surjective,
22+
see `Module.End.mulSemiringActionToAlgEquiv_conjAct_surjective` for the non-continuous
23+
version of this.
24+
-/
25+
26+
open ContinuousLinearMap ContinuousLinearEquiv
27+
28+
/-- This is the continuous version of `AlgEquiv.eq_linearEquivConjAlgEquiv`. -/
29+
public theorem ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv {𝕜 V W : Type*}
30+
[NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [SeminormedAddCommGroup W]
31+
[NormedSpace 𝕜 V] [NormedSpace 𝕜 W] [SeparatingDual 𝕜 V] [SeparatingDual 𝕜 W]
32+
(f : (V →L[𝕜] V) ≃A[𝕜] (W →L[𝕜] W)) :
33+
∃ U : V ≃L[𝕜] W, f = U.conjContinuousAlgEquiv := by
34+
/- The proof goes as follows:
35+
We want to show the existence of a continuous linear equivalence `U : V ≃L[𝕜] W` such that
36+
`f A (U x) = U (A x)` for all `A : V →L[𝕜] V` and `x : V`.
37+
Assume nontriviality of `V`, and let `(u : V) ≠ 0`. Let `v` be a strong dual on `V` such that
38+
`v u ≠ 0` (exists since it has a separating dual).
39+
Let `z : W` such that `f (smulRight v u) z ≠ 0`.
40+
Then we construct a bijective continuous linear map `T : V →L[𝕜] W`
41+
given by `x ↦ f (smulRight v x) z` and so satisfies `T (A x) = f A (T x)` for all
42+
`A : V →L[𝕜] V` and `x : V`. So it remains to show that this map has a continuous inverse.
43+
Let `d` be a strong dual on `W` such that `d ((f (smulRight v u)) z) = 1` (exists since it has
44+
a separating dual).
45+
We then construct a right-inverse continuous linear map `T' : W →L[𝕜] V` given by
46+
`x ↦ f.symm (smulRight d x) u`.
47+
And so it follows that `T` is also a continuous linear equivalence. -/
48+
by_cases! hV : Subsingleton V
49+
· by_cases! hV : Subsingleton W
50+
· exact ⟨{ toLinearEquiv := 0 }, ext <| Subsingleton.allEq _ _⟩
51+
simpa using congr(f $(Subsingleton.allEq 0 1))
52+
simp_rw [ContinuousAlgEquiv.ext_iff, funext_iff, conjContinuousAlgEquiv_apply, ← comp_assoc,
53+
eq_comp_toContinuousLinearMap_symm]
54+
obtain ⟨u, hu⟩ := exists_ne (0 : V)
55+
obtain ⟨v, huv⟩ := SeparatingDual.exists_ne_zero (R := 𝕜) hu
56+
obtain ⟨z, hz⟩ : ∃ z : W, ¬ f (smulRight v u) z = (0 : W →L[𝕜] W) z := by
57+
rw [← not_forall, ← ContinuousLinearMap.ext_iff, map_eq_zero_iff, ContinuousLinearMap.ext_iff]
58+
exact not_forall.mpr ⟨u, huv.isUnit.smul_eq_zero.not.mpr hu⟩
59+
set T := apply' _ (.id 𝕜) z ∘L f.toContinuousAlgHom.toContinuousLinearMap ∘L smulRightL 𝕜 _ _ v
60+
have hT x : T x = f (smulRight v x) z := rfl
61+
have this A x : T (A x) = f A (T x) := by
62+
simp only [hT, ← mul_apply, ← map_mul]
63+
congr; ext; simp
64+
have ⟨d, hd⟩ := SeparatingDual.exists_eq_one (R := 𝕜) hz
65+
have surj : Function.Surjective T := fun w ↦ ⟨f.symm (smulRight d w) u, by simp [T, this, hd]⟩
66+
have inj : Function.Injective T := fun x y hxy ↦ by
67+
have h_smul : smulRight v x = smulRight v y := by
68+
apply f.injective <| ContinuousLinearMap.ext fun z ↦ ?_
69+
obtain ⟨w, rfl⟩ := surj z
70+
simp [← this, hxy]
71+
simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)
72+
set Tₗ : V ≃ₗ[𝕜] W := .ofBijective T.toLinearMap ⟨inj, surj⟩
73+
set T' := apply' _ (.id 𝕜) u ∘L f.symm.toContinuousAlgHom.toContinuousLinearMap ∘L
74+
smulRightL 𝕜 _ _ d
75+
set TL : V ≃L[𝕜] W := { Tₗ with
76+
continuous_toFun := T.continuous
77+
continuous_invFun := by
78+
change Continuous Tₗ.symm.toLinearMap
79+
suffices T'.toLinearMap = Tₗ.symm from this ▸ T'.continuous
80+
simp [LinearMap.ext_iff, ← Tₗ.injective.eq_iff, T', this, hT, hd, Tₗ] }
81+
exact ⟨TL, fun A ↦ (ContinuousLinearMap.ext <| this A).symm⟩

‎Mathlib/Topology/Algebra/Algebra.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -233,6 +233,11 @@ theorem ext_on [T2Space B] {s : Set A} (hs : Dense (Algebra.adjoin R s : Set A))
233233
{f g : A →A[R] B} (h : Set.EqOn f g s) : f = g :=
234234
ext fun x => eqOn_closure_adjoin h (hs x)
235235

236+
/-- Interpret a `ContinuousAlgHom` as a `ContinuousLinearMap`. -/
237+
def toContinuousLinearMap (e : A →A[R] B) : A →L[R] B where toLinearMap := e.toAlgHom.toLinearMap
238+
239+
@[simp] theorem coe_toContinuousLinearMap (e : A →A[R] B) : ⇑e.toContinuousLinearMap = e := rfl
240+
236241
variable [IsTopologicalSemiring A]
237242

238243
/-- The topological closure of a subalgebra -/

‎Mathlib/Topology/Algebra/Module/Equiv.lean‎

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -660,25 +660,22 @@ theorem symm_equivOfInverse' (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ h₁ h₂)
660660
(equivOfInverse' f₁ f₂ h₁ h₂).symm = equivOfInverse' f₂ f₁ h₂ h₁ :=
661661
rfl
662662

663+
theorem eq_comp_toContinuousLinearMap_symm (e₁₂ : M₁ ≃SL[σ₁₂] M₂) [RingHomCompTriple σ₂₁ σ₁₃ σ₂₃]
664+
(f : M₂ →SL[σ₂₃] M₃) (g : M₁ →SL[σ₁₃] M₃) :
665+
f = g.comp e₁₂.symm.toContinuousLinearMap ↔ f.comp e₁₂.toContinuousLinearMap = g := by
666+
aesop
667+
663668
variable (M₁)
664669

665670
/-- The continuous linear equivalences from `M` to itself form a group under composition. -/
666671
instance automorphismGroup : Group (M₁ ≃L[R₁] M₁) where
667672
mul f g := g.trans f
668673
one := ContinuousLinearEquiv.refl R₁ M₁
669674
inv f := f.symm
670-
mul_assoc f g h := by
671-
ext
672-
rfl
673-
mul_one f := by
674-
ext
675-
rfl
676-
one_mul f := by
677-
ext
678-
rfl
679-
inv_mul_cancel f := by
680-
ext x
681-
exact f.left_inv x
675+
mul_assoc f g h := rfl
676+
mul_one f := rfl
677+
one_mul f := rfl
678+
inv_mul_cancel f := ext <| funext fun _ ↦ f.left_inv _
682679

683680
variable {M₁} {R₄ : Type*} [Semiring R₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃}
684681
[RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄}

‎Mathlib/Topology/Algebra/Module/StrongTopology.lean‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Anatole Dedecker, Yury Kudryashov
55
-/
66
module
77

8+
public import Mathlib.Topology.Algebra.Algebra.Equiv
89
public import Mathlib.Topology.Algebra.Module.Equiv
910
public import Mathlib.Topology.Algebra.Module.UniformConvergence
1011
public import Mathlib.Topology.Algebra.SeparationQuotient.Section
@@ -801,6 +802,32 @@ def arrowCongr (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H
801802
@[simp] lemma arrowCongr_symm (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) :
802803
(e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm := rfl
803804

805+
/-- A continuous linear equivalence of two spaces induces a continuous equivalence of algebras of
806+
their endomorphisms. -/
807+
def conjContinuousAlgEquiv (e : G ≃L[𝕜] H) : (G →L[𝕜] G) ≃A[𝕜] (H →L[𝕜] H) :=
808+
{ e.arrowCongr e with
809+
map_mul' _ _ := by ext; simp
810+
commutes' _ := by ext; simp }
811+
812+
@[simp] theorem conjContinuousAlgEquiv_apply_apply (e : G ≃L[𝕜] H) (f : G →L[𝕜] G) (x : H) :
813+
e.conjContinuousAlgEquiv f x = e (f (e.symm x)) := rfl
814+
815+
theorem symm_conjContinuousAlgEquiv_apply_apply (e : G ≃L[𝕜] H) (f : H →L[𝕜] H) (x : G) :
816+
e.conjContinuousAlgEquiv.symm f x = e.symm (f (e x)) := rfl
817+
818+
theorem conjContinuousAlgEquiv_apply (e : G ≃L[𝕜] H) (f : G →L[𝕜] G) :
819+
e.conjContinuousAlgEquiv f = e ∘L f ∘L e.symm := rfl
820+
821+
@[simp] theorem symm_conjContinuousAlgEquiv (e : G ≃L[𝕜] H) :
822+
e.conjContinuousAlgEquiv.symm = e.symm.conjContinuousAlgEquiv := rfl
823+
824+
@[simp] theorem conjContinuousAlgEquiv_refl : conjContinuousAlgEquiv (.refl 𝕜 G) = .refl 𝕜 _ := rfl
825+
826+
theorem conjContinuousAlgEquiv_trans [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
827+
(e : E ≃L[𝕜] G) (f : G ≃L[𝕜] H) :
828+
(e.trans f).conjContinuousAlgEquiv = e.conjContinuousAlgEquiv.trans f.conjContinuousAlgEquiv :=
829+
rfl
830+
804831
end Linear
805832

806833
end ContinuousLinearEquiv

0 commit comments

Comments
 (0)