Lean 源码

此页定位 blueprint 引用的 Lean 声明，展示已验证的源码快照，并非完整的 API 文档。Lean 4.33.1。

GroupAlgebra.lean

源码 SHA-256：1c6c0899fe9bc9f7860f291ba7c5573353d18a3c5809258769d689bc39da8ad4

 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Analysis.Complex.Basic
 
 /-!
 # The complex group algebra of an arbitrary group
 
 This file verifies the algebraic starting point for the reduced group C*-algebra.
 Multiplication is Mathlib's convolution product, not pointwise multiplication.
 The involution conjugates coefficients and reverses group elements.
 No topology, countability, regular representation, or completion is assumed here.
 -/
 
 noncomputable section
 
 namespace BC4lean
 
 /-- Finitely supported complex coefficients with convolution multiplication. -/
 abbrev GroupAlgebra (Γ : Type*) := MonoidAlgebra ℂ Γ
 
 namespace GroupAlgebra
 
 variable {Γ : Type*} [Group Γ]
 
 /-- The basis vector at a group element. -/
 def delta (g : Γ) : GroupAlgebra Γ := MonoidAlgebra.single g 1
 
 /-- The finite coefficient ℓ¹-norm; no normed-algebra instance is claimed. -/
 def l1Norm (a : GroupAlgebra Γ) : ℝ := ∑ g ∈ a.coeff.support, ‖a.coeff g‖
 
 /-- Conjugation of coefficients followed by inversion of the group index. -/
 def involution (a : GroupAlgebra Γ) : GroupAlgebra Γ :=
   .ofCoeff (Finsupp.equivMapDomain (Equiv.inv Γ)
     (a.coeff.mapRange star (star_zero ℂ)))
 
 @[simp]
 theorem coeff_involution (a : GroupAlgebra Γ) (g : Γ) :
     (involution a).coeff g = star (a.coeff g⁻¹) := rfl
 
 @[simp]
 theorem involution_zero : involution (0 : GroupAlgebra Γ) = 0 := by
   ext g
   simp
 
 theorem involution_add (a b : GroupAlgebra Γ) :
     involution (a + b) = involution a + involution b := by
   ext g
   simp
 
 theorem involution_smul (z : ℂ) (a : GroupAlgebra Γ) :
     involution (z • a) = star z • involution a := by
   ext g
   simp
 
 @[simp]
 theorem involution_involution (a : GroupAlgebra Γ) :
     involution (involution a) = a := by
   ext g
   simp
 
 @[simp]
 theorem involution_single (g : Γ) (z : ℂ) :
     involution (MonoidAlgebra.single g z) = MonoidAlgebra.single g⁻¹ (star z) := by
   simp only [involution, MonoidAlgebra.coeff_single, Finsupp.mapRange_single,
     Finsupp.equivMapDomain_single, Equiv.inv_apply, MonoidAlgebra.ofCoeff_single]
 
 theorem involution_mul (a b : GroupAlgebra Γ) :
     involution (a * b) = involution b * involution a := by
   induction a using MonoidAlgebra.induction_linear with
   | zero => simp
   | add a c ha hc => simp only [add_mul, involution_add, ha, hc, mul_add]
   | single g z =>
     induction b using MonoidAlgebra.induction_linear with
     | zero => simp
     | add b c hb hc => simp only [mul_add, involution_add, hb, hc, add_mul]
     | single h w => simp [MonoidAlgebra.single_mul_single, mul_inv_rev, mul_comm]
 
 /-- The group-algebra star is conjugation combined with inversion. -/
 instance instStar : Star (GroupAlgebra Γ) := ⟨involution⟩
 
 /-- Convolution and the group-algebra involution form a star ring. -/
 instance instStarRing : StarRing (GroupAlgebra Γ) where
   star_involutive := involution_involution
   star_mul := involution_mul
   star_add := involution_add
 
 /-- The involution is conjugate-linear over the complex scalars. -/
 instance instStarModule : StarModule ℂ (GroupAlgebra Γ) where
   star_smul := involution_smul
 
 @[simp]
 theorem coeff_star (a : GroupAlgebra Γ) (g : Γ) :
     (star a).coeff g = star (a.coeff g⁻¹) := coeff_involution a g
 
 /-- The multiplication agrees with the blueprint's convolution formula. -/
 theorem coeff_convolution (a b : GroupAlgebra Γ) (h : Γ) :
     (a * b).coeff h = ∑ g ∈ a.coeff.support, a.coeff g * b.coeff (g⁻¹ * h) :=
   MonoidAlgebra.coeff_mul_apply_left a b h
 
 @[simp]
 theorem delta_one : delta (1 : Γ) = 1 := rfl
 
 @[simp]
 theorem delta_mul (g h : Γ) : delta g * delta h = delta (g * h) := by
   simp [delta, MonoidAlgebra.single_mul_single]
 
 @[simp]
 theorem delta_star (g : Γ) : star (delta g) = delta g⁻¹ := by
   change involution (MonoidAlgebra.single g 1) = _
   simp [delta]
 
 theorem delta_expansion (a : GroupAlgebra Γ) :
     ∑ g ∈ a.coeff.support, a.coeff g • delta g = a := by
   simpa [delta, MonoidAlgebra.smul_single, Finsupp.sum] using a.sum_coeff_single
 
 open scoped Pointwise in
 theorem support_convolution [DecidableEq Γ] (a b : GroupAlgebra Γ) :
     (a * b).coeff.support ⊆ a.coeff.support * b.coeff.support :=
   MonoidAlgebra.support_coeff_mul_subset a b
 
 theorem support_star (a : GroupAlgebra Γ) :
     (star a).coeff.support = a.coeff.support.map (Equiv.inv Γ).toEmbedding := by
   classical
   ext g
   simp only [Finsupp.mem_support_iff, coeff_star, star_ne_zero, Finset.mem_map,
     Equiv.toEmbedding_apply, Equiv.inv_apply]
   constructor
   · intro h
     exact ⟨g⁻¹, h, inv_inv g⟩
   · rintro ⟨h, hh, rfl⟩
     simpa using hh
 
 theorem convolution_bilinear (a b c : GroupAlgebra Γ) (z : ℂ) :
     (a + b) * c = a * c + b * c ∧ a * (b + c) = a * b + a * c ∧
     (z • a) * b = z • (a * b) ∧ a * (z • b) = z • (a * b) :=
   ⟨add_mul a b c, mul_add a b c, smul_mul_assoc z a b, mul_smul_comm z a b⟩
 
 /-- The laws appearing together in the blueprint's algebraic proposition. -/
 theorem star_algebra_laws (a b c : GroupAlgebra Γ) (z w : ℂ) :
     (a * b) * c = a * (b * c) ∧
     (delta 1) * a = a ∧ a * (delta 1) = a ∧
     star (a * b) = star b * star a ∧ star (star a) = a ∧
     star (z • a + w • b) = star z • star a + star w • star b := by
   simp only [mul_assoc, delta_one, one_mul, mul_one, star_mul, star_star,
     star_add, star_smul, and_self]
 
 end GroupAlgebra
 end BC4lean

L2Group.lean

源码 SHA-256：c29e90c17d29b0a55f4ca3e568c275b8246603e15b0f7ebb6b41b43d62d410d4

 import Mathlib.Analysis.InnerProductSpace.l2Space
 
 /-!
 # Square-summable functions and the delta Hilbert basis
 
 The index type need not be countable or carry a group structure.
 Mathlib supplies the complete complex inner product space structure on `lp`.
 Sums are unordered sums over finite subsets, not a chosen enumeration.
 -/
 
 noncomputable section
 
 namespace BC4lean
 
 open scoped ENNReal
 
 /-- Square-summable complex-valued functions, with their Hilbert space structure. -/
 abbrev L2Group (Γ : Type*) := lp (fun _ : Γ => ℂ) 2
 
 namespace L2Group
 
 variable {Γ : Type*}
 
 /-- Membership is exactly summability of the squared coefficient norms. -/
 theorem mem_iff (f : Γ → ℂ) :
     Memℓp f 2 ↔ Summable (fun g => ‖f g‖ ^ (2 : ℕ)) := by
   simpa using (memℓp_gen_iff (by norm_num : 0 < (2 : ℝ≥0∞).toReal) (f := f))
 
 /-- Completeness is inherited from Mathlib's `lp` construction. -/
 theorem completeSpace : CompleteSpace (L2Group Γ) := inferInstance
 
 theorem summable_norm_sq (ξ : L2Group Γ) : Summable (fun g => ‖ξ g‖ ^ (2 : ℕ)) :=
   (mem_iff ξ).mp (lp.memℓp ξ)
 
 theorem norm_sq (ξ : L2Group Γ) : ‖ξ‖ ^ (2 : ℕ) = ∑' g, ‖ξ g‖ ^ (2 : ℕ) := by
   simpa using lp.norm_rpow_eq_tsum (by norm_num : 0 < (2 : ℝ≥0∞).toReal) ξ
 
 theorem inner_eq_tsum (ξ η : L2Group Γ) :
     inner ℂ ξ η = ∑' g, star (ξ g) * η g := by
   simpa [RCLike.inner_apply, mul_comm] using lp.inner_eq_tsum (𝕜 := ℂ) ξ η
 
 theorem summable_inner (ξ η : L2Group Γ) :
     Summable (fun g => star (ξ g) * η g) := by
   simpa [RCLike.inner_apply, mul_comm] using lp.summable_inner (𝕜 := ℂ) ξ η
 
 /-- The delta vector at `g`. -/
 def delta (g : Γ) : L2Group Γ := by
   classical
   exact lp.single 2 g 1
 
 open scoped Classical in
 theorem delta_apply (g h : Γ) : delta g h = if h = g then 1 else 0 := by
   classical
   simp [delta, lp.single_apply, Pi.single_apply]
 
 @[simp] theorem delta_apply_self (g : Γ) : delta g g = 1 := by
   classical
   simp [delta_apply]
 
 @[simp] theorem norm_delta (g : Γ) : ‖delta g‖ = 1 := by
   classical
   simp only [delta, lp.norm_single (by norm_num : (0 : ℝ≥0∞) < 2), norm_one]
 
 /-- The identity coordinate representation gives the canonical Hilbert basis. -/
 def deltaBasis : HilbertBasis Γ ℂ (L2Group Γ) :=
   HilbertBasis.ofRepr (LinearIsometryEquiv.refl ℂ _)
 
 @[simp] theorem deltaBasis_apply (g : Γ) : deltaBasis g = delta g := rfl
 
 theorem delta_orthonormal : Orthonormal ℂ (delta : Γ → L2Group Γ) :=
   deltaBasis.orthonormal
 
 theorem delta_dense_span :
     (Submodule.span ℂ (Set.range (delta : Γ → L2Group Γ))).topologicalClosure = ⊤ :=
   deltaBasis.dense_span
 
 theorem hasSum_delta (ξ : L2Group Γ) : HasSum (fun g => ξ g • delta g) ξ :=
   deltaBasis.hasSum_repr ξ
 
 @[simp] theorem inner_delta (g : Γ) (ξ : L2Group Γ) : inner ℂ (delta g) ξ = ξ g :=
   (deltaBasis.repr_apply_apply ξ g).symm
 
 theorem norm_apply_le (ξ : L2Group Γ) (g : Γ) : ‖ξ g‖ ≤ ‖ξ‖ :=
   lp.norm_apply_le_norm (by norm_num : (2 : ℝ≥0∞) ≠ 0) ξ g
 
 end L2Group
 end BC4lean

LeftRegularRepresentation.lean

源码 SHA-256：400a9225e55f140dcdca8e494397443be99304852e0d69a4cee8c43e9fd6d0f9

 import BC4lean.L2Group
 import Mathlib.Algebra.Star.Unitary
 import Mathlib.Analysis.InnerProductSpace.Adjoint
 
 /-!
 # First milestone: the left regular representation
 
 We construct translations directly on square-summable functions. No countability
 assumption is required. All groups in this module are regarded as discrete.
 -/
 
 noncomputable section
 
 namespace BC4lean
 
 open scoped ENNReal
 
 universe u
 
 variable {Γ : Type u} [Group Γ]
 
 /-- Left translation preserves square summability by reindexing the sum. -/
 theorem memLp_leftTranslate (g : Γ) (ξ : L2Group Γ) :
     Memℓp (fun h => ξ (g⁻¹ * h)) 2 := by
   apply memℓp_gen
   exact (Equiv.mulLeft g⁻¹).summable_iff.mpr
     ((lp.memℓp ξ).summable (by norm_num))
 
 /-- Left translation, before packaging it as a linear isometry. -/
 def leftTranslate (g : Γ) (ξ : L2Group Γ) : L2Group Γ :=
   ⟨fun h => ξ (g⁻¹ * h), memLp_leftTranslate g ξ⟩
 
 @[simp] theorem leftTranslate_apply (g h : Γ) (ξ : L2Group Γ) :
     leftTranslate g ξ h = ξ (g⁻¹ * h) := rfl
 
 @[simp] theorem leftTranslate_one (ξ : L2Group Γ) : leftTranslate 1 ξ = ξ := by
   apply lp.ext
   funext h
   simp
 
 theorem leftTranslate_mul (g h : Γ) (ξ : L2Group Γ) :
     leftTranslate (g * h) ξ = leftTranslate g (leftTranslate h ξ) := by
   apply lp.ext
   funext k
   simp [mul_assoc]
 
 @[simp] theorem leftTranslate_inv_left (g : Γ) (ξ : L2Group Γ) :
     leftTranslate g⁻¹ (leftTranslate g ξ) = ξ := by
   rw [← leftTranslate_mul, inv_mul_cancel, leftTranslate_one]
 
 @[simp] theorem leftTranslate_inv_right (g : Γ) (ξ : L2Group Γ) :
     leftTranslate g (leftTranslate g⁻¹ ξ) = ξ := by
   rw [← leftTranslate_mul, mul_inv_cancel, leftTranslate_one]
 
 /-- Translations preserve the norm, by invariance of a sum under a bijection. -/
 @[simp] theorem norm_leftTranslate (g : Γ) (ξ : L2Group Γ) :
     ‖leftTranslate g ξ‖ = ‖ξ‖ := by
   rw [lp.norm_eq_tsum_rpow (by norm_num), lp.norm_eq_tsum_rpow (by norm_num)]
   congr 1
   exact (Equiv.mulLeft g⁻¹).tsum_eq (fun h => ‖ξ h‖ ^ (2 : ℝ≥0∞).toReal)
 
 /-- A unitary expressed as a complex-linear isometric equivalence. -/
 def leftRegular (g : Γ) : L2Group Γ ≃ₗᵢ[ℂ] L2Group Γ where
   toFun := leftTranslate g
   invFun := leftTranslate g⁻¹
   left_inv := leftTranslate_inv_left g
   right_inv := leftTranslate_inv_right g
   map_add' ξ η := by
     apply lp.ext
     rfl
   map_smul' c ξ := by
     apply lp.ext
     rfl
   norm_map' := norm_leftTranslate g
 
 @[simp] theorem leftRegular_apply (g h : Γ) (ξ : L2Group Γ) :
     leftRegular g ξ h = ξ (g⁻¹ * h) := rfl
 
 theorem leftRegular_inner (g : Γ) (ξ η : L2Group Γ) :
     inner ℂ (leftRegular g ξ) (leftRegular g η) = inner ℂ ξ η :=
   (leftRegular g).inner_map_map ξ η
 
 /-- The regular operator in the algebra of bounded complex-linear operators. -/
 def regularOperator (g : Γ) : L2Group Γ →L[ℂ] L2Group Γ :=
   (leftRegular g : L2Group Γ →L[ℂ] L2Group Γ)
 
 @[simp] theorem regularOperator_apply (g h : Γ) (ξ : L2Group Γ) :
     regularOperator g ξ h = ξ (g⁻¹ * h) := rfl
 
 @[simp] theorem regularOperator_one : regularOperator (1 : Γ) = 1 := by
   ext ξ h
   simp [regularOperator]
 
 @[simp] theorem regularOperator_mul (g h : Γ) :
     regularOperator (g * h) = regularOperator g * regularOperator h := by
   ext ξ k
   simp [regularOperator, mul_assoc]
 
 @[simp] theorem regularOperator_star (g : Γ) :
     star (regularOperator g) = regularOperator g⁻¹ := by
   change star (leftRegular g : L2Group Γ →L[ℂ] L2Group Γ) = _
   rw [LinearIsometryEquiv.star_eq_symm]
   rfl
 
 /-- Both unitary identities hold in the bounded-operator algebra. -/
 theorem regularOperator_unitary (g : Γ) :
     star (regularOperator g) * regularOperator g = 1 ∧
       regularOperator g * star (regularOperator g) = 1 := by
   constructor <;> simp [← regularOperator_mul]
 
 /-- The left regular representation, packaged as a multiplicative map. -/
 def operatorRepresentation : Γ →* (L2Group Γ →L[ℂ] L2Group Γ) where
   toFun := regularOperator
   map_one' := regularOperator_one
   map_mul' := regularOperator_mul
 
 /-- Translation carries the delta vector at `h` to the delta vector at `g * h`. -/
 @[simp] theorem regularOperator_delta (g h : Γ) :
     regularOperator g (L2Group.delta h) = L2Group.delta (g * h) := by
   classical
   ext k
   simp only [regularOperator_apply, L2Group.delta_apply, inv_mul_eq_iff_eq_mul]
 
 @[simp] theorem norm_regularOperator (g : Γ) : ‖regularOperator g‖ = 1 := by
   apply le_antisymm
   · apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one
     intro ξ
     change ‖leftTranslate g ξ‖ ≤ 1 * ‖ξ‖
     simp only [norm_leftTranslate, one_mul, le_refl]
   · have h := (regularOperator g).le_opNorm (L2Group.delta (1 : Γ))
     simpa only [regularOperator_delta, L2Group.norm_delta, mul_one] using h
 
 /-- The left regular representation with values in the unitary group. -/
 def regularRepresentation : Γ →* unitary (L2Group Γ →L[ℂ] L2Group Γ) where
   toFun g := ⟨regularOperator g, Unitary.mem_iff.mpr (regularOperator_unitary g)⟩
   map_one' := Subtype.ext regularOperator_one
   map_mul' g h := Subtype.ext (regularOperator_mul g h)
 
 @[simp] theorem regularRepresentation_coe (g : Γ) :
     (regularRepresentation g : L2Group Γ →L[ℂ] L2Group Γ) = regularOperator g := rfl
 
 @[simp] theorem regularRepresentation_apply (g h : Γ) (ξ : L2Group Γ) :
     (regularRepresentation g : L2Group Γ →L[ℂ] L2Group Γ) ξ h = ξ (g⁻¹ * h) := rfl
 
 end BC4lean

IntegratedRepresentation.lean

源码 SHA-256：6127ba4543ef7f420056752bcf1731c553a597fe59bc402b8b9af38146f48df0

 import BC4lean.GroupAlgebra
 import BC4lean.LeftRegularRepresentation
 import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
 
 /-! # The integrated regular representation and reduced norm
 
 All groups are regarded as discrete. No countability assumption is used.
 The algebra homomorphism is Mathlib's linear extension of the regular operators;
 compatibility with the group-algebra involution is proved below.
 -/
 
 noncomputable section
 
 namespace BC4lean
 
 variable {Γ : Type*} [Group Γ]
 
 /-- The linear extension of the regular operators to the complex group algebra. -/
 def integratedRepresentation : GroupAlgebra Γ →ₐ[ℂ] (L2Group Γ →L[ℂ] L2Group Γ) :=
   MonoidAlgebra.lift ℂ _ Γ operatorRepresentation
 
 theorem integratedRepresentation_sum (a : GroupAlgebra Γ) :
     integratedRepresentation a = ∑ g ∈ a.coeff.support, a.coeff g • regularOperator g :=
   MonoidAlgebra.lift_apply operatorRepresentation a
 
 @[simp] theorem integratedRepresentation_single (g : Γ) (z : ℂ) :
     integratedRepresentation (MonoidAlgebra.single g z) = z • regularOperator g :=
   MonoidAlgebra.lift_single operatorRepresentation g z
 
 @[simp] theorem integratedRepresentation_delta (g : Γ) :
     integratedRepresentation (GroupAlgebra.delta g) = regularOperator g := by
   simp [GroupAlgebra.delta]
 
 theorem integratedRepresentation_apply (a : GroupAlgebra Γ) (ξ : L2Group Γ) (h : Γ) :
     integratedRepresentation a ξ h =
       ∑ g ∈ a.coeff.support, a.coeff g * ξ (g⁻¹ * h) := by
   rw [integratedRepresentation_sum]
   simp only [sum_apply, smul_apply, lp.coeFn_sum,
     lp.coeFn_smul, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, regularOperator_apply]
 
 theorem norm_integratedRepresentation_le (a : GroupAlgebra Γ) :
     ‖integratedRepresentation a‖ ≤ GroupAlgebra.l1Norm a := by
   rw [integratedRepresentation_sum]
   calc
     _ ≤ ∑ g ∈ a.coeff.support, ‖a.coeff g • regularOperator g‖ := norm_sum_le _ _
     _ = GroupAlgebra.l1Norm a := by simp [GroupAlgebra.l1Norm, norm_smul]
 
 @[simp] theorem integratedRepresentation_star (a : GroupAlgebra Γ) :
     integratedRepresentation (star a) = star (integratedRepresentation a) := by
   induction a using MonoidAlgebra.induction_linear with
   | zero => simp
   | add a b ha hb => simp only [star_add, map_add, ha, hb]
   | single g z =>
     change integratedRepresentation (GroupAlgebra.involution (MonoidAlgebra.single g z)) = _
     simp only [GroupAlgebra.involution_single, integratedRepresentation_single,
       star_smul, regularOperator_star]
 
 /-- The integrated representation as a unital complex star-algebra homomorphism. -/
 def integratedStarHom : GroupAlgebra Γ →⋆ₐ[ℂ] (L2Group Γ →L[ℂ] L2Group Γ) where
   toAlgHom := integratedRepresentation
   map_star' := integratedRepresentation_star
 
 @[simp] theorem integratedStarHom_apply (a : GroupAlgebra Γ) :
     integratedStarHom a = integratedRepresentation a := rfl
 
 /-- Coefficients are recovered by applying the operator to the identity delta vector. -/
 @[simp] theorem integratedRepresentation_delta_one (a : GroupAlgebra Γ) (h : Γ) :
     integratedRepresentation a (L2Group.delta 1) h = a.coeff h := by
   classical
   induction a using MonoidAlgebra.induction_linear with
   | zero => simp
   | add a b ha hb => simpa using congrArg₂ (· + ·) ha hb
   | single g z =>
     simp [L2Group.delta_apply, Finsupp.single_apply, eq_comm]
 
 theorem integratedRepresentation_injective :
     Function.Injective (integratedRepresentation (Γ := Γ)) := by
   intro a b hab
   apply MonoidAlgebra.ext
   apply Finsupp.ext
   intro h
   simpa using congrArg (fun T : L2Group Γ →L[ℂ] L2Group Γ => T (L2Group.delta 1) h) hab
 
 /-- The coefficient function as an ℓ²-vector; the next theorem identifies it pointwise. -/
 def GroupAlgebra.toL2 (a : GroupAlgebra Γ) : L2Group Γ :=
   integratedRepresentation a (L2Group.delta 1)
 
 @[simp] theorem GroupAlgebra.toL2_apply (a : GroupAlgebra Γ) (h : Γ) :
     a.toL2 h = a.coeff h := integratedRepresentation_delta_one a h
 
 theorem norm_toL2_le (a : GroupAlgebra Γ) : ‖a.toL2‖ ≤ ‖integratedRepresentation a‖ := by
   simpa only [GroupAlgebra.toL2, L2Group.norm_delta, mul_one] using
     (integratedRepresentation a).le_opNorm (L2Group.delta (1 : Γ))
 
 theorem norm_coeff_le (a : GroupAlgebra Γ) (h : Γ) :
     ‖a.coeff h‖ ≤ ‖integratedRepresentation a‖ := by
   simpa only [GroupAlgebra.toL2_apply] using
     (L2Group.norm_apply_le a.toL2 h).trans (norm_toL2_le a)
 
 /-- The algebraic image is exactly the finite complex span of the regular operators. -/
 theorem integratedRepresentation_range :
     (integratedRepresentation (Γ := Γ)).range.toSubmodule =
       Submodule.span ℂ (Set.range (regularOperator (Γ := Γ))) := by
   apply le_antisymm
   · rintro T ⟨a, rfl⟩
     change integratedRepresentation a ∈ Submodule.span ℂ (Set.range regularOperator)
     induction a using MonoidAlgebra.induction_linear with
     | zero => simp
     | add a b ha hb =>
       rw [map_add]
       exact Submodule.add_mem _ ha hb
     | single g z =>
       rw [integratedRepresentation_single]
       exact Submodule.smul_mem _ z (Submodule.subset_span ⟨g, rfl⟩)
   · apply Submodule.span_le.mpr
     rintro T ⟨g, rfl⟩
     exact ⟨GroupAlgebra.delta g, integratedRepresentation_delta g⟩
 
 /-- The reduced norm is the norm of the faithful regular operator. -/
 def reducedNorm (a : GroupAlgebra Γ) : ℝ := ‖integratedRepresentation a‖
 
 theorem reducedNorm_nonneg (a : GroupAlgebra Γ) : 0 ≤ reducedNorm a := norm_nonneg _
 
 @[simp] theorem reducedNorm_eq_zero (a : GroupAlgebra Γ) : reducedNorm a = 0 ↔ a = 0 := by
   simp only [reducedNorm, norm_eq_zero, map_eq_zero_iff _ integratedRepresentation_injective]
 
 theorem reducedNorm_add_le (a b : GroupAlgebra Γ) :
     reducedNorm (a + b) ≤ reducedNorm a + reducedNorm b := by
   simpa only [reducedNorm, map_add] using norm_add_le (integratedRepresentation a) _
 
 theorem reducedNorm_smul (z : ℂ) (a : GroupAlgebra Γ) :
     reducedNorm (z • a) = ‖z‖ * reducedNorm a := by
   simp only [reducedNorm, map_smul, norm_smul]
 
 theorem reducedNorm_mul_le (a b : GroupAlgebra Γ) :
     reducedNorm (a * b) ≤ reducedNorm a * reducedNorm b := by
   simpa only [reducedNorm, map_mul] using norm_mul_le (integratedRepresentation a) _
 
 @[simp] theorem reducedNorm_star (a : GroupAlgebra Γ) : reducedNorm (star a) = reducedNorm a := by
   unfold reducedNorm
   rw [integratedRepresentation_star]
   exact norm_star (integratedRepresentation a)
 
 theorem reducedNorm_cstar (a : GroupAlgebra Γ) :
     reducedNorm (star a * a) = reducedNorm a ^ 2 := by
   unfold reducedNorm
   rw [map_mul, integratedRepresentation_star]
   simpa only [pow_two] using CStarRing.norm_star_mul_self (x := integratedRepresentation a)
 
 @[simp] theorem reducedNorm_delta (g : Γ) : reducedNorm (GroupAlgebra.delta g) = 1 := by
   simp only [reducedNorm, integratedRepresentation_delta, norm_regularOperator]
 
 theorem reducedNorm_bounds (a : GroupAlgebra Γ) :
     ‖a.toL2‖ ≤ reducedNorm a ∧ reducedNorm a ≤ GroupAlgebra.l1Norm a :=
   ⟨norm_toL2_le a, norm_integratedRepresentation_le a⟩
 
 end BC4lean

ReducedGroupCStar.lean

源码 SHA-256：96917b6794dc08f3ea214d34285484632b8f7c4a1247dfd480949707cd2da173

 import BC4lean.IntegratedRepresentation
 import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
 
 /-! # The concrete reduced group C⋆-algebra
 
 The underlying set is the operator-norm closure of the integrated regular image.
 The C⋆-algebra structure is inherited from bounded operators on ℓ²(Γ).
 -/
 
 noncomputable section
 
 namespace BC4lean
 
 variable (Γ : Type*) [Group Γ]
 
 /-- The closed star subalgebra generated by the integrated regular image. -/
 def reducedAlgebra : StarSubalgebra ℂ (L2Group Γ →L[ℂ] L2Group Γ) :=
   (integratedStarHom (Γ := Γ)).range.topologicalClosure
 
 /-- The concrete reduced group C⋆-algebra. -/
 abbrev ReducedGroupCStar := ↥(reducedAlgebra Γ)
 
 variable {Γ}
 
 theorem reducedAlgebra_coe_eq_closure_range :
     (reducedAlgebra Γ : Set (L2Group Γ →L[ℂ] L2Group Γ)) =
       closure (Set.range (integratedRepresentation (Γ := Γ))) := rfl
 
 theorem reducedAlgebra_isClosed :
     IsClosed (reducedAlgebra Γ : Set (L2Group Γ →L[ℂ] L2Group Γ)) :=
   isClosed_closure
 
 instance reducedGroupCStarAlgebra : CStarAlgebra (ReducedGroupCStar Γ) :=
   StarSubalgebra.cstarAlgebra _ (h_closed := reducedAlgebra_isClosed)
 
 /-- The identity regular operator has norm one, also for the trivial group. -/
 instance regularOperatorsNormOne : NormOneClass (L2Group Γ →L[ℂ] L2Group Γ) where
   norm_one := by
     simpa only [regularOperator_one] using norm_regularOperator (1 : Γ)
 
 instance reducedGroupCStarNormOne : NormOneClass (ReducedGroupCStar Γ) where
   norm_one := by
     change ‖(1 : L2Group Γ →L[ℂ] L2Group Γ)‖ = 1
     exact norm_one
 
 /-- The canonical faithful star homomorphism with dense image. -/
 def integratedToReduced : GroupAlgebra Γ →⋆ₐ[ℂ] ReducedGroupCStar Γ :=
   integratedStarHom.codRestrict (reducedAlgebra Γ)
     (fun a => subset_closure ⟨a, rfl⟩)
 
 @[simp] theorem integratedToReduced_coe (a : GroupAlgebra Γ) :
     (integratedToReduced a : L2Group Γ →L[ℂ] L2Group Γ) =
       integratedRepresentation a := rfl
 
 theorem integratedToReduced_injective :
     Function.Injective (integratedToReduced (Γ := Γ)) := by
   intro a b h
   exact integratedRepresentation_injective (congrArg Subtype.val h)
 
 @[simp] theorem norm_integratedToReduced (a : GroupAlgebra Γ) :
     ‖integratedToReduced a‖ = reducedNorm a := rfl
 
 theorem denseRange_integratedToReduced :
     DenseRange (integratedToReduced (Γ := Γ)) := by
   intro T
   rw [closure_subtype, ← Set.range_comp]
   change (T : L2Group Γ →L[ℂ] L2Group Γ) ∈
     closure (Set.range (integratedRepresentation (Γ := Γ)))
   rw [← reducedAlgebra_coe_eq_closure_range]
   exact T.property
 
 theorem regularOperator_mem_reducedAlgebra (g : Γ) :
     regularOperator g ∈ reducedAlgebra Γ :=
   subset_closure ⟨GroupAlgebra.delta g, integratedRepresentation_delta g⟩
 
 theorem reducedAlgebra_coe_eq_closure_span :
     (reducedAlgebra Γ : Set (L2Group Γ →L[ℂ] L2Group Γ)) =
       closure (Submodule.span ℂ (Set.range (regularOperator (Γ := Γ))) :
         Set (L2Group Γ →L[ℂ] L2Group Γ)) := by
   rw [← integratedRepresentation_range]
   rfl
 
 /-- Minimality among closed complex star subalgebras containing all regular operators. -/
 theorem reducedAlgebra_minimal (S : StarSubalgebra ℂ (L2Group Γ →L[ℂ] L2Group Γ))
     (hS : IsClosed (S : Set (L2Group Γ →L[ℂ] L2Group Γ)))
     (h : ∀ g : Γ, regularOperator g ∈ S) : reducedAlgebra Γ ≤ S := by
   apply StarSubalgebra.topologicalClosure_minimal _ hS
   rintro T ⟨a, rfl⟩
   change integratedRepresentation a ∈ S
   induction a using MonoidAlgebra.induction_linear with
   | zero => simp
   | add a b ha hb =>
     rw [map_add]
     exact S.add_mem ha hb
   | single g z => simpa only [integratedRepresentation_single] using S.smul_mem (h g) z
 
 /-- Countability is needed here, but not for the C⋆-algebra construction. -/
 instance reducedGroupCStarSeparable [Countable Γ] : TopologicalSpace.SeparableSpace (ReducedGroupCStar Γ) := by
   apply TopologicalSpace.IsSeparable.separableSpace
   rw [reducedAlgebra_coe_eq_closure_span]
   exact ((Set.countable_range (regularOperator (Γ := Γ))).isSeparable.span (R := ℂ)).closure
 
 end BC4lean

ReducedGroupCStarTrivial.lean

源码 SHA-256：3f678a1bd54481bc533b3804cd45ddfc9bab48605ccc730ddf7368799a562df0

 import BC4lean.ReducedGroupCStar
 
 /-! # The reduced group C⋆-algebra of a trivial group -/
 
 noncomputable section
 
 namespace BC4lean
 
 variable {Γ : Type*} [Group Γ] [Subsingleton Γ]
 
 theorem reducedAlgebra_le_scalars :
     reducedAlgebra Γ ≤ (StarAlgHom.ofId ℂ (L2Group Γ →L[ℂ] L2Group Γ)).range := by
   apply reducedAlgebra_minimal
   · exact (algebraMap_isometry (𝕜 := ℂ) (𝕜' := L2Group Γ →L[ℂ] L2Group Γ)).isClosedEmbedding.isClosed_range
   · intro g
     refine ⟨1, ?_⟩
     rw [Subsingleton.elim g 1, regularOperator_one]
     exact map_one _
 
 theorem scalarToReduced_surjective :
     Function.Surjective (StarAlgHom.ofId ℂ (ReducedGroupCStar Γ)) := by
   intro T
   obtain ⟨z, hz⟩ := reducedAlgebra_le_scalars T.property
   refine ⟨z, Subtype.ext ?_⟩
   exact hz
 
 /-- Canonical scalar identification for any group with one element. -/
 def trivialReducedEquiv : ℂ ≃⋆ₐ[ℂ] ReducedGroupCStar Γ :=
   StarAlgEquiv.ofBijective (StarAlgHom.ofId ℂ (ReducedGroupCStar Γ))
     ⟨(algebraMap_isometry (𝕜 := ℂ) (𝕜' := ReducedGroupCStar Γ)).injective,
       scalarToReduced_surjective⟩
 
 @[simp] theorem trivialReducedEquiv_apply (z : ℂ) :
     trivialReducedEquiv (Γ := Γ) z = algebraMap ℂ (ReducedGroupCStar Γ) z := rfl
 
 theorem trivialReducedEquiv_isometry : Isometry (trivialReducedEquiv (Γ := Γ)) :=
   algebraMap_isometry ℂ (ReducedGroupCStar Γ)
 
 end BC4lean

ReducedNormGroupAlgebra.lean

源码 SHA-256：b65b835545d92cb8cf33e3eb4748008cb1a3bd6a9fc8465da8ac2b72a49a2446

 import BC4lean.ReducedGroupCStar
 
 /-! # The group algebra with its reduced norm
 
 A dedicated type synonym keeps this norm separate from possible ℓ¹ norms.
 The algebraic operations are precisely those of `GroupAlgebra Γ`.
 -/
 
 noncomputable section
 namespace BC4lean
 
 variable (Γ : Type*) [Group Γ]
 
 /-- The complex group algebra, reserved for the reduced-norm topology. -/
 def ReducedNormGroupAlgebra := GroupAlgebra Γ
 
 namespace ReducedNormGroupAlgebra
 
 instance instRing : Ring (ReducedNormGroupAlgebra Γ) :=
   inferInstanceAs (Ring (GroupAlgebra Γ))
 instance instAlgebra : Algebra ℂ (ReducedNormGroupAlgebra Γ) :=
   inferInstanceAs (Algebra ℂ (GroupAlgebra Γ))
 instance instStarRing : StarRing (ReducedNormGroupAlgebra Γ) :=
   inferInstanceAs (StarRing (GroupAlgebra Γ))
 instance instStarModule : StarModule ℂ (ReducedNormGroupAlgebra Γ) :=
   inferInstanceAs (StarModule ℂ (GroupAlgebra Γ))
 
 /-- Identity on coefficients; only the choice of topological structure changes. -/
 def ofGroupAlgebra : GroupAlgebra Γ ≃⋆ₐ[ℂ] ReducedNormGroupAlgebra Γ :=
   StarAlgEquiv.refl ℂ (GroupAlgebra Γ)
 
 def toReduced : ReducedNormGroupAlgebra Γ →⋆ₐ[ℂ] ReducedGroupCStar Γ :=
   integratedToReduced
 
 theorem toReduced_injective : Function.Injective (toReduced Γ) :=
   integratedToReduced_injective
 
 instance instNormedRing : NormedRing (ReducedNormGroupAlgebra Γ) :=
   NormedRing.induced _ _ (toReduced Γ) (toReduced_injective Γ)
 instance instNormedAlgebra : NormedAlgebra ℂ (ReducedNormGroupAlgebra Γ) :=
   NormedAlgebra.induced ℂ _ _ (toReduced Γ)
 
 @[simp] theorem norm_ofGroupAlgebra (a : GroupAlgebra Γ) :
     ‖ofGroupAlgebra Γ a‖ = reducedNorm a := rfl
 
 @[simp] theorem norm_toReduced (a : ReducedNormGroupAlgebra Γ) :
     ‖toReduced Γ a‖ = ‖a‖ := rfl
 
 instance instNormedStarGroup : NormedStarGroup (ReducedNormGroupAlgebra Γ) where
   norm_star_le a := by
     change ‖toReduced Γ (star a)‖ ≤ ‖toReduced Γ a‖
     rw [map_star]
     exact (norm_star (toReduced Γ a)).le
 
 instance instCStarRing : CStarRing (ReducedNormGroupAlgebra Γ) where
   norm_mul_self_le a := by
     change ‖toReduced Γ a‖ * ‖toReduced Γ a‖ ≤ ‖toReduced Γ (star a * a)‖
     rw [map_mul, map_star]
     exact CStarRing.norm_star_mul_self.symm.le
 
 theorem toReduced_isometry : Isometry (toReduced Γ) :=
   AddMonoidHomClass.isometry_of_norm (toReduced Γ) (norm_toReduced Γ)
 
 theorem toReduced_denseRange : DenseRange (toReduced Γ) :=
   denseRange_integratedToReduced
 
 end ReducedNormGroupAlgebra
 end BC4lean

ReducedCompletion.lean

源码 SHA-256：27bc0c056893f22d9ed1a17462215a71356768e9d5435025630aa3cb025b2754

 import BC4lean.ReducedNormGroupAlgebra
 import Mathlib.Analysis.Normed.Module.Completion
 
 /-! # The abstract reduced-norm completion and its concrete realization
 
 The source is Mathlib's uniform completion of the reduced-norm group algebra.
 Its ring, complex module and algebra operations are the standard completion
 operations. Its star is `Completion.map star`, not a transported operation.
 -/
 
 noncomputable section
 namespace BC4lean
 open UniformSpace
 
 variable (Γ : Type*) [Group Γ]
 
 /-- Abstract norm completion of the complex group algebra with reduced norm. -/
 abbrev ReducedCompletion := Completion (ReducedNormGroupAlgebra Γ)
 
 /-- Continuous extension of the canonical ring homomorphism. -/
 def completionMap : ReducedCompletion Γ →+* ReducedGroupCStar Γ :=
   Completion.extensionHom (ReducedNormGroupAlgebra.toReduced Γ).toAlgHom.toRingHom
     (ReducedNormGroupAlgebra.toReduced_isometry Γ).continuous
 
 @[simp] theorem completionMap_coe (a : ReducedNormGroupAlgebra Γ) :
     completionMap Γ (a : ReducedCompletion Γ) = ReducedNormGroupAlgebra.toReduced Γ a :=
   Completion.extensionHom_coe _ _ a
 
 theorem completionMap_isometry : Isometry (completionMap Γ) :=
   (ReducedNormGroupAlgebra.toReduced_isometry Γ).completion_extension
 
 theorem completionMap_injective : Function.Injective (completionMap Γ) :=
   (completionMap_isometry Γ).injective
 
 @[simp] theorem norm_completionMap (x : ReducedCompletion Γ) :
     ‖completionMap Γ x‖ = ‖x‖ := by
   simpa only [map_zero, dist_zero_right] using (completionMap_isometry Γ).dist_eq x 0
 
 theorem completionMap_surjective : Function.Surjective (completionMap Γ) := by
   intro T
   have hsubset : Set.range (ReducedNormGroupAlgebra.toReduced Γ) ⊆
       Set.range (completionMap Γ) := by
     rintro _ ⟨a, rfl⟩
     exact ⟨(a : ReducedCompletion Γ), completionMap_coe Γ a⟩
   have h := closure_mono hsubset (ReducedNormGroupAlgebra.toReduced_denseRange Γ T)
   rwa [(completionMap_isometry Γ).isClosedEmbedding.isClosed_range.closure_eq] at h
 
 /-- Complex-linearity of the canonical extension. -/
 def completionAlgHom : ReducedCompletion Γ →ₐ[ℂ] ReducedGroupCStar Γ where
   toRingHom := completionMap Γ
   commutes' z := by
     change completionMap Γ ((algebraMap ℂ (ReducedNormGroupAlgebra Γ) z :
       ReducedNormGroupAlgebra Γ) : ReducedCompletion Γ) = _
     rw [completionMap_coe]
     exact (ReducedNormGroupAlgebra.toReduced Γ).commutes z
 
 instance completionStar : Star (ReducedCompletion Γ) :=
   ⟨Completion.map (star : ReducedNormGroupAlgebra Γ → ReducedNormGroupAlgebra Γ)⟩
 
 @[simp] theorem completion_star_coe (a : ReducedNormGroupAlgebra Γ) :
     star (a : ReducedCompletion Γ) = (star a : ReducedNormGroupAlgebra Γ) :=
   Completion.map_coe star_isometry.uniformContinuous a
 
 instance completionContinuousStar : ContinuousStar (ReducedCompletion Γ) :=
   ⟨Completion.continuous_map⟩
 
 theorem completionMap_star (x : ReducedCompletion Γ) :
     completionMap Γ (star x) = star (completionMap Γ x) := by
   induction x using Completion.induction_on with
   | hp =>
     exact isClosed_eq ((completionMap_isometry Γ).continuous.comp continuous_star)
       (continuous_star.comp (completionMap_isometry Γ).continuous)
   | ih a => simp only [completion_star_coe, completionMap_coe, map_star]
 
 instance completionStarRing : StarRing (ReducedCompletion Γ) :=
   (completionMap_injective Γ).starRing (completionMap Γ)
     (completionMap_star Γ) (map_add _) (map_mul _)
 
 instance completionStarModule : StarModule ℂ (ReducedCompletion Γ) :=
   Function.Injective.starModule (completionMap Γ) ℂ (completionMap_injective Γ)
     (completionMap_star Γ) (map_smul (completionAlgHom Γ))
 
 instance completionNormedAlgebra : NormedAlgebra ℂ (ReducedCompletion Γ) where
   norm_smul_le := norm_smul_le
 
 instance completionCStarRing : CStarRing (ReducedCompletion Γ) where
   norm_mul_self_le x := by
     rw [← norm_completionMap Γ x, ← norm_completionMap Γ (star x * x),
       map_mul, completionMap_star]
     exact CStarRing.norm_star_mul_self.symm.le
 
 instance completionCStarAlgebra : CStarAlgebra (ReducedCompletion Γ) where
 
 /-- The extended map as a unital complex star-algebra homomorphism. -/
 def completionStarHom : ReducedCompletion Γ →⋆ₐ[ℂ] ReducedGroupCStar Γ where
   toAlgHom := completionAlgHom Γ
   map_star' := completionMap_star Γ
 
 /-- The abstract norm completion is canonically the concrete reduced group C⋆-algebra. -/
 def reducedCompletionEquiv : ReducedCompletion Γ ≃⋆ₐ[ℂ] ReducedGroupCStar Γ :=
   StarAlgEquiv.ofBijective (completionStarHom Γ)
     ⟨completionMap_injective Γ, completionMap_surjective Γ⟩
 
 theorem reducedCompletionEquiv_isometry : Isometry (reducedCompletionEquiv Γ) :=
   completionMap_isometry Γ
 
 @[simp] theorem reducedCompletionEquiv_coe (a : ReducedNormGroupAlgebra Γ) :
     reducedCompletionEquiv Γ (a : ReducedCompletion Γ) =
       ReducedNormGroupAlgebra.toReduced Γ a := completionMap_coe Γ a
 
 /-- The original algebra embeds in the abstract completion. -/
 def groupAlgebraToCompletion : GroupAlgebra Γ →⋆ₐ[ℂ] ReducedCompletion Γ where
   toAlgHom :=
     { toRingHom := Completion.coeRingHom.comp
         (ReducedNormGroupAlgebra.ofGroupAlgebra Γ).toAlgEquiv.toAlgHom.toRingHom
       commutes' _ := rfl }
   map_star' a := (completion_star_coe Γ (ReducedNormGroupAlgebra.ofGroupAlgebra Γ a)).symm
 
 @[simp] theorem norm_groupAlgebraToCompletion (a : GroupAlgebra Γ) :
     ‖groupAlgebraToCompletion Γ a‖ = reducedNorm a :=
   Completion.norm_coe (ReducedNormGroupAlgebra.ofGroupAlgebra Γ a)
 
 @[simp] theorem reducedCompletionEquiv_extends (a : GroupAlgebra Γ) :
     reducedCompletionEquiv Γ (groupAlgebraToCompletion Γ a) = integratedToReduced a :=
   completionMap_coe Γ (ReducedNormGroupAlgebra.ofGroupAlgebra Γ a)
 
 /-- Uniqueness already holds among all continuous functions with the prescribed restriction. -/
 theorem reducedCompletionEquiv_unique (f : ReducedCompletion Γ → ReducedGroupCStar Γ)
     (hf : Continuous f)
     (h : ∀ a : GroupAlgebra Γ, f (groupAlgebraToCompletion Γ a) = integratedToReduced a) :
     f = reducedCompletionEquiv Γ := by
   apply Completion.ext hf (reducedCompletionEquiv_isometry Γ).continuous
   intro a
   obtain ⟨b, rfl⟩ := (ReducedNormGroupAlgebra.ofGroupAlgebra Γ).surjective a
   exact (h b).trans (reducedCompletionEquiv_extends Γ b).symm
 
 /-- In particular the extension is the unique isometric star-algebra isomorphism. -/
 theorem reducedCompletionEquiv_unique_isometric
     (e : ReducedCompletion Γ ≃⋆ₐ[ℂ] ReducedGroupCStar Γ) (he : Isometry e)
     (h : ∀ a : GroupAlgebra Γ, e (groupAlgebraToCompletion Γ a) = integratedToReduced a) :
     e = reducedCompletionEquiv Γ := by
   apply DFunLike.coe_injective
   exact reducedCompletionEquiv_unique Γ e he.continuous h
 
 end BC4lean

OperatorProjections.lean

源码 SHA-256：ebd907953cb61d6852bdec4eab229baa97b554af4c4010f998f3febb913ce0c3

 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Algebra.Star.StarProjection
 
 /-! # Projections and Murray–von Neumann equivalence
 
 Projection-level foundations for operator K₀. The two support equations for
 partial isometries are consequences of the C⋆-identity, not extra assumptions.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 
 variable {A B C : Type*} [CStarAlgebra A] [CStarAlgebra B] [CStarAlgebra C]
 
 /-- A projection in a unital complex C⋆-algebra. -/
 abbrev Projection (A : Type*) [CStarAlgebra A] := {p : A // IsStarProjection p}
 
 namespace Projection
 
 @[simp] theorem star_coe (p : Projection A) : star (p : A) = p :=
   p.property.isSelfAdjoint.star_eq
 
 @[simp] theorem mul_self (p : Projection A) : (p : A) * p = p :=
   p.property.isIdempotentElem.eq
 
 def zero : Projection A := ⟨0, IsStarProjection.zero A⟩
 def one : Projection A := ⟨1, IsStarProjection.one A⟩
 def complement (p : Projection A) : Projection A := ⟨1 - p, p.property.one_sub⟩
 
 def map (φ : A →⋆ₐ[ℂ] B) (p : Projection A) : Projection B :=
   ⟨φ p, p.property.map φ⟩
 
 @[simp] theorem map_coe (φ : A →⋆ₐ[ℂ] B) (p : Projection A) :
     (map φ p : B) = φ p := rfl
 
 @[simp] theorem map_id (p : Projection A) : map (StarAlgHom.id ℂ A) p = p := rfl
 
 @[simp] theorem map_comp (ψ : B →⋆ₐ[ℂ] C) (φ : A →⋆ₐ[ℂ] B) (p : Projection A) :
     map (ψ.comp φ) p = map ψ (map φ p) := rfl
 
 @[simp] theorem map_zero (φ : A →⋆ₐ[ℂ] B) : map φ zero = zero :=
   Subtype.ext (_root_.map_zero φ)
 
 @[simp] theorem map_one (φ : A →⋆ₐ[ℂ] B) : map φ one = one :=
   Subtype.ext (_root_.map_one φ)
 
 /-- The initial projection acts as the right support of a partial isometry. -/
 theorem right_support (p : Projection A) (v : A) (hv : star v * v = p) : v * p = v := by
   apply sub_eq_zero.mp
   apply (CStarRing.star_mul_self_eq_zero_iff (v * p - v)).mp
   have h₁ : star v * (v * p) = p := by rw [← mul_assoc, hv, mul_self]
   simp only [star_sub, star_mul, star_coe, sub_mul, mul_sub, mul_assoc, h₁, hv,
     mul_self, sub_self]
 
 /-- Equivalence implemented by the usual two partial-isometry equations. -/
 def Equivalent (p q : Projection A) : Prop :=
   ∃ v : A, star v * v = p ∧ v * star v = q
 
 theorem equivalent_refl (p : Projection A) : Equivalent p p :=
   ⟨p, by simp, by simp⟩
 
 theorem equivalent_symm {p q : Projection A} (h : Equivalent p q) : Equivalent q p := by
   obtain ⟨v, hv, hv'⟩ := h
   exact ⟨star v, by simpa using hv', by simpa using hv⟩
 
 theorem equivalent_trans {p q r : Projection A}
     (hpq : Equivalent p q) (hqr : Equivalent q r) : Equivalent p r := by
   obtain ⟨v, hv, hv'⟩ := hpq
   obtain ⟨w, hw, hw'⟩ := hqr
   have hvp := right_support p v hv
   have hqv : (q : A) * v = v := by rw [← hv', mul_assoc, hv, hvp]
   have hwq := right_support q w hw
   refine ⟨w * v, ?_, ?_⟩
   · calc
       star (w * v) * (w * v) = star v * (star w * w) * v := by simp only [star_mul, mul_assoc]
       _ = star v * q * v := by rw [hw]
       _ = p := by rw [mul_assoc, hqv, hv]
   · calc
       (w * v) * star (w * v) = w * (v * star v) * star w := by simp only [star_mul, mul_assoc]
       _ = w * q * star w := by rw [hv']
       _ = r := by rw [hwq, hw']
 
 /-- Equivalence classes at a fixed algebra, in particular a fixed matrix size. -/
 def equivalenceSetoid : Setoid (Projection A) where
   r := Equivalent
   iseqv := ⟨equivalent_refl, equivalent_symm, equivalent_trans⟩
 
 abbrev Classes (A : Type*) [CStarAlgebra A] := Quotient (equivalenceSetoid (A := A))
 
 theorem equivalent_map (φ : A →⋆ₐ[ℂ] B) {p q : Projection A}
     (h : Equivalent p q) : Equivalent (map φ p) (map φ q) := by
   obtain ⟨v, hv, hv'⟩ := h
   refine ⟨φ v, ?_, ?_⟩
   · simpa only [map_mul, map_star, map_coe] using congrArg φ hv
   · simpa only [map_mul, map_star, map_coe] using congrArg φ hv'
 
 def mapClasses (φ : A →⋆ₐ[ℂ] B) : Classes A → Classes B :=
   Quotient.map (map φ) (fun _ _ h => equivalent_map φ h)
 
 @[simp] theorem mapClasses_mk (φ : A →⋆ₐ[ℂ] B) (p : Projection A) :
     mapClasses φ (Quotient.mk _ p) = Quotient.mk _ (map φ p) := rfl
 
 end Projection
 end BC4lean.OperatorKTheory

MatrixStabilization.lean

源码 SHA-256：ed088f2a4c275e44cb052d1304c855e6e966b5ecdbad4881ddbdd38bfd4c59e1

 import BC4lean.OperatorProjections
 import Mathlib.Analysis.CStarAlgebra.CStarMatrix
 import Mathlib.Data.Matrix.Block
 import Mathlib.Algebra.Star.Unitary
 
 /-! # Matrix projections, unitaries, and stabilization
 
 We use Mathlib's C⋆-matrix norm, not the entrywise supremum norm. The order
 assumptions are the standard compatible C⋆-order required by that API.
 Block sums first use sum-indexed matrices, avoiding arbitrary index choices.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 
 open scoped Matrix
 
 variable {A : Type*} [CStarAlgebra A]
 variable {ι κ : Type*}
 
 /-- Block diagonal sum of C⋆-matrices. -/
 def matrixBlockSum (p : CStarMatrix ι ι A) (q : CStarMatrix κ κ A) :
     CStarMatrix (ι ⊕ κ) (ι ⊕ κ) A :=
   CStarMatrix.ofMatrix (Matrix.fromBlocks (CStarMatrix.ofMatrix.symm p) 0 0
     (CStarMatrix.ofMatrix.symm q))
 
 @[simp] theorem matrixBlockSum_star (p : CStarMatrix ι ι A) (q : CStarMatrix κ κ A) :
     star (matrixBlockSum p q) = matrixBlockSum (star p) (star q) := by
   change (Matrix.fromBlocks (CStarMatrix.ofMatrix.symm p) (0 : Matrix ι κ A)
     (0 : Matrix κ ι A) (CStarMatrix.ofMatrix.symm q))ᴴ = _
   simp only [Matrix.fromBlocks_conjTranspose, Matrix.conjTranspose_zero]
   rfl
 
 theorem matrixBlockSum_mul [Fintype ι] [Fintype κ] (p r : CStarMatrix ι ι A) (q s : CStarMatrix κ κ A) :
     matrixBlockSum p q * matrixBlockSum r s = matrixBlockSum (p * r) (q * s) := by
   change Matrix.fromBlocks (CStarMatrix.ofMatrix.symm p) (0 : Matrix ι κ A)
     (0 : Matrix κ ι A) (CStarMatrix.ofMatrix.symm q) *
     Matrix.fromBlocks (CStarMatrix.ofMatrix.symm r) (0 : Matrix ι κ A)
     (0 : Matrix κ ι A) (CStarMatrix.ofMatrix.symm s) =
     Matrix.fromBlocks (CStarMatrix.ofMatrix.symm p * CStarMatrix.ofMatrix.symm r)
       (0 : Matrix ι κ A) (0 : Matrix κ ι A)
       (CStarMatrix.ofMatrix.symm q * CStarMatrix.ofMatrix.symm s)
   simp only [Matrix.fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add]
 
 @[simp] theorem matrixBlockSum_one [DecidableEq ι] [DecidableEq κ] :
     matrixBlockSum (1 : CStarMatrix ι ι A) (1 : CStarMatrix κ κ A) = 1 :=
   Matrix.fromBlocks_one
 
 @[simp] theorem matrixBlockSum_zero :
     matrixBlockSum (0 : CStarMatrix ι ι A) (0 : CStarMatrix κ κ A) = 0 :=
   Matrix.fromBlocks_zero
 
 variable [PartialOrder A] [StarOrderedRing A]
 variable [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
 
 /-- A matrix projection with the C⋆-matrix norm. -/
 abbrev MatrixProjection (A : Type*) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
     (ι : Type*) [Fintype ι] [DecidableEq ι] := Projection (CStarMatrix ι ι A)
 
 def projectionBlockSum (p : MatrixProjection A ι) (q : MatrixProjection A κ) :
     MatrixProjection A (ι ⊕ κ) :=
   ⟨matrixBlockSum p q, ⟨by
     change matrixBlockSum p.val q.val * matrixBlockSum p.val q.val = matrixBlockSum p.val q.val
     rw [matrixBlockSum_mul]; simp, by
     change star (matrixBlockSum p.val q.val) = matrixBlockSum p.val q.val
     rw [matrixBlockSum_star]; simp⟩⟩
 
 @[simp] theorem projectionBlockSum_coe (p : MatrixProjection A ι) (q : MatrixProjection A κ) :
     (projectionBlockSum p q : CStarMatrix (ι ⊕ κ) (ι ⊕ κ) A) = matrixBlockSum p q := rfl
 
 /-- Projection stabilization adds a zero block. -/
 def stabilizeProjection (p : MatrixProjection A ι) : MatrixProjection A (ι ⊕ κ) :=
   projectionBlockSum p Projection.zero
 
 theorem equivalent_blockSum {p r : MatrixProjection A ι} {q s : MatrixProjection A κ}
     (h : Projection.Equivalent p r) (k : Projection.Equivalent q s) :
     Projection.Equivalent (projectionBlockSum p q) (projectionBlockSum r s) := by
   obtain ⟨v, hv, hv'⟩ := h
   obtain ⟨w, hw, hw'⟩ := k
   refine ⟨matrixBlockSum v w, ?_, ?_⟩
   · simp only [matrixBlockSum_star, matrixBlockSum_mul, hv, hw, projectionBlockSum_coe]
   · simp only [matrixBlockSum_star, matrixBlockSum_mul, hv', hw', projectionBlockSum_coe]
 
 theorem equivalent_stabilize {p q : MatrixProjection A ι} (h : Projection.Equivalent p q) :
     Projection.Equivalent (stabilizeProjection (κ := κ) p) (stabilizeProjection q) :=
   equivalent_blockSum h (Projection.equivalent_refl Projection.zero)
 
 /-- Block sum descends to Murray–von Neumann classes at the indicated matrix sizes. -/
 def blockSumClasses : Projection.Classes (CStarMatrix ι ι A) →
     Projection.Classes (CStarMatrix κ κ A) →
     Projection.Classes (CStarMatrix (ι ⊕ κ) (ι ⊕ κ) A) :=
   Quotient.map₂ projectionBlockSum (fun _ _ h _ _ k => equivalent_blockSum h k)
 
 /-- A matrix unitary with the operator-norm topology. -/
 abbrev MatrixUnitary (A : Type*) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
     (ι : Type*) [Fintype ι] [DecidableEq ι] := unitary (CStarMatrix ι ι A)
 
 def unitaryBlockSum (u : MatrixUnitary A ι) (v : MatrixUnitary A κ) :
     MatrixUnitary A (ι ⊕ κ) :=
   ⟨matrixBlockSum u v, by
     rw [Unitary.mem_iff]
     constructor
     · rw [matrixBlockSum_star, matrixBlockSum_mul,
         Unitary.star_mul_self_of_mem u.property, Unitary.star_mul_self_of_mem v.property,
         matrixBlockSum_one]
     · rw [matrixBlockSum_star, matrixBlockSum_mul,
         Unitary.mul_star_self_of_mem u.property, Unitary.mul_star_self_of_mem v.property,
         matrixBlockSum_one]⟩
 
 @[simp] theorem unitaryBlockSum_coe (u : MatrixUnitary A ι) (v : MatrixUnitary A κ) :
     (unitaryBlockSum u v : CStarMatrix (ι ⊕ κ) (ι ⊕ κ) A) = matrixBlockSum u v := rfl
 
 /-- Unitary stabilization adds an identity block, unlike projection stabilization. -/
 def stabilizeUnitary (u : MatrixUnitary A ι) : MatrixUnitary A (ι ⊕ κ) :=
   unitaryBlockSum u 1
 
 end BC4lean.OperatorKTheory

UnitaryHomotopy.lean

源码 SHA-256：bf4d4b1221bbfc6f46f53faf1e26975d55901455326576a207c7b5ee1ce7e23e

 import BC4lean.MatrixStabilization
 import Mathlib.Topology.Algebra.Star.Unitary
 import Mathlib.Topology.Connected.PathConnected
 
 /-! # Norm homotopy of matrix unitaries
 
 These are path components at a fixed matrix size, not yet the stable group K₁.
 The topology is the subspace topology of Mathlib's operator-norm C⋆-matrices.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 
 variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
 variable {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
 
 /-- A norm-continuous path of matrix unitaries joins the two endpoints. -/
 def UnitaryHomotopic (u v : MatrixUnitary A ι) : Prop := Joined u v
 
 theorem unitaryHomotopic_refl (u : MatrixUnitary A ι) : UnitaryHomotopic u u :=
   Joined.refl u
 
 theorem unitaryHomotopic_symm {u v : MatrixUnitary A ι} (h : UnitaryHomotopic u v) :
     UnitaryHomotopic v u := Joined.symm h
 
 theorem unitaryHomotopic_trans {u v w : MatrixUnitary A ι}
     (h : UnitaryHomotopic u v) (k : UnitaryHomotopic v w) : UnitaryHomotopic u w :=
   Joined.trans h k
 
 theorem unitaryHomotopic_mul {u v w z : MatrixUnitary A ι}
     (h : UnitaryHomotopic u v) (k : UnitaryHomotopic w z) :
     UnitaryHomotopic (u * w) (v * z) := Joined.mul h k
 
 theorem unitaryHomotopic_inv {u v : MatrixUnitary A ι} (h : UnitaryHomotopic u v) :
     UnitaryHomotopic u⁻¹ v⁻¹ := Joined.inv h
 
 /-- Fixed-size norm-path components of the unitary group. -/
 abbrev UnitaryHomotopyClasses (A : Type*) [CStarAlgebra A]
     [PartialOrder A] [StarOrderedRing A] (ι : Type*) [Fintype ι] [DecidableEq ι] :=
   Quotient (pathSetoid (MatrixUnitary A ι))
 
 omit [PartialOrder A] [StarOrderedRing A] [Fintype ι] [Fintype κ]
     [DecidableEq ι] [DecidableEq κ] in
 theorem continuous_matrixBlockSum :
     Continuous (fun x : CStarMatrix ι ι A × CStarMatrix κ κ A =>
       matrixBlockSum x.1 x.2) := by
   exact CStarMatrix.ofMatrixL.continuous.comp
     ((CStarMatrix.ofMatrixL.symm.continuous.comp continuous_fst).matrix_fromBlocks
       continuous_const continuous_const
       (CStarMatrix.ofMatrixL.symm.continuous.comp continuous_snd))
 
 theorem continuous_unitaryBlockSum :
     Continuous (fun x : MatrixUnitary A ι × MatrixUnitary A κ =>
       unitaryBlockSum x.1 x.2) := by
   apply Continuous.subtype_mk
   exact continuous_matrixBlockSum.comp
     ((continuous_subtype_val.comp continuous_fst).prodMk
       (continuous_subtype_val.comp continuous_snd))
 
 theorem unitaryHomotopic_blockSum {u v : MatrixUnitary A ι} {w z : MatrixUnitary A κ}
     (h : UnitaryHomotopic u v) (k : UnitaryHomotopic w z) :
     UnitaryHomotopic (unitaryBlockSum u w) (unitaryBlockSum v z) := by
   exact (Joined.prod h k).map
     continuous_unitaryBlockSum
 
 theorem unitaryHomotopic_stabilize {u v : MatrixUnitary A ι}
     (h : UnitaryHomotopic u v) :
     UnitaryHomotopic (stabilizeUnitary (κ := κ) u) (stabilizeUnitary v) :=
   unitaryHomotopic_blockSum h (unitaryHomotopic_refl 1)
 
 /-- Stabilization is well-defined on norm-path components at each size. -/
 def stabilizeUnitaryClasses : UnitaryHomotopyClasses A ι →
     UnitaryHomotopyClasses A (ι ⊕ κ) :=
   Quotient.map stabilizeUnitary (fun _ _ h => unitaryHomotopic_stabilize h)
 
 end BC4lean.OperatorKTheory

RectangularEquivalence.lean

源码 SHA-256：64e81b38d480648be4ef60b8def7cb16a622f16290f763a4f91d959c4c1112dd

 import BC4lean.MatrixStabilization
 
 /-! # Murray–von Neumann equivalence across finite matrix sizes
 
 Rectangular witnesses compare projections without choosing an ordering of the
 finite index sets. Their support identities follow from the C⋆-identity.
 -/
 
 noncomputable section
 open scoped Matrix
 namespace BC4lean.OperatorKTheory
 
 variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
 variable {ι κ τ υ : Type*} [Fintype ι] [Fintype κ] [Fintype τ] [Fintype υ]
 variable [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] [DecidableEq υ]
 
 abbrev projectionMatrix (p : MatrixProjection A ι) : Matrix ι ι A :=
   CStarMatrix.ofMatrix.symm p.val
 
 @[simp] theorem projectionMatrix_star (p : MatrixProjection A ι) :
     (projectionMatrix p)ᴴ = projectionMatrix p := p.property.isSelfAdjoint.star_eq
 
 @[simp] theorem projectionMatrix_mul (p : MatrixProjection A ι) :
     projectionMatrix p * projectionMatrix p = projectionMatrix p := p.property.isIdempotentElem.eq
 
 /-- Initial and final projections of a rectangular partial isometry. -/
 def RectEquivalent (p : MatrixProjection A ι) (q : MatrixProjection A κ) : Prop :=
   ∃ v : Matrix ι κ A, v * vᴴ = projectionMatrix p ∧ vᴴ * v = projectionMatrix q
 
 /-- The right support equation is derived, rather than included in the definition. -/
 theorem rectangular_right_support (q : MatrixProjection A κ) (v : Matrix ι κ A)
     (hv : vᴴ * v = projectionMatrix q) : v * projectionMatrix q = v := by
   let V : CStarMatrix (ι ⊕ κ) (ι ⊕ κ) A :=
     CStarMatrix.ofMatrix (Matrix.fromBlocks (0 : Matrix ι ι A) v 0 0)
   let P : MatrixProjection A (ι ⊕ κ) := projectionBlockSum Projection.zero q
   have hMat :
       (Matrix.fromBlocks (0 : Matrix ι ι A) v (0 : Matrix κ ι A) (0 : Matrix κ κ A))ᴴ *
         Matrix.fromBlocks (0 : Matrix ι ι A) v (0 : Matrix κ ι A) (0 : Matrix κ κ A) =
         Matrix.fromBlocks (0 : Matrix ι ι A) (0 : Matrix ι κ A)
           (0 : Matrix κ ι A) (projectionMatrix q) := by
     simp only [Matrix.fromBlocks_conjTranspose, Matrix.conjTranspose_zero,
       Matrix.fromBlocks_multiply, Matrix.zero_mul, Matrix.mul_zero, add_zero, hv]
   have hV : star V * V = P.val := hMat
   have h := Projection.right_support P V hV
   have hMat' :
       Matrix.fromBlocks (0 : Matrix ι ι A) v (0 : Matrix κ ι A) (0 : Matrix κ κ A) *
         Matrix.fromBlocks (0 : Matrix ι ι A) (0 : Matrix ι κ A)
           (0 : Matrix κ ι A) (projectionMatrix q) =
       Matrix.fromBlocks (0 : Matrix ι ι A) v (0 : Matrix κ ι A) (0 : Matrix κ κ A) := h
   simp only [Matrix.fromBlocks_multiply, Matrix.zero_mul, Matrix.mul_zero,
     zero_add, add_zero] at hMat'
   exact congrArg Matrix.toBlocks₁₂ hMat'
 
 theorem rectangular_left_support (p : MatrixProjection A ι) (v : Matrix ι κ A)
     (hv : v * vᴴ = projectionMatrix p) : projectionMatrix p * v = v := by
   have h := rectangular_right_support p vᴴ (by simpa using hv)
   simpa using congrArg Matrix.conjTranspose h
 
 theorem rectEquivalent_refl (p : MatrixProjection A ι) : RectEquivalent p p :=
   ⟨projectionMatrix p, by simp, by simp⟩
 
 theorem rectEquivalent_symm {p : MatrixProjection A ι} {q : MatrixProjection A κ}
     (h : RectEquivalent p q) : RectEquivalent q p := by
   obtain ⟨v, hv, hv'⟩ := h
   exact ⟨vᴴ, by simpa using hv', by simpa using hv⟩
 
 theorem rectEquivalent_trans {p : MatrixProjection A ι} {q : MatrixProjection A κ}
     {r : MatrixProjection A τ} (h : RectEquivalent p q) (k : RectEquivalent q r) :
     RectEquivalent p r := by
   obtain ⟨v, hv, hv'⟩ := h
   obtain ⟨w, hw, hw'⟩ := k
   refine ⟨v * w, ?_, ?_⟩
   · calc
       (v * w) * (v * w)ᴴ = (v * (w * wᴴ)) * vᴴ := by
         simp only [Matrix.conjTranspose_mul, Matrix.mul_assoc]
       _ = (v * projectionMatrix q) * vᴴ := by rw [hw]
       _ = projectionMatrix p := by rw [rectangular_right_support q v hv', hv]
   · calc
       (v * w)ᴴ * (v * w) = wᴴ * ((vᴴ * v) * w) := by
         simp only [Matrix.conjTranspose_mul, Matrix.mul_assoc]
       _ = wᴴ * (projectionMatrix q * w) := by rw [hv']
       _ = projectionMatrix r := by rw [rectangular_left_support q w hw, hw']
 
 /-- Rectangular equivalence agrees with the earlier relation at equal index types. -/
 theorem rectEquivalent_iff_equivalent (p q : MatrixProjection A ι) :
     RectEquivalent p q ↔ Projection.Equivalent p q := by
   constructor
   · rintro ⟨v, hv, hv'⟩
     refine ⟨CStarMatrix.ofMatrix vᴴ, ?_, ?_⟩
     · change vᴴᴴ * vᴴ = projectionMatrix p
       simpa only [Matrix.conjTranspose_conjTranspose] using hv
     · change vᴴ * vᴴᴴ = projectionMatrix q
       simpa only [Matrix.conjTranspose_conjTranspose] using hv' 
   · rintro ⟨v, hv, hv'⟩
     change (CStarMatrix.ofMatrix.symm v)ᴴ * CStarMatrix.ofMatrix.symm v = projectionMatrix p at hv
     change CStarMatrix.ofMatrix.symm v * (CStarMatrix.ofMatrix.symm v)ᴴ = projectionMatrix q at hv'
     exact ⟨(CStarMatrix.ofMatrix.symm v)ᴴ, by simpa using hv, by simpa using hv'⟩
 
 theorem rectEquivalent_blockSum {p : MatrixProjection A ι} {q : MatrixProjection A κ}
     {r : MatrixProjection A τ} {s : MatrixProjection A υ}
     (h : RectEquivalent p q) (k : RectEquivalent r s) :
     RectEquivalent (projectionBlockSum p r) (projectionBlockSum q s) := by
   obtain ⟨v, hv, hv'⟩ := h
   obtain ⟨w, hw, hw'⟩ := k
   refine ⟨Matrix.fromBlocks v 0 0 w, ?_, ?_⟩
   · change Matrix.fromBlocks v (0 : Matrix ι υ A) (0 : Matrix τ κ A) w *
       (Matrix.fromBlocks v 0 0 w)ᴴ =
       Matrix.fromBlocks (projectionMatrix p) 0 0 (projectionMatrix r)
     simp only [Matrix.fromBlocks_conjTranspose, Matrix.conjTranspose_zero,
       Matrix.fromBlocks_multiply, Matrix.zero_mul, Matrix.mul_zero, zero_add, add_zero, hv, hw]
   · change (Matrix.fromBlocks v (0 : Matrix ι υ A) (0 : Matrix τ κ A) w)ᴴ *
       Matrix.fromBlocks v 0 0 w =
       Matrix.fromBlocks (projectionMatrix q) 0 0 (projectionMatrix s)
     simp only [Matrix.fromBlocks_conjTranspose, Matrix.conjTranspose_zero,
       Matrix.fromBlocks_multiply, Matrix.zero_mul, Matrix.mul_zero, zero_add, add_zero, hv', hw']
 
 /-- A change of finite matrix indices does not change the equivalence class. -/
 theorem rectEquivalent_of_reindex (p : MatrixProjection A ι) (q : MatrixProjection A κ)
     (e : κ ≃ ι) (hq : projectionMatrix q = (projectionMatrix p).submatrix e e) :
     RectEquivalent p q := by
   refine ⟨(projectionMatrix p).submatrix id e, ?_, ?_⟩
   · simp only [Matrix.conjTranspose_submatrix, projectionMatrix_star,
       Matrix.submatrix_mul_equiv, projectionMatrix_mul, Matrix.submatrix_id_id]
   · rw [Matrix.conjTranspose_submatrix, projectionMatrix_star]
     change (projectionMatrix p).submatrix e (Equiv.refl ι) *
       (projectionMatrix p).submatrix (Equiv.refl ι) e = projectionMatrix q
     rw [Matrix.submatrix_mul_equiv, projectionMatrix_mul, ← hq]
 
 theorem rectEquivalent_zero : RectEquivalent (Projection.zero : MatrixProjection A ι)
     (Projection.zero : MatrixProjection A κ) := by
   refine ⟨0, ?_, ?_⟩ <;> simp only [Matrix.conjTranspose_zero, Matrix.zero_mul] <;> rfl
 
 theorem rectEquivalent_block_comm (p : MatrixProjection A ι) (q : MatrixProjection A κ) :
     RectEquivalent (projectionBlockSum p q) (projectionBlockSum q p) := by
   apply rectEquivalent_of_reindex _ _ (Equiv.sumComm κ ι)
   ext i j
   cases i <;> cases j <;> rfl
 
 /-- Adding a zero block does not change the rectangular equivalence class. -/
 theorem rectEquivalent_stabilize (p : MatrixProjection A ι) :
     RectEquivalent p (stabilizeProjection (κ := κ) p) := by
   have h : RectEquivalent (projectionBlockSum p (Projection.zero : MatrixProjection A κ))
       (projectionBlockSum p (Projection.zero : MatrixProjection A Empty)) :=
     rectEquivalent_blockSum (rectEquivalent_refl p) rectEquivalent_zero
   have k : RectEquivalent p (projectionBlockSum p (Projection.zero : MatrixProjection A Empty)) := by
     apply rectEquivalent_of_reindex _ _ (Equiv.sumEmpty ι Empty)
     ext i j
     rcases i with i | i
     · rcases j with j | j
       · rfl
       · exact j.elim
     · exact i.elim
   exact rectEquivalent_trans k (rectEquivalent_symm h)
 
 /-- Rectangular witnesses are equivalent to ordinary equivalence in a common
 matrix algebra after the two projections are placed in disjoint corners. -/
 theorem rectEquivalent_iff_padded (p : MatrixProjection A ι) (q : MatrixProjection A κ) :
     RectEquivalent p q ↔ Projection.Equivalent
       (projectionBlockSum p (Projection.zero : MatrixProjection A κ))
       (projectionBlockSum (Projection.zero : MatrixProjection A ι) q) := by
   have hp := rectEquivalent_stabilize (κ := κ) p
   have hq := rectEquivalent_trans (rectEquivalent_stabilize (κ := ι) q)
     (rectEquivalent_block_comm q (Projection.zero : MatrixProjection A ι))
   rw [← rectEquivalent_iff_equivalent]
   constructor
   · intro h
     exact rectEquivalent_trans (rectEquivalent_trans (rectEquivalent_symm hp) h) hq
   · intro h
     exact rectEquivalent_trans (rectEquivalent_trans hp h) (rectEquivalent_symm hq)
 
 end BC4lean.OperatorKTheory

StableProjectionMonoid.lean

源码 SHA-256：e61cd47688e2e352293eb0a933f93b06d5fdd59275359faf87e6858386e8c6a6

 import BC4lean.RectangularEquivalence
 
 /-! # The stable projection monoid
 
 Objects are projections indexed by arbitrary small finite types. Rectangular
 Murray–von Neumann witnesses make the quotient independent of the index type.
 Addition is actual matrix block sum, not a freely imposed relation.
 -/
 
 noncomputable section
 open scoped Matrix
 namespace BC4lean.OperatorKTheory
 
 universe u
 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
 
 /-- A finite matrix projection, with its finite index type recorded. -/
 structure FiniteProjection (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] where
   Index : Type
   [indexFintype : Fintype Index]
   [indexDecidableEq : DecidableEq Index]
   projection : MatrixProjection A Index
 
 attribute [instance] FiniteProjection.indexFintype FiniteProjection.indexDecidableEq
 
 namespace FiniteProjection
 
 /-- Record the index type of a matrix projection. -/
 def ofProjection {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixProjection A ι) :
     FiniteProjection A where
   Index := ι
   projection := p
 
 /-- Every object can be represented using a standard finite ordinal. -/
 def toFin (p : FiniteProjection A) : FiniteProjection A where
   Index := Fin (Fintype.card p.Index)
   projection := Projection.map
     (CStarMatrix.reindexₐ ℂ A (Fintype.equivFin p.Index)).toStarAlgHom p.projection
 
 /-- Block sum of finite matrix projections. -/
 def blockSum (p q : FiniteProjection A) : FiniteProjection A where
   Index := p.Index ⊕ q.Index
   projection := projectionBlockSum p.projection q.projection
 
 /-- The empty matrix represents zero. -/
 def zero : FiniteProjection A where
   Index := Empty
   projection := Projection.zero
 
 /-- Equivalence compares different sizes using a rectangular partial isometry. -/
 def Equivalent (p q : FiniteProjection A) : Prop := RectEquivalent p.projection q.projection
 
 theorem equivalent_refl (p : FiniteProjection A) : Equivalent p p :=
   rectEquivalent_refl p.projection
 
 theorem equivalent_symm {p q : FiniteProjection A} (h : Equivalent p q) : Equivalent q p :=
   rectEquivalent_symm h
 
 theorem equivalent_trans {p q r : FiniteProjection A}
     (h : Equivalent p q) (k : Equivalent q r) : Equivalent p r := rectEquivalent_trans h k
 
 theorem equivalent_toFin (p : FiniteProjection A) : Equivalent p p.toFin := by
   apply rectEquivalent_of_reindex _ _ (Fintype.equivFin p.Index).symm
   rfl
 
 theorem equivalent_zero {ι : Type} [Fintype ι] [DecidableEq ι] :
     Equivalent (ofProjection (Projection.zero : MatrixProjection A ι)) zero :=
   rectEquivalent_zero
 
 def setoid : Setoid (FiniteProjection A) where
   r := Equivalent
   iseqv := ⟨equivalent_refl, equivalent_symm, equivalent_trans⟩
 
 theorem blockSum_congr {p q r s : FiniteProjection A}
     (h : Equivalent p q) (k : Equivalent r s) : Equivalent (blockSum p r) (blockSum q s) :=
   rectEquivalent_blockSum h k
 
 theorem blockSum_comm (p q : FiniteProjection A) :
     Equivalent (blockSum p q) (blockSum q p) := by
   apply rectEquivalent_of_reindex _ _ (Equiv.sumComm q.Index p.Index)
   ext i j
   cases i <;> cases j <;> rfl
 
 theorem blockSum_assoc (p q r : FiniteProjection A) :
     Equivalent (blockSum (blockSum p q) r) (blockSum p (blockSum q r)) := by
   apply rectEquivalent_of_reindex _ _ (Equiv.sumAssoc p.Index q.Index r.Index).symm
   ext i j
   rcases i with i | (i | i) <;> rcases j with j | (j | j) <;> rfl
 
 theorem zero_blockSum (p : FiniteProjection A) : Equivalent (blockSum zero p) p := by
   apply equivalent_symm
   apply rectEquivalent_of_reindex _ _ (Equiv.emptySum Empty p.Index)
   ext i j
   rcases i with i | i
   · exact i.elim
   · rcases j with j | j
     · exact j.elim
     · rfl
 
 theorem blockSum_zero (p : FiniteProjection A) : Equivalent (blockSum p zero) p :=
   equivalent_trans (blockSum_comm p zero) (zero_blockSum p)
 
 end FiniteProjection
 
 /-- Stable Murray–von Neumann classes of finite matrix projections. -/
 abbrev StableProjectionMonoid (A : Type u) [CStarAlgebra A]
     [PartialOrder A] [StarOrderedRing A] := Quotient (FiniteProjection.setoid (A := A))
 
 namespace StableProjectionMonoid
 
 /-- The class represented by a finite matrix projection. -/
 def of (p : FiniteProjection A) : StableProjectionMonoid A := Quotient.mk _ p
 
 instance : Zero (StableProjectionMonoid A) := ⟨of FiniteProjection.zero⟩
 
 instance : Add (StableProjectionMonoid A) :=
   ⟨Quotient.map₂ FiniteProjection.blockSum (fun _ _ h _ _ k =>
     FiniteProjection.blockSum_congr h k)⟩
 
 @[simp] theorem of_blockSum (p q : FiniteProjection A) :
     of (FiniteProjection.blockSum p q) = of p + of q := rfl
 
 theorem of_eq_of_equivalent {p q : FiniteProjection A} (h : FiniteProjection.Equivalent p q) :
     of p = of q := Quotient.sound h
 
 theorem of_eq_iff (p q : FiniteProjection A) :
     of p = of q ↔ FiniteProjection.Equivalent p q := Quotient.eq
 
 /-- Block sum gives an additive commutative monoid on the stable classes. -/
 instance instAddCommMonoid : AddCommMonoid (StableProjectionMonoid A) where
   add_assoc a b c := Quotient.inductionOn₃ a b c fun p q r =>
     Quotient.sound (FiniteProjection.blockSum_assoc p q r)
   zero_add a := Quotient.inductionOn a fun p => Quotient.sound (FiniteProjection.zero_blockSum p)
   add_zero a := Quotient.inductionOn a fun p => Quotient.sound (FiniteProjection.blockSum_zero p)
   add_comm a b := Quotient.inductionOn₂ a b fun p q =>
     Quotient.sound (FiniteProjection.blockSum_comm p q)
   nsmul := nsmulRec
 
 @[simp] theorem of_zeroProjection {ι : Type} [Fintype ι] [DecidableEq ι] :
     of (FiniteProjection.ofProjection (Projection.zero : MatrixProjection A ι)) = 0 :=
   Quotient.sound FiniteProjection.equivalent_zero
 
 /-- The quotient really identifies zero-padding of a projection. -/
 theorem of_stabilize {ι κ : Type} [Fintype ι] [Fintype κ]
     [DecidableEq ι] [DecidableEq κ] (p : MatrixProjection A ι) :
     of (FiniteProjection.ofProjection (stabilizeProjection (κ := κ) p)) =
       of (FiniteProjection.ofProjection p) :=
   Quotient.sound (rectEquivalent_symm (rectEquivalent_stabilize p))
 
 /-- Allowing arbitrary small finite index types adds no extra classes. -/
 theorem exists_finRepresentative (x : StableProjectionMonoid A) :
     ∃ (n : ℕ) (p : MatrixProjection A (Fin n)), of (FiniteProjection.ofProjection p) = x := by
   refine Quotient.inductionOn x ?_
   intro p
   exact ⟨Fintype.card p.Index, p.toFin.projection,
     Quotient.sound (FiniteProjection.equivalent_symm (FiniteProjection.equivalent_toFin p))⟩
 
 end StableProjectionMonoid
 end BC4lean.OperatorKTheory

OperatorK0.lean

源码 SHA-256：bf4d9c7370788493ac0339b6bb884700db599ec86a87e5c5f147abe95e1492d6

 import BC4lean.StableProjectionMonoid
 import Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
 
 /-! # Unital operator K₀ as a Grothendieck group
 
 The input is the verified stable projection monoid. No cancellation or
 injectivity of its canonical map to the group completion is assumed.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 
 universe u v
 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
 
 /-- The unital operator K₀ group, obtained by group-completing V(A). -/
 abbrev K0 (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :=
   Algebra.GrothendieckAddGroup (StableProjectionMonoid A)
 
 /-- The canonical additive map from stable projection classes to K₀. -/
 def k0Class : StableProjectionMonoid A →+ K0 A := Algebra.GrothendieckAddGroup.of
 
 /-- The K₀ class of a finite matrix projection. -/
 def k0Projection (p : FiniteProjection A) : K0 A := k0Class (StableProjectionMonoid.of p)
 
 @[simp] theorem k0Projection_zero : k0Projection (FiniteProjection.zero : FiniteProjection A) = 0 :=
   map_zero k0Class
 
 @[simp] theorem k0Projection_blockSum (p q : FiniteProjection A) :
     k0Projection (FiniteProjection.blockSum p q) = k0Projection p + k0Projection q := by
   simp only [k0Projection, StableProjectionMonoid.of_blockSum, map_add]
 
 theorem k0Projection_eq_of_equivalent {p q : FiniteProjection A}
     (h : FiniteProjection.Equivalent p q) : k0Projection p = k0Projection q :=
   congrArg k0Class (StableProjectionMonoid.of_eq_of_equivalent h)
 
 /-- Every additive map from V(A) to an abelian group extends uniquely to K₀(A). -/
 def k0Universal {G : Type v} [AddCommGroup G] :
     (StableProjectionMonoid A →+ G) ≃ (K0 A →+ G) := Algebra.GrothendieckAddGroup.lift
 
 @[simp] theorem k0Universal_comp {G : Type v} [AddCommGroup G]
     (f : StableProjectionMonoid A →+ G) : (k0Universal f).comp k0Class = f :=
   k0Universal.left_inv f
 
 @[simp] theorem k0Universal_class {G : Type v} [AddCommGroup G]
     (f : StableProjectionMonoid A →+ G) (x : StableProjectionMonoid A) :
     k0Universal f (k0Class x) = f x := DFunLike.congr_fun (k0Universal_comp f) x
 
 theorem k0Universal_unique {G : Type v} [AddCommGroup G]
     (f : StableProjectionMonoid A →+ G) (g : K0 A →+ G)
     (h : g.comp k0Class = f) : k0Universal f = g := by
   apply k0Universal.symm.injective
   exact (k0Universal.left_inv f).trans h.symm
 
 end BC4lean.OperatorKTheory

ReducedOperatorK0.lean

源码 SHA-256：06b9ab3abc14445efde6e19e43a22cbe74174054d6d99dee277a5a77fbf55ec1

 import BC4lean.OperatorK0
 import BC4lean.ReducedGroupCStar
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
 
 /-! # The degree-zero analytic target
 
 The reduced group C⋆-algebra carries its canonical spectral order. This makes
 its stable projection monoid and unital operator K₀ available for every group.
 No assembly map, K₁ construction, or computation of these groups is asserted.
 -/
 
 noncomputable section
 namespace BC4lean
 
 universe u v
 variable (Γ : Type u) [Group Γ]
 
 /-- Stable projection classes for the reduced group C⋆-algebra, with spectral order. -/
 def ReducedProjectionMonoid : Type _ :=
   letI := CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
   letI := CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
   OperatorKTheory.StableProjectionMonoid (ReducedGroupCStar Γ)
 
 instance reducedProjectionAddCommMonoid : AddCommMonoid (ReducedProjectionMonoid Γ) := by
   letI := CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
   letI := CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
   exact inferInstanceAs (AddCommMonoid (OperatorKTheory.StableProjectionMonoid (ReducedGroupCStar Γ)))
 
 /-- The degree-zero analytic target K₀(Cᵣ*(Γ)), using the canonical spectral order. -/
 def ReducedK0 : Type _ :=
   letI := CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
   letI := CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
   OperatorKTheory.K0 (ReducedGroupCStar Γ)
 
 instance reducedK0AddCommGroup : AddCommGroup (ReducedK0 Γ) := by
   letI := CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
   letI := CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
   exact inferInstanceAs (AddCommGroup (OperatorKTheory.K0 (ReducedGroupCStar Γ)))
 
 /-- The canonical map from projection classes to the degree-zero analytic group. -/
 def reducedK0Class : ReducedProjectionMonoid Γ →+ ReducedK0 Γ := by
   letI := CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
   letI := CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
   exact OperatorKTheory.k0Class
 
 /-- The universal property specialized to the reduced group algebra. -/
 def reducedK0Universal {G : Type v} [AddCommGroup G] :
     (ReducedProjectionMonoid Γ →+ G) ≃ (ReducedK0 Γ →+ G) := by
   letI := CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
   letI := CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
   exact OperatorKTheory.k0Universal
 
 end BC4lean

MatrixProjectionMap.lean

源码 SHA-256：8302a0991199155f7aa3e835bb5fcc264ba4ad9b845b96f83dd81941cfb37592

 import BC4lean.StableProjectionMonoid
 
 /-! # Entrywise maps of finite matrix projections
 
 A unital complex ⋆-homomorphism acts on rectangular witnesses entrywise.
 Consequently it preserves stable Murray–von Neumann equivalence and block sums.
 -/
 
 noncomputable section
 open scoped Matrix
 namespace BC4lean.OperatorKTheory
 
 universe u v w
 variable {A : Type u} {B : Type v} {C : Type w}
 variable [CStarAlgebra A] [CStarAlgebra B] [CStarAlgebra C]
 variable {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
 
 /-- The entrywise map, bundled on square matrices with the C⋆-matrix norm. -/
 def matrixMap (φ : A →⋆ₐ[ℂ] B) : CStarMatrix ι ι A →⋆ₐ[ℂ] CStarMatrix ι ι B :=
   CStarMatrix.ofMatrixStarAlgEquiv.toStarAlgHom.comp
     (({ φ.toAlgHom.mapMatrix with
         map_star' := fun _ => Matrix.conjTranspose_map φ (fun a => map_star φ a) } :
           Matrix ι ι A →⋆ₐ[ℂ] Matrix ι ι B).comp
       CStarMatrix.ofMatrixStarAlgEquiv.symm.toStarAlgHom)
 
 @[simp] theorem matrixMap_apply (φ : A →⋆ₐ[ℂ] B) (M : CStarMatrix ι ι A) (i j : ι) :
     matrixMap φ M i j = φ (M i j) := rfl
 
 @[simp] theorem matrixMap_id :
     matrixMap (ι := ι) (StarAlgHom.id ℂ A) = StarAlgHom.id ℂ (CStarMatrix ι ι A) := by
   ext M i j
   rfl
 
 @[simp] theorem matrixMap_comp (ψ : B →⋆ₐ[ℂ] C) (φ : A →⋆ₐ[ℂ] B) :
     matrixMap (ι := ι) (ψ.comp φ) = (matrixMap ψ).comp (matrixMap φ) := by
   ext M i j
   rfl
 
 variable [PartialOrder A] [StarOrderedRing A]
 variable [PartialOrder B] [StarOrderedRing B]
 variable [PartialOrder C] [StarOrderedRing C]
 
 /-- Applying the entrywise homomorphism to a matrix projection. -/
 def matrixProjectionMap (φ : A →⋆ₐ[ℂ] B) (p : MatrixProjection A ι) : MatrixProjection B ι :=
   Projection.map (matrixMap φ) p
 
 @[simp] theorem projectionMatrix_map (φ : A →⋆ₐ[ℂ] B) (p : MatrixProjection A ι) :
     projectionMatrix (matrixProjectionMap φ p) = (projectionMatrix p).map φ := rfl
 
 @[simp] theorem matrixProjectionMap_id (p : MatrixProjection A ι) :
     matrixProjectionMap (StarAlgHom.id ℂ A) p = p := by
   apply Subtype.ext
   rfl
 
 @[simp] theorem matrixProjectionMap_comp (ψ : B →⋆ₐ[ℂ] C) (φ : A →⋆ₐ[ℂ] B)
     (p : MatrixProjection A ι) :
     matrixProjectionMap (ψ.comp φ) p = matrixProjectionMap ψ (matrixProjectionMap φ p) := rfl
 
 @[simp] theorem matrixProjectionMap_zero (φ : A →⋆ₐ[ℂ] B) :
     matrixProjectionMap φ (Projection.zero : MatrixProjection A ι) = Projection.zero :=
   Projection.map_zero _
 
 @[simp] theorem matrixProjectionMap_blockSum (φ : A →⋆ₐ[ℂ] B)
     (p : MatrixProjection A ι) (q : MatrixProjection A κ) :
     matrixProjectionMap φ (projectionBlockSum p q) =
       projectionBlockSum (matrixProjectionMap φ p) (matrixProjectionMap φ q) := by
   apply Subtype.ext
   ext i j
   cases i <;> cases j <;> simp [matrixProjectionMap, Projection.map,
     matrixMap_apply, projectionBlockSum, matrixBlockSum, Matrix.fromBlocks]
 
 /-- Map the actual rectangular witness; no injectivity of φ is required. -/
 theorem rectEquivalent_map (φ : A →⋆ₐ[ℂ] B)
     {p : MatrixProjection A ι} {q : MatrixProjection A κ} (h : RectEquivalent p q) :
     RectEquivalent (matrixProjectionMap φ p) (matrixProjectionMap φ q) := by
   obtain ⟨v, hv, hv'⟩ := h
   refine ⟨v.map φ, ?_, ?_⟩
   · simpa only [Matrix.map_mul, Matrix.conjTranspose_map φ (fun a => map_star φ a),
       projectionMatrix_map] using congrArg (fun M => M.map φ) hv
   · simpa only [Matrix.map_mul, Matrix.conjTranspose_map φ (fun a => map_star φ a),
       projectionMatrix_map] using congrArg (fun M => M.map φ) hv'
 
 namespace FiniteProjection
 
 /-- Entrywise transport keeps the finite index type. -/
 def map (φ : A →⋆ₐ[ℂ] B) (p : FiniteProjection A) : FiniteProjection B where
   Index := p.Index
   projection := matrixProjectionMap φ p.projection
 
 @[simp] theorem map_id (p : FiniteProjection A) : map (StarAlgHom.id ℂ A) p = p := by
   cases p
   simp only [map, matrixProjectionMap_id]
 
 @[simp] theorem map_comp (ψ : B →⋆ₐ[ℂ] C) (φ : A →⋆ₐ[ℂ] B) (p : FiniteProjection A) :
     map (ψ.comp φ) p = map ψ (map φ p) := rfl
 
 @[simp] theorem map_zero (φ : A →⋆ₐ[ℂ] B) : map φ zero = zero := by
   exact congrArg (fun p : MatrixProjection B Empty => ofProjection p) (matrixProjectionMap_zero φ)
 
 @[simp] theorem map_blockSum (φ : A →⋆ₐ[ℂ] B) (p q : FiniteProjection A) :
     map φ (blockSum p q) = blockSum (map φ p) (map φ q) := by
   exact congrArg (fun r : MatrixProjection B (p.Index ⊕ q.Index) => ofProjection r)
     (matrixProjectionMap_blockSum φ p.projection q.projection)
 
 theorem equivalent_map (φ : A →⋆ₐ[ℂ] B) {p q : FiniteProjection A}
     (h : Equivalent p q) : Equivalent (map φ p) (map φ q) := rectEquivalent_map φ h
 
 end FiniteProjection
 end BC4lean.OperatorKTheory

OperatorK0Functoriality.lean

源码 SHA-256：c8a9e804b78fef151656b5af0b31794e6400684db49dd051775e2a018dad8e37

 import BC4lean.MatrixProjectionMap
 import BC4lean.OperatorK0
 
 /-! # Functoriality of unital operator K₀
 
 First descend entrywise maps to the stable projection monoid, then use the
 Grothendieck group universal property. No cancellation hypothesis is needed.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 
 universe u v w t
 variable {A : Type u} {B : Type v} {C : Type w}
 variable [CStarAlgebra A] [CStarAlgebra B] [CStarAlgebra C]
 variable [PartialOrder A] [StarOrderedRing A]
 variable [PartialOrder B] [StarOrderedRing B]
 variable [PartialOrder C] [StarOrderedRing C]
 
 namespace StableProjectionMonoid
 
 /-- The additive map on stable projection classes induced by a unital ⋆-homomorphism. -/
 def map (φ : A →⋆ₐ[ℂ] B) : StableProjectionMonoid A →+ StableProjectionMonoid B where
   toFun := Quotient.map (FiniteProjection.map φ) (fun _ _ h => FiniteProjection.equivalent_map φ h)
   map_zero' := by
     change of (FiniteProjection.map φ FiniteProjection.zero) = of FiniteProjection.zero
     rw [FiniteProjection.map_zero]
   map_add' x y := by
     refine Quotient.inductionOn₂ x y ?_
     intro p q
     change of (FiniteProjection.map φ (FiniteProjection.blockSum p q)) =
       of (FiniteProjection.blockSum (FiniteProjection.map φ p) (FiniteProjection.map φ q))
     rw [FiniteProjection.map_blockSum]
 
 @[simp] theorem map_of (φ : A →⋆ₐ[ℂ] B) (p : FiniteProjection A) :
     map φ (of p) = of (FiniteProjection.map φ p) := rfl
 
 @[simp] theorem map_id : map (StarAlgHom.id ℂ A) = AddMonoidHom.id (StableProjectionMonoid A) := by
   ext x
   refine Quotient.inductionOn x ?_
   intro p
   change of (FiniteProjection.map (StarAlgHom.id ℂ A) p) = of p
   rw [FiniteProjection.map_id]
 
 @[simp] theorem map_comp (ψ : B →⋆ₐ[ℂ] C) (φ : A →⋆ₐ[ℂ] B) :
     map (ψ.comp φ) = (map ψ).comp (map φ) := by
   ext x
   refine Quotient.inductionOn x ?_
   intro p
   rfl
 
 end StableProjectionMonoid
 
 /-- The homomorphism K₀(A) → K₀(B) induced by a unital complex ⋆-homomorphism. -/
 def k0Map (φ : A →⋆ₐ[ℂ] B) : K0 A →+ K0 B :=
   k0Universal (k0Class.comp (StableProjectionMonoid.map φ))
 
 @[simp] theorem k0Map_class (φ : A →⋆ₐ[ℂ] B) (x : StableProjectionMonoid A) :
     k0Map φ (k0Class x) = k0Class (StableProjectionMonoid.map φ x) :=
   k0Universal_class _ x
 
 /-- Naturality of the canonical group-completion homomorphism. -/
 theorem k0Map_comp_class (φ : A →⋆ₐ[ℂ] B) :
     (k0Map φ).comp k0Class = k0Class.comp (StableProjectionMonoid.map φ) :=
   k0Universal_comp _
 
 @[simp] theorem k0Map_projection (φ : A →⋆ₐ[ℂ] B) (p : FiniteProjection A) :
     k0Map φ (k0Projection p) = k0Projection (FiniteProjection.map φ p) :=
   k0Map_class φ (StableProjectionMonoid.of p)
 
 /-- Homomorphisms out of K₀ are determined by their values on projection classes. -/
 theorem k0Hom_ext {G : Type t} [AddCommGroup G] {f g : K0 A →+ G}
     (h : ∀ p : FiniteProjection A, f (k0Projection p) = g (k0Projection p)) : f = g := by
   apply k0Universal.symm.injective
   change f.comp k0Class = g.comp k0Class
   ext x
   refine Quotient.inductionOn x ?_
   intro p
   exact h p
 
 @[simp] theorem k0Map_id : k0Map (StarAlgHom.id ℂ A) = AddMonoidHom.id (K0 A) := by
   apply k0Hom_ext
   intro p
   simp only [k0Map_projection, FiniteProjection.map_id, AddMonoidHom.id_apply]
 
 @[simp] theorem k0Map_comp (ψ : B →⋆ₐ[ℂ] C) (φ : A →⋆ₐ[ℂ] B) :
     k0Map (ψ.comp φ) = (k0Map ψ).comp (k0Map φ) := by
   apply k0Hom_ext
   intro p
   simp only [k0Map_projection, FiniteProjection.map_comp, AddMonoidHom.comp_apply]
 
 /-- The induced map is the unique homomorphism with the entrywise projection-class formula. -/
 theorem k0Map_unique (φ : A →⋆ₐ[ℂ] B) (f : K0 A →+ K0 B)
     (h : ∀ p : FiniteProjection A, f (k0Projection p) = k0Projection (FiniteProjection.map φ p)) :
     k0Map φ = f := by
   apply k0Hom_ext
   intro p
   exact (k0Map_projection φ p).trans (h p).symm
 
 end BC4lean.OperatorKTheory

OperatorK0Equivalence.lean

源码 SHA-256：9e950900ab47ebfbfe4b9f715a551aade982f90c85b6e2d88b9ed5a56a9c0307

 import BC4lean.OperatorK0Functoriality
 
 /-! # Invariance of unital K₀ under star-algebra equivalence
 
 The forward map comes from the given equivalence and the inverse map from its
 inverse. Both inverse laws follow from functoriality. The compatible star orders
 remain the explicit implementation assumptions of the matrix-algebra API.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 
 universe u v w
 variable {A : Type u} {B : Type v} {C : Type w}
 variable [CStarAlgebra A] [CStarAlgebra B] [CStarAlgebra C]
 variable [PartialOrder A] [StarOrderedRing A]
 variable [PartialOrder B] [StarOrderedRing B]
 variable [PartialOrder C] [StarOrderedRing C]
 
 namespace StableProjectionMonoid
 
 theorem map_leftInverse (e : A ≃⋆ₐ[ℂ] B) :
     Function.LeftInverse (map e.symm.toStarAlgHom) (map e.toStarAlgHom) := by
   intro x
   have h : e.symm.toStarAlgHom.comp e.toStarAlgHom = StarAlgHom.id ℂ A := by
     ext a
     exact e.symm_apply_apply a
   change ((map e.symm.toStarAlgHom).comp (map e.toStarAlgHom)) x = x
   rw [← map_comp, h, map_id]
   rfl
 
 theorem map_rightInverse (e : A ≃⋆ₐ[ℂ] B) :
     Function.RightInverse (map e.symm.toStarAlgHom) (map e.toStarAlgHom) := by
   intro x
   have h : e.toStarAlgHom.comp e.symm.toStarAlgHom = StarAlgHom.id ℂ B := by
     ext a
     exact e.apply_symm_apply a
   change ((map e.toStarAlgHom).comp (map e.symm.toStarAlgHom)) x = x
   rw [← map_comp, h, map_id]
   rfl
 
 /-- A unital star-algebra equivalence induces an additive equivalence of stable projection monoids. -/
 def mapEquiv (e : A ≃⋆ₐ[ℂ] B) : StableProjectionMonoid A ≃+ StableProjectionMonoid B where
   toFun := map e.toStarAlgHom
   invFun := map e.symm.toStarAlgHom
   left_inv := map_leftInverse e
   right_inv := map_rightInverse e
   map_add' := (map e.toStarAlgHom).map_add
 
 @[simp] theorem mapEquiv_toAddMonoidHom (e : A ≃⋆ₐ[ℂ] B) :
     (mapEquiv e).toAddMonoidHom = map e.toStarAlgHom := rfl
 
 @[simp] theorem mapEquiv_of (e : A ≃⋆ₐ[ℂ] B) (p : FiniteProjection A) :
     mapEquiv e (of p) = of (FiniteProjection.map e.toStarAlgHom p) := rfl
 
 @[simp] theorem mapEquiv_refl :
     mapEquiv (StarAlgEquiv.refl ℂ A) = AddEquiv.refl (StableProjectionMonoid A) := by
   ext x
   change map (StarAlgHom.id ℂ A) x = x
   rw [map_id]
   rfl
 
 @[simp] theorem mapEquiv_symm (e : A ≃⋆ₐ[ℂ] B) : mapEquiv e.symm = (mapEquiv e).symm := by
   ext x
   rfl
 
 @[simp] theorem mapEquiv_trans (e : A ≃⋆ₐ[ℂ] B) (f : B ≃⋆ₐ[ℂ] C) :
     mapEquiv (e.trans f) = (mapEquiv e).trans (mapEquiv f) := by
   ext x
   exact DFunLike.congr_fun (map_comp f.toStarAlgHom e.toStarAlgHom) x
 
 end StableProjectionMonoid
 
 theorem k0Map_leftInverse (e : A ≃⋆ₐ[ℂ] B) :
     Function.LeftInverse (k0Map e.symm.toStarAlgHom) (k0Map e.toStarAlgHom) := by
   intro x
   have h : e.symm.toStarAlgHom.comp e.toStarAlgHom = StarAlgHom.id ℂ A := by
     ext a
     exact e.symm_apply_apply a
   change ((k0Map e.symm.toStarAlgHom).comp (k0Map e.toStarAlgHom)) x = x
   rw [← k0Map_comp, h, k0Map_id]
   rfl
 
 theorem k0Map_rightInverse (e : A ≃⋆ₐ[ℂ] B) :
     Function.RightInverse (k0Map e.symm.toStarAlgHom) (k0Map e.toStarAlgHom) := by
   intro x
   have h : e.toStarAlgHom.comp e.symm.toStarAlgHom = StarAlgHom.id ℂ B := by
     ext a
     exact e.apply_symm_apply a
   change ((k0Map e.toStarAlgHom).comp (k0Map e.symm.toStarAlgHom)) x = x
   rw [← k0Map_comp, h, k0Map_id]
   rfl
 
 /-- The canonical additive equivalence on unital K₀ induced by a star-algebra equivalence. -/
 def k0Equiv (e : A ≃⋆ₐ[ℂ] B) : K0 A ≃+ K0 B where
   toFun := k0Map e.toStarAlgHom
   invFun := k0Map e.symm.toStarAlgHom
   left_inv := k0Map_leftInverse e
   right_inv := k0Map_rightInverse e
   map_add' := (k0Map e.toStarAlgHom).map_add
 
 @[simp] theorem k0Equiv_toAddMonoidHom (e : A ≃⋆ₐ[ℂ] B) :
     (k0Equiv e).toAddMonoidHom = k0Map e.toStarAlgHom := rfl
 
 @[simp] theorem k0Equiv_class (e : A ≃⋆ₐ[ℂ] B) (x : StableProjectionMonoid A) :
     k0Equiv e (k0Class x) = k0Class (StableProjectionMonoid.mapEquiv e x) :=
   k0Map_class e.toStarAlgHom x
 
 @[simp] theorem k0Equiv_projection (e : A ≃⋆ₐ[ℂ] B) (p : FiniteProjection A) :
     k0Equiv e (k0Projection p) = k0Projection (FiniteProjection.map e.toStarAlgHom p) :=
   k0Map_projection e.toStarAlgHom p
 
 @[simp] theorem k0Equiv_refl : k0Equiv (StarAlgEquiv.refl ℂ A) = AddEquiv.refl (K0 A) := by
   ext x
   change k0Map (StarAlgHom.id ℂ A) x = x
   rw [k0Map_id]
   rfl
 
 @[simp] theorem k0Equiv_symm (e : A ≃⋆ₐ[ℂ] B) : k0Equiv e.symm = (k0Equiv e).symm := by
   ext x
   rfl
 
 @[simp] theorem k0Equiv_trans (e : A ≃⋆ₐ[ℂ] B) (f : B ≃⋆ₐ[ℂ] C) :
     k0Equiv (e.trans f) = (k0Equiv e).trans (k0Equiv f) := by
   ext x
   exact DFunLike.congr_fun (k0Map_comp f.toStarAlgHom e.toStarAlgHom) x
 
 end BC4lean.OperatorKTheory

ReducedCompletionK0.lean

源码 SHA-256：f46dd10925af007c8f7fa33ec2becbc25df9a0082c739a1de12cc630f4fcb21c

 import BC4lean.OperatorK0Equivalence
 import BC4lean.ReducedCompletion
 import BC4lean.ReducedOperatorK0
 
 /-! # Abstract and concrete models of the degree-zero analytic target
 
 The actual reduced-norm completion and the concrete reduced group C⋆-algebra
 are equipped with their canonical spectral orders. Their already verified
 star-algebra equivalence induces the comparison on projection classes and K₀.
 No countability assumption, computation of K₀, or assembly theorem is used.
 -/
 
 noncomputable section
 namespace BC4lean
 open OperatorKTheory
 
 universe u
 variable (Γ : Type u) [Group Γ]
 
 local instance completionSpectralOrder : PartialOrder (ReducedCompletion Γ) :=
   CStarAlgebra.spectralOrder (ReducedCompletion Γ)
 
 local instance completionSpectralOrderedRing : StarOrderedRing (ReducedCompletion Γ) :=
   CStarAlgebra.spectralOrderedRing (ReducedCompletion Γ)
 
 local instance reducedSpectralOrder : PartialOrder (ReducedGroupCStar Γ) :=
   CStarAlgebra.spectralOrder (ReducedGroupCStar Γ)
 
 local instance reducedSpectralOrderedRing : StarOrderedRing (ReducedGroupCStar Γ) :=
   CStarAlgebra.spectralOrderedRing (ReducedGroupCStar Γ)
 
 /-- Stable projection classes in the actual abstract reduced-norm completion. -/
 def ReducedCompletionProjectionMonoid : Type _ := StableProjectionMonoid (ReducedCompletion Γ)
 
 instance reducedCompletionProjectionAddCommMonoid :
     AddCommMonoid (ReducedCompletionProjectionMonoid Γ) :=
   inferInstanceAs (AddCommMonoid (StableProjectionMonoid (ReducedCompletion Γ)))
 
 /-- K₀ of the abstract reduced-norm completion, using its canonical spectral order. -/
 def ReducedCompletionK0 : Type _ := K0 (ReducedCompletion Γ)
 
 instance reducedCompletionK0AddCommGroup : AddCommGroup (ReducedCompletionK0 Γ) :=
   inferInstanceAs (AddCommGroup (K0 (ReducedCompletion Γ)))
 
 /-- The group-completion map for stable projection classes in the abstract model. -/
 def reducedCompletionK0Class : ReducedCompletionProjectionMonoid Γ →+ ReducedCompletionK0 Γ :=
   k0Class
 
 /-- Apply the canonical algebra comparison entrywise to a finite matrix projection. -/
 def reducedCompletionProjectionMap (p : FiniteProjection (ReducedCompletion Γ)) :
     FiniteProjection (ReducedGroupCStar Γ) :=
   FiniteProjection.map (reducedCompletionEquiv Γ).toStarAlgHom p
 
 @[simp] theorem reducedCompletionProjectionMap_entry (p : FiniteProjection (ReducedCompletion Γ))
     (i j : p.Index) :
     projectionMatrix (reducedCompletionProjectionMap Γ p).projection i j =
       reducedCompletionEquiv Γ (projectionMatrix p.projection i j) := rfl
 
 /-- Canonical comparison of the stable projection monoids of the two models. -/
 def reducedCompletionProjectionEquiv :
     ReducedCompletionProjectionMonoid Γ ≃+ ReducedProjectionMonoid Γ :=
   StableProjectionMonoid.mapEquiv (reducedCompletionEquiv Γ)
 
 @[simp] theorem reducedCompletionProjectionEquiv_of (p : FiniteProjection (ReducedCompletion Γ)) :
     reducedCompletionProjectionEquiv Γ (StableProjectionMonoid.of p) =
       StableProjectionMonoid.of (reducedCompletionProjectionMap Γ p) :=
   StableProjectionMonoid.mapEquiv_of (reducedCompletionEquiv Γ) p
 
 @[simp] theorem reducedCompletionProjectionEquiv_symm_of
     (p : FiniteProjection (ReducedGroupCStar Γ)) :
     (reducedCompletionProjectionEquiv Γ).symm (StableProjectionMonoid.of p) =
       StableProjectionMonoid.of
         (FiniteProjection.map (reducedCompletionEquiv Γ).symm.toStarAlgHom p) := rfl
 
 /-- The abstract completion gives canonically the same degree-zero analytic target. -/
 def reducedCompletionK0Equiv : ReducedCompletionK0 Γ ≃+ ReducedK0 Γ :=
   k0Equiv (reducedCompletionEquiv Γ)
 
 @[simp] theorem reducedCompletionK0Equiv_class (x : ReducedCompletionProjectionMonoid Γ) :
     reducedCompletionK0Equiv Γ (reducedCompletionK0Class Γ x) =
       reducedK0Class Γ (reducedCompletionProjectionEquiv Γ x) :=
   k0Equiv_class (reducedCompletionEquiv Γ) x
 
 @[simp] theorem reducedCompletionK0Equiv_symm_class (x : ReducedProjectionMonoid Γ) :
     (reducedCompletionK0Equiv Γ).symm (reducedK0Class Γ x) =
       reducedCompletionK0Class Γ ((reducedCompletionProjectionEquiv Γ).symm x) :=
   k0Equiv_class (reducedCompletionEquiv Γ).symm x
 
 /-- Naturality of group completion for the abstract/concrete comparison. -/
 theorem reducedCompletionK0Equiv_comp_class :
     (reducedCompletionK0Equiv Γ).toAddMonoidHom.comp (reducedCompletionK0Class Γ) =
       (reducedK0Class Γ).comp (reducedCompletionProjectionEquiv Γ).toAddMonoidHom := by
   ext x
   exact reducedCompletionK0Equiv_class Γ x
 
 @[simp] theorem reducedCompletionK0Equiv_projection (p : FiniteProjection (ReducedCompletion Γ)) :
     reducedCompletionK0Equiv Γ (reducedCompletionK0Class Γ (StableProjectionMonoid.of p)) =
       reducedK0Class Γ (StableProjectionMonoid.of (reducedCompletionProjectionMap Γ p)) :=
   k0Equiv_projection (reducedCompletionEquiv Γ) p
 
 /-- The comparison is uniquely determined by compatibility with projection classes. -/
 theorem reducedCompletionK0Equiv_unique (f : ReducedCompletionK0 Γ →+ ReducedK0 Γ)
     (h : f.comp (reducedCompletionK0Class Γ) =
       (reducedK0Class Γ).comp (reducedCompletionProjectionEquiv Γ).toAddMonoidHom) :
     (reducedCompletionK0Equiv Γ).toAddMonoidHom = f := by
   apply k0Hom_ext
   intro p
   exact (reducedCompletionK0Equiv_class Γ (StableProjectionMonoid.of p)).trans
     (DFunLike.congr_fun h (StableProjectionMonoid.of p)).symm
 
 end BC4lean

UnitaryRotation.lean

源码 SHA-256：997580bc744a09a0c35007ceb52f228aaefc3f5a884f3e7b564ccced1e999dc7

 import BC4lean.UnitaryHomotopy
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 
 /-! # Block rotation and the inverse homotopy for matrix unitaries
 
 The explicit rotation path gives the inverse mechanism for stable K₁.
 The stable quotient and its group structure are separate constructions.
 -/
 
 noncomputable section
 namespace BC4lean.OperatorKTheory
 open scoped Matrix
 
 variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
 
 /-- The scalar block rotation through angle `t`, with identity blocks indexed by `ι`. -/
 def rotationMatrix (t : ℝ) : CStarMatrix (ι ⊕ ι) (ι ⊕ ι) A :=
   CStarMatrix.ofMatrix (Matrix.fromBlocks
     (Real.cos t • (1 : Matrix ι ι A)) (-Real.sin t • (1 : Matrix ι ι A))
     (Real.sin t • (1 : Matrix ι ι A)) (Real.cos t • (1 : Matrix ι ι A)))
 
 omit [PartialOrder A] [StarOrderedRing A] in
 theorem rotationMatrix_mem_unitary (t : ℝ) :
     rotationMatrix (A := A) (ι := ι) t ∈ unitary (CStarMatrix (ι ⊕ ι) (ι ⊕ ι) A) := by
   have h : Real.cos t * Real.cos t + Real.sin t * Real.sin t = 1 := by
     nlinarith [Real.sin_sq_add_cos_sq t]
   have h' : Real.sin t * Real.sin t + Real.cos t * Real.cos t = 1 := by
     simpa only [add_comm] using h
   rw [Unitary.mem_iff]
   let M : Matrix (ι ⊕ ι) (ι ⊕ ι) A := Matrix.fromBlocks
     (Real.cos t • (1 : Matrix ι ι A)) (-Real.sin t • (1 : Matrix ι ι A))
     (Real.sin t • (1 : Matrix ι ι A)) (Real.cos t • (1 : Matrix ι ι A))
   change (Mᴴ * M = 1) ∧ (M * Mᴴ = 1)
   dsimp [M]
   simp only [Matrix.fromBlocks_conjTranspose, Matrix.conjTranspose_smul,
     star_trivial, Matrix.conjTranspose_one, Matrix.fromBlocks_multiply,
     Matrix.smul_mul, Matrix.mul_smul, Matrix.one_mul, smul_smul]
   constructor <;>
     simp [mul_neg, neg_smul, ← add_smul, h, h', mul_comm, Matrix.fromBlocks_one]
 
 /-- Scalar rotations, bundled as matrix unitaries. -/
 def rotationUnitary (t : ℝ) : MatrixUnitary A (ι ⊕ ι) :=
   ⟨rotationMatrix t, rotationMatrix_mem_unitary t⟩
 
 theorem continuous_rotationUnitary :
     Continuous (rotationUnitary (A := A) (ι := ι)) := by
   apply Continuous.subtype_mk
   exact CStarMatrix.ofMatrixL.continuous.comp
     ((Real.continuous_cos.smul continuous_const).matrix_fromBlocks
       (Real.continuous_sin.neg.smul continuous_const)
       (Real.continuous_sin.smul continuous_const)
       (Real.continuous_cos.smul continuous_const))
 
 @[simp] theorem rotationUnitary_zero : rotationUnitary (A := A) (ι := ι) 0 = 1 := by
   apply Subtype.ext
   change rotationMatrix 0 = 1
   simp only [rotationMatrix, Real.cos_zero, Real.sin_zero, neg_zero,
     one_smul, zero_smul, Matrix.fromBlocks_one]
   rfl
 
 @[simp] theorem unitaryBlockSum_one :
     unitaryBlockSum (1 : MatrixUnitary A ι) (1 : MatrixUnitary A ι) = 1 := by
   apply Subtype.ext
   exact matrixBlockSum_one
 
 theorem unitaryBlockSum_mul (u v w z : MatrixUnitary A ι) :
     unitaryBlockSum u v * unitaryBlockSum w z = unitaryBlockSum (u * w) (v * z) := by
   apply Subtype.ext
   change matrixBlockSum (u : CStarMatrix ι ι A) (v : CStarMatrix ι ι A) *
     matrixBlockSum (w : CStarMatrix ι ι A) (z : CStarMatrix ι ι A) =
     matrixBlockSum ((u : CStarMatrix ι ι A) * (w : CStarMatrix ι ι A))
       ((v : CStarMatrix ι ι A) * (z : CStarMatrix ι ι A))
   exact matrixBlockSum_mul (u : CStarMatrix ι ι A) (w : CStarMatrix ι ι A)
     (v : CStarMatrix ι ι A) (z : CStarMatrix ι ι A)
 
 /-- A quarter-turn exchanges diagonal blocks by conjugation. -/
 theorem rotationUnitary_conjugate (u v : MatrixUnitary A ι) :
     rotationUnitary (Real.pi / 2) * unitaryBlockSum u v *
       (rotationUnitary (Real.pi / 2))⁻¹ = unitaryBlockSum v u := by
   apply Subtype.ext
   let U : Matrix ι ι A := CStarMatrix.ofMatrix.symm u
   let V : Matrix ι ι A := CStarMatrix.ofMatrix.symm v
   let R : Matrix (ι ⊕ ι) (ι ⊕ ι) A := Matrix.fromBlocks
     (Real.cos (Real.pi / 2) • (1 : Matrix ι ι A))
     (-Real.sin (Real.pi / 2) • (1 : Matrix ι ι A))
     (Real.sin (Real.pi / 2) • (1 : Matrix ι ι A))
     (Real.cos (Real.pi / 2) • (1 : Matrix ι ι A))
   change R * Matrix.fromBlocks U 0 0 V * Rᴴ = Matrix.fromBlocks V 0 0 U
   dsimp [R]
   simp [Real.cos_pi_div_two, Real.sin_pi_div_two,
     Matrix.fromBlocks_conjTranspose, Matrix.fromBlocks_multiply]
 
 /-- Rotate the second factor from the lower block into the upper block. -/
 def unitaryBlockProductPath (u v : MatrixUnitary A ι) :
     Path (unitaryBlockSum u v) (unitaryBlockSum (u * v) 1) where
   toFun t := unitaryBlockSum u 1 * rotationUnitary ((t : ℝ) * (Real.pi / 2)) *
     unitaryBlockSum 1 v * (rotationUnitary ((t : ℝ) * (Real.pi / 2)))⁻¹
   continuous_toFun := by
     have h : Continuous (fun t : unitInterval =>
         rotationUnitary (A := A) (ι := ι) ((t : ℝ) * (Real.pi / 2))) :=
       continuous_rotationUnitary.comp
       (continuous_subtype_val.mul_const (Real.pi / 2))
     exact ((continuous_const.mul h).mul continuous_const).mul h.inv
   source' := by
     simp [unitaryBlockSum_mul]
   target' := by
     simp only [Set.Icc.coe_one, one_mul]
     rw [mul_assoc (unitaryBlockSum u 1), mul_assoc (unitaryBlockSum u 1),
       rotationUnitary_conjugate]
     simp only [unitaryBlockSum_mul, one_mul]
 
 /-- After doubling the matrix size, block sum agrees with multiplication up to norm homotopy. -/
 theorem unitaryHomotopic_blockSum_mul (u v : MatrixUnitary A ι) :
     UnitaryHomotopic (unitaryBlockSum u v) (unitaryBlockSum (u * v) 1) :=
   ⟨unitaryBlockProductPath u v⟩
 
 /-- The block sum of a unitary and its adjoint has an explicit path to the identity. -/
 def unitaryInversePath (u : MatrixUnitary A ι) :
     Path (unitaryBlockSum u (star u)) 1 := by
   simpa using unitaryBlockProductPath u (star u)
 
 theorem unitaryHomotopic_blockSum_star (u : MatrixUnitary A ι) :
     UnitaryHomotopic (unitaryBlockSum u (star u)) 1 :=
   ⟨unitaryInversePath u⟩
 
 theorem unitaryHomotopic_star_blockSum (u : MatrixUnitary A ι) :
     UnitaryHomotopic (unitaryBlockSum (star u) u) 1 := by
   simpa using unitaryHomotopic_blockSum_star (star u)
 
 end BC4lean.OperatorKTheory