Exact source: MathlibAnnex/Analysis/Normed/Plucker/ModelRigidity.lean
Pinned GitHub source · Raw UTF-8 source
Back to All Plücker bodies determine the norm up to linear isometry
1import MathlibAnnex.Analysis.Normed.Plucker.LimitRecovery2import MathlibAnnex.Analysis.Normed.Plucker.BodyInvariance3import MathlibAnnex.Analysis.Normed.Module.EquivalentSeminorm.Transport45noncomputable section6set_option autoImplicit false7open Set8universe u v910namespace MathlibAnnex11namespace PluckerRecovery.Internal12/-- Private coordinate witness retaining bijectivity, ball image and exact norm equality. -/13private structure CoordinateLinearIsometryCertificate {m : ℕ}14 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ)) where15 linearMap : (Fin (m + 1) → ℝ) →L[ℝ] (Fin (m + 1) → ℝ)16 injective : Function.Injective linearMap17 surjective : Function.Surjective linearMap18 image_closedUnitBall : linearMap '' MX.closedUnitBall = MY.closedUnitBall19 seminorm_linearMap_eq : ∀ x, MY.p (linearMap x) = MX.p x2021private theorem nonempty_coordinateLinearIsometry_of_all_body_eq {m : ℕ}22 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))23 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) :24 Nonempty (CoordinateLinearIsometryCertificate MX MY) := by25 let C := Classical.choice (PluckerRecovery.nonempty_limitCertificate_of_pluckerBodies_eq MX MY hBodies)26 have hball : C.linearMap '' MX.closedUnitBall = MY.closedUnitBall := C.image_unitBall_eq27 exact ⟨{28 linearMap := C.linearMap29 injective := C.injective30 surjective := C.surjective31 image_closedUnitBall := hball32 seminorm_linearMap_eq := fun x => SeminormBall.map_eq MX.p MY.p33 (fun _ h => MX.eq_zero_of_apply_eq_zero h)34 (fun _ h => MY.eq_zero_of_apply_eq_zero h) C.linearMap.toLinearMap35 ⟨C.injective, C.surjective⟩ hball x }⟩36end PluckerRecovery.Internal3738namespace EquivalentSeminorm39/-- Equality of all finite Plücker bodies gives an equivalence preserving the stored norms. -/40theorem nonempty_linearIsometryEquiv_of_pluckerBodies_eq {m : ℕ}41 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))42 (hBodies : ∀ N : ℕ, PluckerBody.body MX N = PluckerBody.body MY N) :43 Nonempty (LinearIsometryEquiv MX MY) := by44 let C := Classical.choice (PluckerRecovery.Internal.nonempty_coordinateLinearIsometry_of_all_body_eq MX MY hBodies)45 let e : (Fin (m + 1) → ℝ) ≃ₗ[ℝ] (Fin (m + 1) → ℝ) :=46 LinearEquiv.ofBijective C.linearMap.toLinearMap ⟨C.injective, C.surjective⟩47 exact ⟨{ toLinearEquiv := e, map_p_eq := fun x => by simpa [e] using C.seminorm_linearMap_eq x }⟩4849/-- Sphere isometry supplies the exact B3 body equality used by recovery. -/50theorem nonempty_linearIsometryEquiv_of_sphereIsometryEquiv {m : ℕ}51 (MX MY : EquivalentSeminorm (Fin (m + 1) → ℝ))52 (Δ : Metric.sphere (0 : Space MX) 1 ≃ᵢ Metric.sphere (0 : Space MY) 1) :53 Nonempty (LinearIsometryEquiv MX MY) := by54 apply nonempty_linearIsometryEquiv_of_pluckerBodies_eq MX MY55 intro N56 exact PluckerBody.eq_of_sphereIsometry Δ57end EquivalentSeminorm58end MathlibAnnex