Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/FiniteStages.lean, lines 86–87.
Back to Constructing the normalized trace on the completed CAR algebra
1import Mathlib.Analysis.CStarAlgebra.CStarMatrix 2import Mathlib.Analysis.CStarAlgebra.Hom 3import Mathlib.Analysis.Normed.Module.FiniteDimension 4import Mathlib.LinearAlgebra.Matrix.Kronecker 5import Mathlib.RingTheory.SimpleRing.Congr 6import Mathlib.RingTheory.SimpleRing.Matrix 7 8/-! 9# Binary matrix stages for the CAR inductive system 10 11This file constructs the actual finite-dimensional C-star algebras 12`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-/ 15 16set_option autoImplicit false 17 18open scoped ComplexOrder Matrix Kronecker 19 20namespace MathlibAnnex.CStarAlgebra.CAR 21 22/-- The `n`-th binary matrix stage. -/ 23abbrev Stage (n : ℕ) := CStarMatrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ 24 25/-- 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])) 28 29set_option backward.isDefEq.respectTransparency false in 30/-- 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) ℂ where 33 toFun x := CStarMatrix.ofMatrix 34 (Matrix.kronecker (CStarMatrix.ofMatrix.symm x) (1 : Matrix (Fin 2) (Fin 2) ℂ)) 35 map_one' := by 36 change Matrix.kronecker (1 : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) 37 (1 : Matrix (Fin 2) (Fin 2) ℂ) = 1 38 exact Matrix.one_kronecker_one 39 map_mul' x y := by 40 change Matrix.kronecker (x * y) (1 : Matrix (Fin 2) (Fin 2) ℂ) = 41 Matrix.kronecker x 1 * Matrix.kronecker y 1 42 simpa using Matrix.mul_kronecker_mul x y 43 (1 : Matrix (Fin 2) (Fin 2) ℂ) (1 : Matrix (Fin 2) (Fin 2) ℂ) 44 map_zero' := by 45 change Matrix.kronecker (0 : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) 46 (1 : Matrix (Fin 2) (Fin 2) ℂ) = 0 47 exact Matrix.zero_kronecker _ 48 map_add' x y := by 49 change Matrix.kronecker (x + y) (1 : Matrix (Fin 2) (Fin 2) ℂ) = 50 Matrix.kronecker x 1 + Matrix.kronecker y 1 51 exact Matrix.add_kronecker _ _ _ 52 commutes' r := by 53 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 := by 57 ext ⟨i, b⟩ ⟨j, c⟩ 58 by_cases hbc : b = c 59 · subst c 60 simp [CStarMatrix.star_apply] 61 · simp [CStarMatrix.star_apply, hbc, Ne.symm hbc] 62 63theorem amplify_injective (n : ℕ) : Function.Injective (amplify n) := by 64 intro x y hxy 65 apply CStarMatrix.ext 66 intro i j 67 have hentry := congrFun (congrFun hxy (i, (0 : Fin 2))) (j, (0 : Fin 2)) 68 simpa [amplify, Matrix.kronecker_apply] using hentry 69 70/-- The standard diagonal amplification is not onto: it has no matrix entry 71between the two new bit coordinates. Thus it must not be confused with an 72ambient matrix-algebra equivalence. -/ 73theorem amplify_not_surjective (n : ℕ) : ¬ Function.Surjective (amplify n) := by 74 intro hsurj 75 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 y 78 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 hentry 81 82/-- 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) 85 86theorem step_injective (n : ℕ) : Function.Injective (step n) := 87 (CStarMatrix.reindexₐ ℂ ℂ (stepIndexEquiv n)).injective.comp (amplify_injective n) 88 89/-- 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) x 92 93/-- Each finite matrix stage is nonzero. -/ 94instance stageNontrivial (n : ℕ) : Nontrivial (Stage n) := inferInstance 95 96/-- Full finite matrix stages are simple rings. -/ 97noncomputable instance stageIsSimpleRing (n : ℕ) : IsSimpleRing (Stage n) := 98 IsSimpleRing.of_ringEquiv CStarMatrix.ofMatrixRingEquiv inferInstance 99 100/-- Each matrix stage is finite-dimensional over `ℂ`. -/ 101noncomputable instance stageFiniteDimensional (n : ℕ) : FiniteDimensional ℂ (Stage n) := 102 LinearEquiv.finiteDimensional (CStarMatrix.ofMatrixₗ (R := ℂ)) 103 104/-- 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 ℂ).symm 109 e.symm.surjective.denseRange.separableSpace e.symm.continuous 110 111end MathlibAnnex.CStarAlgebra.CAR