Theory Cotangent_Space
section ‹Cotangent Space›
theory Cotangent_Space
imports Tangent_Space
begin
subsection ‹Dual of a vector space›
abbreviation "linear_fun_on S ≡ linear_on S (UNIV::real set) scaleR scaleR"
definition dual_space :: "'a::real_vector set ⇒ ('a ⇒ real) set" where
"dual_space S = {E. linear_fun_on S E ∧ extensional0 S E}"
lemma dual_space_eq:
"dual_space S = {E. linear_fun_on S E} ∩ {E. extensional0 S E}"
by (auto simp: dual_space_def)
lemma mem_dual_space:
"E ∈ dual_space S ⟷ linear_fun_on S E ∧ extensional0 S E"
by (auto simp: dual_space_def)
lemma dual_spaceI:
"E ∈ dual_space S"
if "extensional0 S E" "linear_fun_on S E"
using that
by (auto simp: dual_space_def)
lemma dual_spaceD:
assumes "E ∈ dual_space S"
shows dual_space_linear_on: "linear_fun_on S E"
and dual_space_restrict[simp]: "extensional0 S E"
using assms by (auto simp: dual_space_def)
lemma linear_fun_on_zero:
"linear_fun_on S 0"
if "subspace S"
by (unfold_locales, auto simp add: algebra_simps that[unfolded subspace_def])
lemma "linear_fun_on S x ⟹ a ∈ S ⟹ b ∈ S ⟹ x (a + b) = x a + x b"
using linear_on.axioms module_hom_on.add by blast
lemma linear_fun_on_add:
"linear_fun_on S (x + y)"
if x: "linear_fun_on S x" and y: "linear_fun_on S y" and S: "subspace S"
using x that
by (unfold_locales, auto dest!: linear_on.axioms
simp add: algebra_simps module_hom_on.add module_hom_on.scale subspace_def)
lemma linear_fun_on_scaleR:
"linear_fun_on S (c *⇩R x)"
if x: "linear_fun_on S x" and S: "subspace S"
using x that
by (unfold_locales, auto dest!: linear_on.axioms
simp add: module_hom_on.add module_hom_on.scale algebra_simps subspace_def)
lemma subspace_linear_fun_on:
"subspace {E. linear_fun_on S E}"
if "subspace S"
by (auto simp: subspace_def linear_fun_on_zero[OF that]
linear_fun_on_add[OF _ _ that] linear_fun_on_scaleR[OF _ that])
lemma subspace_dual_space:
"subspace (dual_space S)"
if "subspace S"
unfolding dual_space_eq
apply (rule subspace_inter)
apply (rule subspace_linear_fun_on[OF that])
apply (rule subspace_extensional0)
done
subsection ‹Dimension of dual space›
text ‹Mapping from S to the dual of S›
context fixes B S assumes B: "independent B" "span B = S"
begin
definition "inner_Basis a b = (∑i∈B. representation B a i * representation B b i)"
definition std_dual :: "'a::real_vector ⇒ ('a ⇒ real)" where
"std_dual a = restrict0 S (restrict0 S (λb. inner_Basis a b))"
lemma inner_Basis_add:
"b1 ∈ S ⟹ b2 ∈ S ⟹ inner_Basis (b1 + b2) v = inner_Basis b1 v + inner_Basis b2 v"
by (auto simp: std_dual_def restrict0_def algebra_simps representation_add representation_scale
B inner_Basis_def
sum.distrib sum_distrib_left)
lemma inner_Basis_add2:
"b1 ∈ S ⟹ b2 ∈ S ⟹ inner_Basis v (b1 + b2) = inner_Basis v b1 + inner_Basis v b2"
by (auto simp: std_dual_def restrict0_def algebra_simps representation_add representation_scale
B inner_Basis_def
sum.distrib sum_distrib_left)
lemma inner_Basis_scale:
"b1 ∈ S ⟹ inner_Basis (c *⇩R b1) v = c * inner_Basis b1 v"
by (auto simp: std_dual_def restrict0_def algebra_simps representation_add representation_scale
B inner_Basis_def sum.distrib sum_distrib_left)
lemma inner_Basis_scale2:
"b1 ∈ S ⟹ inner_Basis v (c *⇩R b1) = c * inner_Basis v b1"
by (auto simp: std_dual_def restrict0_def algebra_simps representation_add representation_scale
B inner_Basis_def sum.distrib sum_distrib_left)
lemma inner_Basis_minus:
"b1 ∈ S ⟹ b2 ∈ S ⟹ inner_Basis (b1 - b2) v = inner_Basis b1 v - inner_Basis b2 v"
and inner_Basis_minus2:
"b1 ∈ S ⟹ b2 ∈ S ⟹ inner_Basis v (b1 - b2) = inner_Basis v b1 - inner_Basis v b2"
by (auto simp: std_dual_def restrict0_def algebra_simps representation_diff representation_scale
B inner_Basis_def
sum_subtractf sum_distrib_left)
lemma sum_zero_representation:
"v = 0"
if "⋀b. b ∈ B ⟹ representation B v b = 0" and v: "v ∈ S"
proof -
have empty: "{b. representation B v b ≠ 0} = {}"
using that(1) representation_ne_zero by auto
have "v ∈ span B" using B v by simp
from sum_nonzero_representation_eq[OF B(1) this]
show ?thesis
by (simp add: empty)
qed
lemma inner_Basis_0[simp]: "inner_Basis 0 a = 0" "inner_Basis a 0 = 0"
by (auto simp: inner_Basis_def representation_zero)
lemma inner_Basis_eq_zeroI: "a = 0" if "inner_Basis a a = 0"
and "finite B" "a ∈ S"
by (rule sum_zero_representation)
(use that in ‹auto simp: inner_Basis_def that sum_nonneg_eq_0_iff›)
lemma inner_Basis_zero: "inner_Basis a a = 0 ⟷ a = 0"
if "finite B" "a ∈ S"
by (auto simp: inner_Basis_eq_zeroI that)
lemma subspace_S: "subspace S"
using B by auto
interpretation S: real_vector_space_on S
using subspace_S
by unfold_locales
interpretation dual: real_vector_space_on "dual_space S"
using subspace_dual_space[OF subspace_S]
by unfold_locales
lemma std_dual_linear:
"linear_on S (dual_space S) scaleR scaleR std_dual"
by unfold_locales
(auto simp add: subspace_S[unfolded subspace_def] subspace_dual_space[unfolded subspace_def] algebra_simps
std_dual_def inner_Basis_scale inner_Basis_add restrict0_def)
lemma image_std_dual:
"std_dual ` S ⊆ dual_space S"
if "subspace S"
proof safe
fix y assume "y ∈ S"
show "std_dual y ∈ dual_space S"
proof (rule dual_spaceI)
show "extensional0 S (std_dual y)"
by (auto simp: std_dual_def)
show "linear_fun_on S (std_dual y)"
by (unfold_locales, auto simp: std_dual_def algebra_simps that[unfolded subspace_def]
inner_Basis_add2 inner_Basis_scale2 B)
qed
qed
lemma inj_std_dual:
"inj_on std_dual S"
if "subspace S" "finite B"
proof (intro inj_onI)
fix x y assume x: "x ∈ S" and y: "y ∈ S" and eq: "std_dual x = std_dual y"
have 1: "inner_Basis x b = inner_Basis y b" if b: "b ∈ S" for b
proof -
have "std_dual x b = inner_Basis x b" "std_dual y b = inner_Basis y b"
unfolding std_dual_def restrict0_def
using b by auto
then show ?thesis using eq by auto
qed
have 2: "x - y ∈ S" using that(1) x y by (rule subspace_diff)
have "inner_Basis x (x - y) - inner_Basis y (x - y) = 0" using 1 2 by auto
then have "inner_Basis (x - y) (x - y) = 0"
by (auto simp: inner_Basis_minus inner_Basis_minus2 2 B x y algebra_simps)
then show "x = y"
by (auto simp: inner_Basis_zero B that 2)
qed
lemma inner_Basis_sum:
"(⋀i. i ∈ I ⟹ x i ∈ S) ⟹ inner_Basis (∑i∈I. x i) v = (∑i∈I. inner_Basis (x i) v)"
apply (induction I rule: infinite_finite_induct)
apply auto
apply (subst inner_Basis_add)
apply auto
by (metis B(2) subspace_span subspace_sum)
lemma inner_Basis_sum2:
"(⋀i. i ∈ I ⟹ x i ∈ S) ⟹ inner_Basis v (∑i∈I. x i) = (∑i∈I. inner_Basis v (x i))"
apply (induction I rule: infinite_finite_induct)
apply auto
apply (subst inner_Basis_add2)
apply auto
by (metis B(2) subspace_span subspace_sum)
lemma B_sub_S: "B ⊆ S"
using B(2) span_eq by auto
lemma inner_Basis_eq_representation:
"inner_Basis i x = representation B x i"
if "i ∈ B" "finite B"
unfolding inner_Basis_def
by (simp add: B that representation_basis if_distrib if_distribR cong: if_cong)
lemma surj_std_dual:
"std_dual ` S ⊇ dual_space S" if "subspace S" "finite B"
proof safe
fix y
assume y: "y ∈ dual_space S"
show "y ∈ std_dual ` S"
proof -
let ?x = "∑i∈B. (y i) *⇩R i"
have x: "?x ∈ S"
using that(1) apply (rule subspace_sum) using that(1) apply (rule subspace_scale)
using B span_superset
by auto
from dual_space_linear_on[OF y]
have linear_y: "linear_fun_on S y" .
then interpret linear_on S UNIV scaleR scaleR y .
interpret vector_space_pair_on S "UNIV::real set" scaleR scaleR by unfold_locales
have "y = std_dual ?x"
apply (rule ext_extensional0[of S])
subgoal using y dual_space_def by auto
subgoal by (auto simp: std_dual_def)
unfolding std_dual_def restrict0_def apply auto
apply (subst inner_Basis_sum) subgoal
using B(2) span_base subspace_scale by blast
subgoal for x
proof goal_cases
case 1
have "(∑i∈B. inner_Basis (y i *⇩R i) x) = (∑i∈B. y (inner_Basis i x *⇩R i))"
proof (rule sum.cong[OF refl])
fix i assume i: "i ∈ B"
then have "i : S" using B_sub_S by auto
have "inner_Basis (y i *⇩R i) x = y i * inner_Basis i x"
apply (subst inner_Basis_scale)
subgoal using B_sub_S i by auto
apply (rule refl)
done
also have "… = y i *⇩R inner_Basis i x" by simp
also have "… = y (inner_Basis i x *⇩R i)"
by (auto simp: ‹i ∈ S› scale)
finally show "inner_Basis (y i *⇩R i) x = y (inner_Basis i x *⇩R i)" .
qed
also have "… = y (∑i∈B. (inner_Basis i x *⇩R i))" (is "_ = y ?sum")
apply (subst linear_sum'[OF _ _ linear_y])
apply (auto simp: inner_Basis_eq_representation)
using B(2) S.mem_scale span_base by blast
also have "?sum = x"
apply (subst sum.cong[OF refl])
apply (subst inner_Basis_eq_representation, assumption, rule that, rule refl)
apply (subst sum_representation_eq)
by (auto simp: that B ‹x : S›)
finally show ?thesis by simp
qed
done
then show ?thesis
using x by auto
qed
qed
lemma std_dual_bij_betw:
"bij_betw (std_dual) S (dual_space S)"
if "finite B"
unfolding bij_betw_def
using subspace_S inj_std_dual image_std_dual surj_std_dual that by blast
lemma std_dual_eq_dual_space: "finite B ⟹ std_dual ` S = dual_space S"
using image_std_dual surj_std_dual subspace_S by auto
lemma dim_dual_space:
assumes "finite B"
shows "dim (dual_space S) = dim S"
proof -
interpret finite_dimensional_real_vector_space_pair_1_on S "dual_space S" B
using B assms span_superset
by unfold_locales auto
have *: "span S = S" using subspace_S by auto
then have "dual.dim (std_dual ` S) = S.dim S"
apply (intro dim_image_eq[OF _ order_refl std_dual_linear])
using std_dual_bij_betw[OF assms]
by (auto simp: bij_betw_def *)
also have "S.dim S = dim S"
unfolding S.dim_eq[OF order_refl] ..
also have "dual.dim (std_dual ` S) = dim (std_dual ` S)"
using image_std_dual[OF subspace_S]
by (rule dual.dim_eq)
also have "std_dual ` S = dual_space S"
using assms
by (rule std_dual_eq_dual_space)
finally show ?thesis .
qed
end
subsection ‹Dual map›
context real_vector_space_pair_on begin
definition dual_map :: "('a ⇒ 'b) ⇒ ('b ⇒ real) ⇒ ('a ⇒ real)" where
"dual_map f y = restrict0 S (λx. y (f x))"
lemma subspace_dual_S: "subspace (dual_space S)"
apply (rule subspace_dual_space)
apply (rule local.vs1.subspace)
done
lemma subspace_dual_T: "subspace (dual_space T)"
apply (rule subspace_dual_space)
apply (rule local.vs2.subspace)
done
lemma dual_map_linear:
"linear_on (dual_space T) (dual_space S) scaleR scaleR (dual_map f)"
apply unfold_locales
by (auto simp add: dual_map_def restrict0_def subspace_dual_S[unfolded subspace_def]
subspace_dual_T[unfolded subspace_def] algebra_simps)
lemma image_dual_map:
"dual_map f ` (dual_space T) ⊆ dual_space S"
if f: "linear_on S T scaleR scaleR f" and
defined: "f ` S ⊆ T"
proof safe
fix x assume x: "x ∈ dual_space T"
show "dual_map f x ∈ dual_space S"
proof (rule dual_spaceI)
have 1: "linear_fun_on T x"
using x by (rule dual_space_linear_on)
show "extensional0 S (dual_map f x)" by (auto simp: dual_map_def)
show "linear_fun_on S (dual_map f x)"
apply (unfold_locales, auto simp: dual_map_def restrict0_def linear_on_def algebra_simps
local.vs1.subspace[unfolded subspace_def])
proof -
show "x (f (b1 + b2)) = x (f b1) + x (f b2)" if "b1 ∈ S" "b2 ∈ S" for b1 b2
proof -
have "f b1 ∈ T" using ‹b1 ∈ S› defined by auto
have "f b2 ∈ T" using ‹b2 ∈ S› defined by auto
have "x (f (b1 + b2)) = x (f b1 + f b2)"
by (auto simp: f[THEN linear_on.axioms, THEN module_hom_on.add] that)
also have "x (f b1 + f b2) = x (f b1) + x (f b2)"
by (auto simp: 1[THEN linear_on.axioms, THEN module_hom_on.add] ‹f b1 ∈ T› ‹f b2 ∈ T›)
finally show ?thesis .
qed
show "x (f (r *⇩R b)) = r * x (f b)" if "b ∈ S" for r b
proof -
have "f b ∈ T" using ‹b ∈ S› defined by auto
have "x (f (r *⇩R b)) = x (r *⇩R f b)"
by (auto simp: f[THEN linear_on.axioms, THEN module_hom_on.scale] that)
also have "x (r *⇩R f b) = r * x (f b)"
by (auto simp: 1[THEN linear_on.axioms, THEN module_hom_on.scale] ‹f b ∈ T›)
finally show ?thesis .
qed
qed
qed
qed
end
text ‹Functoriality of dual map: identity›
context real_vector_space_on begin
lemma dual_map_id:
"real_vector_space_pair_on.dual_map S f y = y"
if f: "⋀x. x ∈ S ⟹ f x = x" and y: "y ∈ dual_space S"
proof (rule ext_extensional0[of S])
have 1: "real_vector_space_pair_on S S" ..
show "extensional0 S (real_vector_space_pair_on.dual_map S f y)"
unfolding real_vector_space_pair_on.dual_map_def[OF 1] by auto
show "extensional0 S y"
using y by auto
fix x assume x: "x ∈ S"
show "real_vector_space_pair_on.dual_map S f y x = y x"
proof -
have "real_vector_space_pair_on.dual_map S f y x = y (f x)"
by (auto simp: real_vector_space_pair_on.dual_map_def[OF 1] restrict0_def x)
also have "y (f x) = y x"
using f x by auto
finally show ?thesis .
qed
qed
end
abbreviation "dual_map ≡ real_vector_space_pair_on.dual_map"
lemmas dual_map_def = real_vector_space_pair_on.dual_map_def
text ‹Functoriality of dual map: composition›
lemma dual_map_compose:
"dual_map S f (dual_map T g x) = dual_map S (g ∘ f) x"
if "x ∈ dual_space U" and "linear_on T U scaleR scaleR g"
and f: "linear_on S T scaleR scaleR f"
and defined: "f ` S ⊆ T"
and ST: "real_vector_space_pair_on S T"
and TU: "real_vector_space_pair_on T U"
proof (rule ext)
have SU: "real_vector_space_pair_on S U"
using ST TU by (auto simp add: real_vector_space_pair_on_def)
fix v show "dual_map S f (dual_map T g x) v = dual_map S (g ∘ f) x v"
unfolding dual_map_def[OF ST] dual_map_def[OF TU] dual_map_def[OF SU] restrict0_def
using defined by auto
qed
subsection ‹Definition of cotangent space›
context c_manifold begin
definition cotangent_space :: "'a ⇒ ((('a ⇒ real) ⇒ real) ⇒ real) set" where
"cotangent_space p = dual_space (tangent_space p)"
lemma subspace_cotangent_space:
"subspace (cotangent_space p)"
unfolding cotangent_space_def
apply (rule subspace_dual_space)
apply (rule subspace_tangent_space)
done