OAI/Analysis/KadisonKastler/IsometryRangeCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coordinates from two isometric embeddings with the same range

  1. theorem OAI.KadisonKastler.isometry_adjoint_self_apply line 19
  2. def OAI.KadisonKastler.isometryRangeCoordinates line 24

    Source documentation

    The adjoint of the second embedding gives coordinates for the first.

    def isometryRangeCoordinates (J : E →ₗᵢ[ℂ] K) (W : F →ₗᵢ[ℂ] K)
    (h : LinearMap.range J.toLinearMap = LinearMap.range W.toLinearMap) : E ≃ₗᵢ[ℂ] F := by
…
  3. theorem OAI.KadisonKastler.isometryRangeCoordinates_apply line 44
  4. theorem OAI.KadisonKastler.isometryRangeCoordinates_intertwines line 49
  5. theorem OAI.KadisonKastler.isometry_range_iff_field_fixed line 60