MathlibAnnex/Analysis/CStarAlgebra/Quotient/Image.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import MathlibAnnex.Analysis.CStarAlgebra.Quotient.KernelAlgebra7import Mathlib.Algebra.Star.NonUnitalSubalgebra8import Mathlib.Analysis.CStarAlgebra.Classes910/-!11# The isometric first-isomorphism theorem onto the actual representation image1213The range is `NonUnitalStarAlgHom.range q`, with its inherited subspace norm,14not an abstract algebra declared to be an image. Its closedness comes from15the complete standard kernel quotient. The equivalence below preserves16products, addition, complex scalars and star, and is isometric.17-/1819set_option autoImplicit false20noncomputable section21open Set22open scoped CStarAlgebra2324namespace MathlibAnnex.Analysis.CStarAlgebra.HomKernelQuotient2526universe u v27variable {A : Type u} {B : Type v}28variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]29variable (q : A →⋆ₙₐ[ℂ] B)3031/-- Codomain restriction to the literal algebraic range. -/32def toImageHom : HomKernelQuotient q →⋆ₙₐ[ℂ] (NonUnitalStarAlgHom.range q) :=33  NonUnitalStarAlgHom.codRestrict (toCodomainHom q) (NonUnitalStarAlgHom.range q) fun x => by34    change toCodomain q x ∈ Set.range q35    rw [← range_toCodomain q]36    exact ⟨x, rfl⟩3738@[simp]39theorem coe_toImageHom (x : HomKernelQuotient q) :40    (toImageHom q x : B) = toCodomain q x := rfl4142theorem toImageHom_bijective : Function.Bijective (toImageHom q) := by43  constructor44  · intro x y h45    apply toCodomain_injective q46    exact congrArg Subtype.val h47  · intro b48    obtain ⟨a, ha⟩ := (NonUnitalStarAlgHom.mem_range q).mp b.property49    exact ⟨mk q a, Subtype.ext ha⟩5051/-- The first-isomorphism equivalence, with the ACTUAL quotient and ACTUAL range. -/52def imageStarAlgEquiv : HomKernelQuotient q ≃⋆ₐ[ℂ] (NonUnitalStarAlgHom.range q) :=53  { Equiv.ofBijective (toImageHom q) (toImageHom_bijective q) with54    map_add' := map_add (toImageHom q)55    map_mul' := map_mul (toImageHom q)56    map_smul' := map_smul (toImageHom q)57    map_star' := map_star (toImageHom q) }5859@[simp]60theorem imageStarAlgEquiv_apply (x : HomKernelQuotient q) :61    (imageStarAlgEquiv q x : B) = toCodomain q x := rfl6263/-- The quotient-to-image map has the expected representative formula. -/64@[simp]65theorem imageStarAlgEquiv_mk (a : A) :66    imageStarAlgEquiv q (mk q a) = (NonUnitalStarAlgHom.rangeRestrict q) a := by67  apply Subtype.ext68  rfl6970variable [PartialOrder A] [StarOrderedRing A]71variable [PartialOrder B] [StarOrderedRing B]7273/-- The algebraic range, with its original subspace norm, is norm-closed. -/74theorem isClosed_image : IsClosed ((NonUnitalStarAlgHom.range q) : Set B) := isClosed_range q7576/-- Named structure: installing it locally retains the inherited range norm77and supplies the proved completeness, rather than assuming it. -/78def imageCStarAlgebra : NonUnitalCStarAlgebra (NonUnitalStarAlgHom.range q) :=79  NonUnitalStarSubalgebra.nonUnitalCStarAlgebra (NonUnitalStarAlgHom.range q) (h_closed := isClosed_image q)8081theorem norm_imageStarAlgEquiv (x : HomKernelQuotient q) :82    ‖imageStarAlgEquiv q x‖ = ‖x‖ := norm_toCodomain q x8384theorem isometry_imageStarAlgEquiv : Isometry (imageStarAlgEquiv q) :=85  AddMonoidHomClass.isometry_of_norm (imageStarAlgEquiv q) (norm_imageStarAlgEquiv q)8687/-- The same map exposed as a linear isometry equivalence for Banach clients. -/88def imageLinearIsometryEquiv : HomKernelQuotient q ≃ₗᵢ[ℂ] (NonUnitalStarAlgHom.range q) :=89  { toLinearEquiv :=90      { (imageStarAlgEquiv q).toEquiv with91        map_add' := map_add (imageStarAlgEquiv q)92        map_smul' := map_smul (imageStarAlgEquiv q) }93    norm_map' := norm_imageStarAlgEquiv q }9495@[simp]96theorem imageLinearIsometryEquiv_apply (x : HomKernelQuotient q) :97    imageLinearIsometryEquiv q x = imageStarAlgEquiv q x := rfl9899/-- This equality is about the standard quotient norm, not a newly assigned norm. -/100theorem norm_mk_eq (a : A) : ‖mk q a‖ = ‖q a‖ := (norm_toCodomain q (mk q a)).symm101102/-- Every point of the genuine quotient has an EXACT norm-minimizing representative. -/103theorem exists_representative_norm_eq (x : HomKernelQuotient q) :104    ∃ a : A, mk q a = x ∧ ‖a‖ = ‖x‖ := by105  obtain ⟨b, rfl⟩ := mk_surjective q x106  obtain ⟨a, ha, hn⟩ := exists_same_image_norm_eq q b107  exact ⟨a, (mk_eq_mk_iff q a b).2 ha, hn.trans (norm_mk_eq q b).symm⟩108109end MathlibAnnex.Analysis.CStarAlgebra.HomKernelQuotient