Skip to content

Commit

Permalink
Try to prove norm_map'
Browse files Browse the repository at this point in the history
  • Loading branch information
MetalCreator666 committed Dec 20, 2024
1 parent 334fbe5 commit c6b2989
Show file tree
Hide file tree
Showing 3 changed files with 7 additions and 4 deletions.
4 changes: 2 additions & 2 deletions DeRhamCohomology/Alternating/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ variable

def _root_.LinearIsometryEquiv.flipAlternating :
(M' →L[𝕜] (M [⋀^ι]→L[𝕜] N)) ≃ₗᵢ[𝕜] (M [⋀^ι]→L[𝕜] (M' →L[𝕜] N)) where
toFun f := ContinuousLinearMap.flipAlternating f
invFun := sorry
toFun := ContinuousLinearMap.flipAlternating
invFun f := sorry
map_add' _ _ := rfl
map_smul' _ _ := rfl
left_inv := sorry
Expand Down
2 changes: 1 addition & 1 deletion DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ theorem uncurryFin_uncurryFinCLM_comp_of_symmetric {f : E →L[𝕜] E →L[𝕜
Fin.succAbove_succAbove_predAbove, Fin.neg_one_pow_succAbove_add_predAbove, pow_succ',
neg_one_mul, neg_smul, Fin.removeNth_apply, add_neg_cancel]

def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι ⊕ ι']→L[𝕜] F := by sorry
def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι ⊕ ι']→L[𝕜] F := sorry

def uncurryFinAdd (f : E [⋀^Fin m]→L[𝕜] E [⋀^Fin n]→L[𝕜] F) : E [⋀^Fin (m + n)]→L[𝕜] F := by sorry

Expand Down
5 changes: 4 additions & 1 deletion DeRhamCohomology/Multilinear/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -68,4 +68,7 @@ def LinearIsometryEquiv.flipMultilinear :
map_smul' _ _ := rfl
left_inv := congrFun rfl
right_inv := congrFun rfl
norm_map' := fun x => by sorry -- TODO
norm_map' := fun f => by
simp
simp_rw[ContinuousLinearMap.flipMultilinear, MultilinearMap.mkContinuous, LinearMap.mkContinuous]
sorry

0 comments on commit c6b2989

Please sign in to comment.