Exact source: MathlibAnnex/Analysis/CStarAlgebra/ShellMatching.lean, lines 19–20.
Back to Exact projection links for one approximately inner automorphism
1import Mathlib.Algebra.Star.Unitary 2 3/-! 4# Exact shell matching 5 6The algebraic tail of shell matching. Once two projection shells are exactly 7unitarily matched after an auxiliary conjugation, the displayed link has both 8required support identities. 9-/ 10 11set_option autoImplicit false 12 13namespace MathlibAnnex.CStarAlgebra 14 15variable {A : Type*} [Semiring A] [StarRing A] 16 17/-- 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) * e 20 21/-- If `t` takes `e` to the conjugate of `f` by `g`, then `g⁺ t e` has initial 22support `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 := by 28 constructor 29 · 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 · calc 35 matchedLink g t e * star (matchedLink g t e) = 36 star (g : A) * ((t : A) * e * star (t : A)) * (g : A) := by 37 simp only [matchedLink, star_mul, star_star, he.isSelfAdjoint.star_eq] 38 rw [mul_assoc (star (g : A) * (t : A)) e 39 (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 := by 44 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] 48 49end MathlibAnnex.CStarAlgebra