fixes and moving stuff

themathqueen · Jul 16, 2024 · d68f02d · d68f02d
1 parent e2ece37
commit d68f02d
Show file tree

Hide file tree

Showing 8 changed files with 312 additions and 175 deletions.
diff --git a/Monlib/LinearAlgebra/Ips/Basic.lean b/Monlib/LinearAlgebra/Ips/Basic.lean
@@ -149,3 +149,54 @@ lemma inner_self_nonpos' {E : Type _} [NormedAddCommGroup E] [InnerProductSpace
   ⟪x, x⟫_𝕜 ≤ 0 ↔ x = 0 :=
 by
 simp_rw [@RCLike.nonpos_def 𝕜, inner_self_nonpos, inner_self_im, and_true]
+
+
+lemma _root_.isometry_iff_norm {E F : Type _} [SeminormedAddGroup E] [SeminormedAddGroup F]
+  {e : Type*} [FunLike e E F]
+  [AddMonoidHomClass e E F]
+  (f : e) :
+  Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖ :=
+by
+  rw [isometry_iff_dist_eq]
+  simp_rw [dist_eq_norm, ← map_sub]
+  constructor
+  . intro h x
+    specialize h x 0
+    simp_rw [sub_zero] at h
+    exact h
+  . intro h x y
+    exact h _
+lemma _root_.isometry_iff_norm' {E F : Type _} [_root_.NormedAddCommGroup E] [_root_.NormedAddCommGroup F]
+  {e : Type*} [FunLike e E F]
+  [AddMonoidHomClass e E F]
+  (f : e) :
+  Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖ :=
+isometry_iff_norm _
+lemma _root_.isometry_iff_inner {R E F : Type _} [RCLike R]
+  [_root_.NormedAddCommGroup E] [_root_.NormedAddCommGroup F]
+  [_root_.InnerProductSpace R E] [_root_.InnerProductSpace R F]
+  {M : Type*} [FunLike M E F] [LinearMapClass M R E F]
+  (f : M) :
+  Isometry f ↔ ∀ x y, ⟪f x, f y⟫_R = ⟪x, y⟫_R :=
+by
+  rw [isometry_iff_dist_eq]
+  simp_rw [dist_eq_norm, ← map_sub]
+  constructor
+  . simp_rw [inner_eq_sum_norm_sq_div_four, ← _root_.map_smul, ← map_add, ← map_sub]
+    intro h x y
+    have := λ x => h x 0
+    simp_rw [sub_zero] at this
+    simp_rw [this]
+  . intro h x y
+    simp_rw [@norm_eq_sqrt_inner R, h]
+lemma _root_.isometry_iff_inner_norm'
+  {R E F : Type _} [RCLike R] [_root_.NormedAddCommGroup E] [_root_.NormedAddCommGroup F]
+  [_root_.InnerProductSpace R E] [_root_.InnerProductSpace R F]
+  {M : Type*} [FunLike M E F] [LinearMapClass M R E F] (f : M) :
+  (∀ x, ‖f x‖ = ‖x‖) ↔ ∀ x y, ⟪f x, f y⟫_R = ⟪x, y⟫_R :=
+by rw [← isometry_iff_inner, isometry_iff_norm]
+
+lemma _root_.seminormedAddGroup_norm_eq_norm_NormedAddCommGroup
+  {E : Type _} [_root_.NormedAddCommGroup E] (x : E) :
+  @norm E SeminormedAddGroup.toNorm x = @norm E _root_.NormedAddCommGroup.toNorm x :=
+rfl
diff --git a/Monlib/LinearAlgebra/Ips/MatIps.lean b/Monlib/LinearAlgebra/Ips/MatIps.lean
@@ -900,55 +900,6 @@ private theorem mul_inv_eq_iff_eq_mul_aux [hψ : ∀ i, (ψ i).IsFaithfulPosMap]
 --   simp only [mul_assoc, unitary.coe_star_mul_self, mul_one, eq_comm, Commute, SemiconjBy,
 --     Pi.mul_def, Pi.star_def]
 
-lemma _root_.isometry_iff_norm {E F : Type _} [SeminormedAddGroup E] [SeminormedAddGroup F]
-  {e : Type*} [FunLike e E F]
-  [AddMonoidHomClass e E F]
-  (f : e) :
-  Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖ :=
-by
-  rw [isometry_iff_dist_eq]
-  simp_rw [dist_eq_norm, ← map_sub]
-  constructor
-  . intro h x
-    specialize h x 0
-    simp_rw [sub_zero] at h
-    exact h
-  . intro h x y
-    exact h _
-lemma _root_.isometry_iff_norm' {E F : Type _} [_root_.NormedAddCommGroup E] [_root_.NormedAddCommGroup F]
-  {e : Type*} [FunLike e E F]
-  [AddMonoidHomClass e E F]
-  (f : e) :
-  Isometry f ↔ ∀ x, ‖f x‖ = ‖x‖ :=
-isometry_iff_norm _
-lemma _root_.isometry_iff_inner {R E F : Type _} [RCLike R]
-  [_root_.NormedAddCommGroup E] [_root_.NormedAddCommGroup F]
-  [_root_.InnerProductSpace R E] [_root_.InnerProductSpace R F]
-  (f : E →ₗ[R] F) :
-  Isometry f ↔ ∀ x y, ⟪f x, f y⟫_R = ⟪x, y⟫_R :=
-by
-  rw [isometry_iff_dist_eq]
-  simp_rw [dist_eq_norm, ← map_sub]
-  constructor
-  . simp_rw [inner_eq_sum_norm_sq_div_four, ← _root_.map_smul, ← map_add, ← map_sub]
-    intro h x y
-    have := λ x => h x 0
-    simp_rw [sub_zero] at this
-    simp_rw [this]
-  . intro h x y
-    simp_rw [@norm_eq_sqrt_inner R, h]
-lemma _root_.isometry_iff_inner_norm'
-  {R E F : Type _} [RCLike R] [_root_.NormedAddCommGroup E] [_root_.NormedAddCommGroup F]
-  [_root_.InnerProductSpace R E] [_root_.InnerProductSpace R F]
-  (f : E →ₗ[R] F) :
-  (∀ x, ‖f x‖ = ‖x‖) ↔ ∀ x y, ⟪f x, f y⟫_R = ⟪x, y⟫_R :=
-by rw [← isometry_iff_inner, isometry_iff_norm]
-
-lemma _root_.seminormedAddGroup_norm_eq_norm_NormedAddCommGroup
-  {E : Type _} [_root_.NormedAddCommGroup E] (x : E) :
-  @norm E SeminormedAddGroup.toNorm x = @norm E _root_.NormedAddCommGroup.toNorm x :=
-rfl
-
 -- theorem starAlgEquiv_is_isometry_tfae [hψ : ∀ i, (ψ i).IsFaithfulPosMap]
 --     [∀ i, Nontrivial (s i)] (f : ∀ i, Matrix (s i) (s i) ℂ ≃⋆ₐ[ℂ] Matrix (s i) (s i) ℂ) :
 --     List.TFAE

diff --git a/Monlib/LinearAlgebra/IsReal.lean b/Monlib/LinearAlgebra/IsReal.lean
@@ -27,6 +27,14 @@ def LinearMap.IsReal {M₁ M₂ : Type*} {F : Type*} [FunLike F M₁ M₂]
   [Star M₁] [Star M₂] (φ : F) : Prop :=
 ∀ x, φ (star x) = star (φ x)
 
+@[simp]
+theorem starHomClass.linearMap_isReal {M₁ M₂ : Type*} {F : Type*} [FunLike F M₁ M₂]
+  [Star M₁] [Star M₂] [StarHomClass F M₁ M₂] (φ : F) :
+    LinearMap.IsReal φ :=
+by
+  intro
+  simp only [map_star]
+
 section Sec
 
 variable {E F K : Type _} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F]
@@ -84,6 +92,11 @@ theorem LinearMap.isReal_iff
   simp_rw [LinearMap.IsReal, LinearMap.ext_iff, LinearMap.real_apply,
     @eq_star_iff_eq_star _ _ (φ (star _)), eq_comm]
 
+theorem LinearMap.real_of_isReal {φ : E →ₗ[K] F}
+   (hφ : LinearMap.IsReal φ) :
+  φ.real = φ :=
+(LinearMap.isReal_iff φ).mp hφ
+
 open scoped BigOperators
 
 @[simp]

diff --git a/Monlib/LinearAlgebra/QuantumSet/Basic.lean b/Monlib/LinearAlgebra/QuantumSet/Basic.lean
@@ -986,16 +986,16 @@ lemma _root_.LinearMap.apply_eq_id {R M : Type*} [Semiring R] [AddCommMonoid M]
 by simp_rw [LinearMap.ext_iff, LinearMap.one_apply]
 
 theorem _root_.QuantumSet.starAlgEquiv_is_isometry_tfae
-    (gns₁ : hA.k = 0) (gns₂ : hB.k = 0)
+    -- (gns₁ : hA.k = 0) (gns₂ : hB.k = 0)
     (f : A ≃⋆ₐ[ℂ] B) :
     List.TFAE
-      [LinearMap.adjoint f.toLinearMap =
-          f.symm.toLinearMap,
-        Coalgebra.counit ∘ₗ f.toLinearMap = Coalgebra.counit,
+      [LinearMap.adjoint f.toLinearMap = f.symm.toLinearMap,
+
         ∀ x y, ⟪f x, f y⟫_ℂ = ⟪x, y⟫_ℂ,
-        ∀ x, ‖f x‖ = ‖x‖] :=
+        ∀ x, ‖f x‖ = ‖x‖,
+        Isometry f] :=
 by
-  tfae_have 4 ↔ 1
+  tfae_have 3 ↔ 1
   · simp_rw [@norm_eq_sqrt_inner ℂ, Real.sqrt_inj inner_self_nonneg inner_self_nonneg,
       ← @RCLike.ofReal_inj ℂ, @inner_self_re ℂ, ← @sub_eq_zero _ _ _ ⟪_, _⟫_ℂ]
     have :
@@ -1008,21 +1008,99 @@ by
         LinearMap.adjoint_inner_left, StarAlgEquiv.toLinearMap_apply]
     simp_rw [this, inner_map_self_eq_zero, sub_eq_zero, StarAlgEquiv.comp_eq_iff,
       LinearMap.one_comp]
-  rw [tfae_4_iff_1]
-  tfae_have 3 ↔ 2
-  ·
-    simp_rw [QuantumSet.inner_eq_counit, ← map_star f,
-      LinearMap.ext_iff, LinearMap.comp_apply, StarAlgEquiv.toLinearMap_apply,
-        gns₁, gns₂, starAlgebra.modAut_zero, AlgEquiv.one_apply, ← map_mul]
-    refine' ⟨fun h x => _, fun h x y => h _⟩
-    rw [← one_mul x, ← star_one]
-    exact h _ _
-  rw [← tfae_3_iff_2]
+  rw [tfae_3_iff_1]
+  -- tfae_have 3 ↔ 2
+  -- ·
+  --
   simp_rw [← StarAlgEquiv.toLinearMap_apply, ← LinearMap.adjoint_inner_left,
     ← ext_inner_left_iff, ← LinearMap.comp_apply, _root_.LinearMap.apply_eq_id,
     StarAlgEquiv.comp_eq_iff, LinearMap.one_comp]
+  rw [AddMonoidHomClass.isometry_iff_norm]
   tfae_finish
 
+theorem _root_.QuantumSet.starAlgEquiv_isometry_iff_adjoint_eq_symm
+    {f : A ≃⋆ₐ[ℂ] B} :
+    Isometry f ↔ LinearMap.adjoint f.toLinearMap = f.symm.toLinearMap :=
+List.TFAE.out (starAlgEquiv_is_isometry_tfae f) 3 0
+
+theorem QuantumSet.starAlgEquiv_isometry_iff_coalgHom
+  (gns₁ : hA.k = 0) (gns₂ : hB.k = 0)
+  {f : A ≃⋆ₐ[ℂ] B} :
+  Isometry f ↔
+  Coalgebra.counit ∘ₗ f.toLinearMap = Coalgebra.counit :=
+by
+  simp_rw [isometry_iff_inner,
+    QuantumSet.inner_eq_counit, ← map_star f,
+    LinearMap.ext_iff, LinearMap.comp_apply, StarAlgEquiv.toLinearMap_apply,
+    gns₁, gns₂, starAlgebra.modAut_zero, AlgEquiv.one_apply, ← map_mul]
+  refine' ⟨fun h x => _, fun h x y => h _⟩
+  rw [← one_mul x, ← star_one]
+  exact h _ _
+
+theorem _root_.StarAlgEquiv.isReal {R A B : Type*} [Semiring R]
+  [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A]
+  [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) :
+    LinearMap.IsReal f.toLinearMap :=
+by
+  intro
+  simp only [StarAlgEquiv.toLinearMap_apply, map_star]
+
+theorem QuantumSet.modAut_real (r : ℝ) :
+    (ha.modAut r).toLinearMap.real = (ha.modAut (-r)).toLinearMap :=
+by
+  rw [LinearMap.ext_iff]
+  intro
+  simp_rw [LinearMap.real_apply, AlgEquiv.toLinearMap_apply, ha.modAut_star, star_star]
+
+theorem _root_.AlgEquiv.linearMap_comp_eq_iff {R E₁ E₂ E₃ : Type _} [CommSemiring R] [Semiring E₁] [Semiring E₂]
+    [AddCommMonoid E₃] [Algebra R E₁] [Algebra R E₂] [Module R E₃]
+    (f : E₁ ≃ₐ[R] E₂) (x : E₂ →ₗ[R] E₃) (y : E₁ →ₗ[R] E₃) :
+    x ∘ₗ f.toLinearMap = y ↔ x = y ∘ₗ f.symm.toLinearMap :=
+by aesop
+theorem _root_.AlgEquiv.comp_linearMap_eq_iff
+  {R E₁ E₂ E₃ : Type _} [CommSemiring R] [Semiring E₁] [Semiring E₂]
+  [AddCommMonoid E₃] [Algebra R E₁] [Algebra R E₂] [Module R E₃]
+  (f : E₁ ≃ₐ[R] E₂) (x : E₃ →ₗ[R] E₁) (y : E₃ →ₗ[R] E₂) :
+  f.toLinearMap ∘ₗ x = y ↔ x = f.symm.toLinearMap ∘ₗ y :=
+by aesop
+
+lemma QuantumSet.modAut_adjoint (r : ℝ) :
+  LinearMap.adjoint (ha.modAut r).toLinearMap = (ha.modAut r).toLinearMap :=
+by
+  rw [← LinearMap.isSelfAdjoint_iff']
+  exact modAut_isSelfAdjoint r
+
+theorem _root_.QuantumSet.starAlgEquiv_commutes_with_modAut_of_isometry
+  {f : A ≃⋆ₐ[ℂ] B} (hf : Isometry f) :
+  (modAut ((2 * k A) + 1)).trans f.toAlgEquiv = f.toAlgEquiv.trans (modAut ((2 * k B) + 1)) :=
+by
+  rw [starAlgEquiv_isometry_iff_adjoint_eq_symm] at hf
+  have := LinearMap.adjoint_real_eq f.toLinearMap
+  rw [← neg_sub] at this
+  simp only [sub_neg_eq_add,
+    LinearMap.real_of_isReal (_root_.StarAlgEquiv.isReal _), hf] at this
+  simp only [← LinearMap.comp_assoc, ← modAut_symm,
+    ← AlgEquiv.linearMap_comp_eq_iff] at this
+  apply_fun LinearMap.adjoint at this
+  simp only [LinearMap.adjoint_comp, ← hf, LinearMap.adjoint_adjoint,
+    QuantumSet.modAut_adjoint] at this
+  simp only [LinearMap.ext_iff, LinearMap.comp_apply, StarAlgEquiv.toLinearMap_apply,
+    AlgEquiv.toLinearMap_apply] at this
+  simp only [AlgEquiv.ext_iff, AlgEquiv.trans_apply, StarAlgEquiv.coe_toAlgEquiv]
+  nth_rw 2 [add_comm]
+  exact λ _ => (this _).symm
+
+theorem _root_.QuantumSet.starAlgEquiv_commutes_with_modAut_of_isometry'
+  {f : A ≃⋆ₐ[ℂ] B} (hf : Isometry f) :
+  f.toLinearMap.comp (modAut ((2 * k A) + 1)).toLinearMap =
+    (modAut ((2 * k B) + 1)).toLinearMap.comp f.toLinearMap :=
+by
+  have := _root_.QuantumSet.starAlgEquiv_commutes_with_modAut_of_isometry hf
+  simp only [AlgEquiv.ext_iff, AlgEquiv.trans_apply,
+    LinearMap.ext_iff, LinearMap.comp_apply, StarAlgEquiv.coe_toAlgEquiv,
+    StarAlgEquiv.toLinearMap_apply, AlgEquiv.toLinearMap_apply] at this ⊢
+  exact this
+
 set_option synthInstance.maxHeartbeats 0 in
 private noncomputable def tenSwap_Psi_aux :
   (A →ₗ[ℂ] B) →ₗ[ℂ] (B ⊗[ℂ] Aᵐᵒᵖ) where

diff --git a/Monlib/LinearAlgebra/QuantumSet/Symm.lean b/Monlib/LinearAlgebra/QuantumSet/Symm.lean
@@ -251,25 +251,6 @@ theorem commute_real_real {R A : Type _} [Semiring R] [StarRing R] [AddCommMonoi
   simp_rw [Commute, SemiconjBy, LinearMap.mul_eq_comp, ← LinearMap.real_comp, ←
     LinearMap.real_inj_eq]
 
-theorem QuantumSet.modAut_real (r : ℝ) :
-    (ha.modAut r).toLinearMap.real = (ha.modAut (-r)).toLinearMap :=
-by
-  rw [LinearMap.ext_iff]
-  intro
-  simp_rw [LinearMap.real_apply, AlgEquiv.toLinearMap_apply, ha.modAut_star, star_star]
-
-theorem _root_.AlgEquiv.linearMap_comp_eq_iff {R E₁ E₂ E₃ : Type _} [CommSemiring R] [Semiring E₁] [Semiring E₂]
-    [AddCommMonoid E₃] [Algebra R E₁] [Algebra R E₂] [Module R E₃]
-    (f : E₁ ≃ₐ[R] E₂) (x : E₂ →ₗ[R] E₃) (y : E₁ →ₗ[R] E₃) :
-    x ∘ₗ f.toLinearMap = y ↔ x = y ∘ₗ f.symm.toLinearMap :=
-by aesop
-theorem _root_.AlgEquiv.comp_linearMap_eq_iff
-  {R E₁ E₂ E₃ : Type _} [CommSemiring R] [Semiring E₁] [Semiring E₂]
-  [AddCommMonoid E₃] [Algebra R E₁] [Algebra R E₂] [Module R E₃]
-  (f : E₁ ≃ₐ[R] E₂) (x : E₃ →ₗ[R] E₁) (y : E₃ →ₗ[R] E₂) :
-  f.toLinearMap ∘ₗ x = y ↔ x = f.symm.toLinearMap ∘ₗ y :=
-by aesop
-
 theorem linearMap_commute_modAut_pos_neg (r : ℝ) (x : B →ₗ[ℂ] B) :
     Commute x (hb.modAut r).toLinearMap ↔
       Commute x (hb.modAut (-r)).toLinearMap :=