Exact source: MathlibAnnex/Analysis/CStarAlgebra/ShellMatching.lean
Pinned GitHub source · Raw UTF-8 source
Back to Exact projection links for one approximately inner automorphism
1import Mathlib.Algebra.Star.Unitary23/-!4# Exact shell matching56The algebraic tail of shell matching. Once two projection shells are exactly7unitarily matched after an auxiliary conjugation, the displayed link has both8required support identities.9-/1011set_option autoImplicit false1213namespace MathlibAnnex.CStarAlgebra1415variable {A : Type*} [Semiring A] [StarRing A]1617/-- The partial-isometry link obtained after exact matching of two shells. -/18def matchedLink (g t : unitary A) (e : A) : A :=19 star (g : A) * (t : A) * e2021/-- If `t` takes `e` to the conjugate of `f` by `g`, then `g⁺ t e` has initial22support `e` and final support `f`. -/23theorem matchedLink_supports (g t : unitary A) (e f : A)24 (he : IsStarProjection e)25 (hmatch : (t : A) * e * star (t : A) = (g : A) * f * star (g : A)) :26 star (matchedLink g t e) * matchedLink g t e = e ∧27 matchedLink g t e * star (matchedLink g t e) = f := by28 constructor29 · simp only [matchedLink, star_mul, star_star, he.isSelfAdjoint.star_eq, mul_assoc]30 rw [← mul_assoc (g : A) (star (g : A)) ((t : A) * e),31 Unitary.mul_star_self_of_mem g.prop, one_mul,32 ← mul_assoc (star (t : A)) (t : A) e,33 Unitary.star_mul_self_of_mem t.prop, one_mul, he.isIdempotentElem.eq]34 · calc35 matchedLink g t e * star (matchedLink g t e) =36 star (g : A) * ((t : A) * e * star (t : A)) * (g : A) := by37 simp only [matchedLink, star_mul, star_star, he.isSelfAdjoint.star_eq]38 rw [mul_assoc (star (g : A) * (t : A)) e39 (e * (star (t : A) * (g : A)))]40 rw [← mul_assoc e e (star (t : A) * (g : A)), he.isIdempotentElem.eq]41 simp only [mul_assoc]42 _ = star (g : A) * ((g : A) * f * star (g : A)) * (g : A) := by rw [hmatch]43 _ = f := by44 simp only [mul_assoc]45 rw [Unitary.star_mul_self_of_mem g.prop, mul_one,46 ← mul_assoc (star (g : A)) (g : A) f,47 Unitary.star_mul_self_of_mem g.prop, one_mul]4849end MathlibAnnex.CStarAlgebra