Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/FiniteStages.lean
Pinned GitHub source · Raw UTF-8 source
Back to Constructing the normalized trace on the completed CAR algebra
1import Mathlib.Analysis.CStarAlgebra.CStarMatrix2import Mathlib.Analysis.CStarAlgebra.Hom3import Mathlib.Analysis.Normed.Module.FiniteDimension4import Mathlib.LinearAlgebra.Matrix.Kronecker5import Mathlib.RingTheory.SimpleRing.Congr6import Mathlib.RingTheory.SimpleRing.Matrix78/-!9# Binary matrix stages for the CAR inductive system1011This file constructs the actual finite-dimensional C-star algebras12`M_(2^n)(ℂ)` and the standard unital star embeddings `x ↦ x ⊗ 1₂`.13The embeddings are proved injective and hence isometric in the C-star norms.14-/1516set_option autoImplicit false1718open scoped ComplexOrder Matrix Kronecker1920namespace MathlibAnnex.CStarAlgebra.CAR2122/-- The `n`-th binary matrix stage. -/23abbrev Stage (n : ℕ) := CStarMatrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ2425/-- Reindex a pair consisting of an old coordinate and a bit as the next-stage coordinate. -/26def stepIndexEquiv (n : ℕ) : Fin (2 ^ n) × Fin 2 ≃ Fin (2 ^ (n + 1)) :=27 finProdFinEquiv.trans (finCongr (by simp [pow_succ]))2829set_option backward.isDefEq.respectTransparency false in30/-- Before reindexing, the standard CAR stage embedding is Kronecker product with `1₂`. -/31noncomputable def amplify (n : ℕ) :32 Stage n →⋆ₐ[ℂ] CStarMatrix (Fin (2 ^ n) × Fin 2) (Fin (2 ^ n) × Fin 2) ℂ where33 toFun x := CStarMatrix.ofMatrix34 (Matrix.kronecker (CStarMatrix.ofMatrix.symm x) (1 : Matrix (Fin 2) (Fin 2) ℂ))35 map_one' := by36 change Matrix.kronecker (1 : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ)37 (1 : Matrix (Fin 2) (Fin 2) ℂ) = 138 exact Matrix.one_kronecker_one39 map_mul' x y := by40 change Matrix.kronecker (x * y) (1 : Matrix (Fin 2) (Fin 2) ℂ) =41 Matrix.kronecker x 1 * Matrix.kronecker y 142 simpa using Matrix.mul_kronecker_mul x y43 (1 : Matrix (Fin 2) (Fin 2) ℂ) (1 : Matrix (Fin 2) (Fin 2) ℂ)44 map_zero' := by45 change Matrix.kronecker (0 : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ)46 (1 : Matrix (Fin 2) (Fin 2) ℂ) = 047 exact Matrix.zero_kronecker _48 map_add' x y := by49 change Matrix.kronecker (x + y) (1 : Matrix (Fin 2) (Fin 2) ℂ) =50 Matrix.kronecker x 1 + Matrix.kronecker y 151 exact Matrix.add_kronecker _ _ _52 commutes' r := by53 ext ⟨i, b⟩ ⟨j, c⟩54 by_cases hij : i = j <;> by_cases hbc : b = c <;>55 simp [CStarMatrix.algebraMap_apply, Prod.ext_iff, hij, hbc]56 map_star' x := by57 ext ⟨i, b⟩ ⟨j, c⟩58 by_cases hbc : b = c59 · subst c60 simp [CStarMatrix.star_apply]61 · simp [CStarMatrix.star_apply, hbc, Ne.symm hbc]6263theorem amplify_injective (n : ℕ) : Function.Injective (amplify n) := by64 intro x y hxy65 apply CStarMatrix.ext66 intro i j67 have hentry := congrFun (congrFun hxy (i, (0 : Fin 2))) (j, (0 : Fin 2))68 simpa [amplify, Matrix.kronecker_apply] using hentry6970/-- The standard diagonal amplification is not onto: it has no matrix entry71between the two new bit coordinates. Thus it must not be confused with an72ambient matrix-algebra equivalence. -/73theorem amplify_not_surjective (n : ℕ) : ¬ Function.Surjective (amplify n) := by74 intro hsurj75 let y : CStarMatrix (Fin (2 ^ n) × Fin 2) (Fin (2 ^ n) × Fin 2) ℂ :=76 CStarMatrix.ofMatrix (Matrix.single (0, 0) (0, 1) 1)77 obtain ⟨x, hx⟩ := hsurj y78 have hentry := congrFun (congrFun hx ((0, 0) : Fin (2 ^ n) × Fin 2))79 ((0, 1) : Fin (2 ^ n) × Fin 2)80 simp [amplify, y, Matrix.single] at hentry8182/-- The standard map from stage `n` to stage `n+1`. -/83noncomputable def step (n : ℕ) : Stage n →⋆ₐ[ℂ] Stage (n + 1) :=84 (CStarMatrix.reindexₐ ℂ ℂ (stepIndexEquiv n)).toStarAlgHom.comp (amplify n)8586theorem step_injective (n : ℕ) : Function.Injective (step n) :=87 (CStarMatrix.reindexₐ ℂ ℂ (stepIndexEquiv n)).injective.comp (amplify_injective n)8889/-- Each standard stage embedding preserves the actual C-star norm. -/90theorem norm_step (n : ℕ) (x : Stage n) : ‖step n x‖ = ‖x‖ :=91 NonUnitalStarAlgHom.norm_map (step n) (step_injective n) x9293/-- Each finite matrix stage is nonzero. -/94instance stageNontrivial (n : ℕ) : Nontrivial (Stage n) := inferInstance9596/-- Full finite matrix stages are simple rings. -/97noncomputable instance stageIsSimpleRing (n : ℕ) : IsSimpleRing (Stage n) :=98 IsSimpleRing.of_ringEquiv CStarMatrix.ofMatrixRingEquiv inferInstance99100/-- Each matrix stage is finite-dimensional over `ℂ`. -/101noncomputable instance stageFiniteDimensional (n : ℕ) : FiniteDimensional ℂ (Stage n) :=102 LinearEquiv.finiteDimensional (CStarMatrix.ofMatrixₗ (R := ℂ))103104/-- Each finite stage is separable in its actual C-star norm topology. -/105noncomputable instance stageSeparableSpace (n : ℕ) :106 TopologicalSpace.SeparableSpace (Stage n) :=107 let e : Stage n ≃L[ℂ] Fin (Module.finrank ℂ (Stage n)) → ℂ :=108 ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℂ).symm109 e.symm.surjective.denseRange.separableSpace e.symm.continuous110111end MathlibAnnex.CStarAlgebra.CAR