--- a/src/HOL/Analysis/Linear_Algebra.thy Tue Jun 03 12:22:58 2025 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue Jun 03 15:18:54 2025 +0200
@@ -426,6 +426,18 @@
lemma in_span_Basis: "x \<in> span Basis"
unfolding span_Basis ..
+lemma representation_euclidean_space:
+ "representation Basis x = (\<lambda>b. if b \<in> Basis then inner x b else 0)"
+proof (rule representation_eqI)
+ have "(\<Sum>b | (if b \<in> Basis then inner x b else 0) \<noteq> 0. (if b \<in> Basis then inner x b else 0) *\<^sub>R b) =
+ (\<Sum>b\<in>Basis. inner x b *\<^sub>R b)"
+ by (intro sum.mono_neutral_cong_left) auto
+ also have "\<dots> = x"
+ by (simp add: euclidean_representation)
+ finally show "(\<Sum>b | (if b \<in> Basis then inner x b else 0) \<noteq> 0.
+ (if b \<in> Basis then inner x b else 0) *\<^sub>R b) = x" .
+qed (insert independent_Basis span_Basis, auto split: if_splits)
+
subsection\<^marker>\<open>tag unimportant\<close> \<open>Linearity and Bilinearity continued\<close>
--- a/src/HOL/Library/Disjoint_Sets.thy Tue Jun 03 12:22:58 2025 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Tue Jun 03 15:18:54 2025 +0200
@@ -450,6 +450,67 @@
lemma partition_on_alt: "partition_on A P \<longleftrightarrow> (\<exists>r. equiv A r \<and> P = A // r)"
by (auto simp: partition_on_eq_quotient intro!: partition_on_quotient intro: equiv_partition_on)
+lemma (in comm_monoid_set) partition:
+ assumes "finite X" "partition_on X A"
+ shows "F g X = F (\<lambda>B. F g B) A"
+proof -
+ have "finite A"
+ using assms finite_UnionD partition_onD1 by auto
+ have [intro]: "finite B" if "B \<in> A" for B
+ by (rule finite_subset[OF _ assms(1)])
+ (use assms that in \<open>auto simp: partition_on_def\<close>)
+ have "F g X = F g (\<Union>A)"
+ using assms by (simp add: partition_on_def)
+ also have "\<dots> = (F \<circ> F) g A"
+ by (rule Union_disjoint) (use assms \<open>finite A\<close> in \<open>auto simp: partition_on_def disjoint_def\<close>)
+ finally show ?thesis
+ by simp
+qed
+
+
+text \<open>
+ If $h$ is an involution on $X$ with no fixed points in $X$ and
+ $f(h(x)) = -f(x)$ then $\sum_{x\in X} f(x) = 0$.
+
+ This is easy to show in a ring with characteristic not equal to $2", since then we can do
+ \[\sum_{x\in X} f(x) = \sum_{x\in X} f(h(x)) = -\sum_{x\in X} f(x)\]
+ and therefore $2 \sum_{x\in X} f(x) = 0$.
+
+ However, the following proof also works in rings of characteristic 2.
+ The idea is to simply partition $X$ into a disjoint union of doubleton sets of the form
+ $\{x, h(x)\}$.
+\<close>
+lemma sum_involution_eq_0:
+ assumes f_h: "\<And>x. x \<in> X \<Longrightarrow> f (h x) + f x = 0"
+ assumes h: "\<And>x. x \<in> X \<Longrightarrow> h x \<in> X" "\<And>x. x \<in> X \<Longrightarrow> h (h x) = x" "\<And>x. x \<in> X \<Longrightarrow> h x \<noteq> x"
+ shows "(\<Sum>x\<in>X. f x) = 0"
+proof (cases "finite X")
+ assume fin: "finite X"
+ define R where "R = {(x,y). x \<in> X \<and> y \<in> X \<and> (x = y \<or> h x = y)}"
+ have R: "equiv X R"
+ unfolding equiv_def R_def using h(2,3)
+ by (auto simp: refl_on_def sym_def trans_def)
+ define A where "A = X // R"
+ have partition: "partition_on X A"
+ unfolding A_def using R by (rule partition_on_quotient)
+
+ have "(\<Sum>x\<in>X. f x) = (\<Sum>B\<in>A. \<Sum>x\<in>B. f x)"
+ by (subst sum.partition[OF fin partition]) auto
+ also have "\<dots> = (\<Sum>B\<in>A. 0)"
+ proof (rule sum.cong)
+ fix B assume B: "B \<in> A"
+ then obtain x where x: "x \<in> X" and [simp]: "B = R `` {x}"
+ using R by (metis A_def quotientE)
+ have "R `` {x} = {x, h x}" "h x \<noteq> x"
+ using h x(1) by (auto simp: R_def)
+ thus "(\<Sum>x\<in>B. f x) = 0"
+ using x f_h[of x] by (simp add: add.commute)
+ qed auto
+ finally show ?thesis
+ by simp
+qed auto
+
+
subsection \<open>Refinement of partitions\<close>
definition refines :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set \<Rightarrow> bool"
--- a/src/HOL/Vector_Spaces.thy Tue Jun 03 12:22:58 2025 +0200
+++ b/src/HOL/Vector_Spaces.thy Tue Jun 03 15:18:54 2025 +0200
@@ -1516,6 +1516,42 @@
from finite_basis_to_basis_subspace_isomorphism[OF s t d fB B fC C] show ?thesis .
qed
+lemma basis_change_exists':
+ assumes "vs1.independent B" "vs2.independent B'"
+ assumes "vs1.span B = UNIV" "vs2.span B' = UNIV" "vs1.dimension = vs2.dimension"
+ shows "\<exists>g. linear s1 s2 g \<and> bij g \<and> bij_betw g B B'"
+proof -
+ have "finite B" "finite B'"
+ using assms by (auto intro: vs1.finiteI_independent vs2.finiteI_independent)
+ moreover from assms have "card B = card B'"
+ by (metis vs1.dim_span vs2.dim_span vs1.dim_UNIV vs2.dim_UNIV vs1.dimension_def vs2.dimension_def
+ vs1.dim_eq_card_independent vs2.dim_eq_card_independent)
+ ultimately obtain h where h: "bij_betw h B B'"
+ using \<open>card B = card B'\<close> by (meson bij_betw_iff_card)
+
+ define g where "g = construct B h"
+ interpret g: Vector_Spaces.linear s1 s2 g
+ unfolding g_def by (rule linear_construct) fact
+
+ have "bij_betw g B B' \<longleftrightarrow> bij_betw h B B'"
+ using assms(1) by (intro bij_betw_cong) (auto simp: g_def construct_basis)
+ hence "bij_betw g B B'"
+ using h by simp
+ moreover from this have "bij g"
+ using assms(3-5)
+ by (metis bij_betw_imp_surj_on bij_def g.linear_axioms local.linear_span_image
+ local.linear_surjective_imp_injective vs1.dim_UNIV vs1.dimension_def
+ vs2.dim_UNIV vs2.dimension_def)
+ ultimately show ?thesis
+ using g.linear_axioms by blast
+qed
+
+lemma basis_change_exists:
+ assumes "vs1.dimension = vs2.dimension"
+ shows "\<exists>g. linear s1 s2 g \<and> bij g \<and> bij_betw g B1 B2"
+ using basis_change_exists'[OF vs1.independent_Basis vs2.independent_Basis
+ vs1.span_Basis vs2.span_Basis assms] .
+
end
context finite_dimensional_vector_space begin
@@ -1612,6 +1648,83 @@
with h(1) show ?thesis by blast
qed
+lemma linear_independent_extend_inj:
+ assumes "independent B" "independent (f ` B)" "inj_on f B"
+ shows "\<exists>g. linear scale scale g \<and> inj g \<and> (\<forall>x\<in>B. g x = f x)"
+proof -
+ obtain B' where B': "span B' = UNIV" "B \<subseteq> B'" "independent B'"
+ using assms(1) by (meson extend_basis_superset independent_extend_basis span_extend_basis)
+ obtain B'' where B'': "span B'' = UNIV" "f ` B \<subseteq> B''" "independent B''"
+ using assms(2) by (meson extend_basis_superset independent_extend_basis span_extend_basis)
+ have "card B' = card B''"
+ using B' B'' by (metis local.dim_eq_card)
+ hence "card (B' - B) = card (B'' - f ` B)"
+ using finiteI_independent[OF assms(1)] B' B''
+ by (subst (1 2) card_Diff_subset) (auto simp: card_image[OF \<open>inj_on f B\<close>])
+ hence "\<exists>h. bij_betw h (B' - B) (B'' - f ` B)"
+ using finiteI_independent[of B'] finiteI_independent[of B''] B' B''
+ by (intro finite_same_card_bij) auto
+ then obtain h where h: "bij_betw h (B' - B) (B'' - f ` B)"
+ by blast
+
+ have [simp, intro]: "finite B'"
+ using finiteI_independent[of B'] B' by auto
+ define r where "r = representation B'"
+ define g where "g = (\<lambda>v. \<Sum>b\<in>B'. scale (r v b) (if b \<in> B then f b else h b))"
+ interpret pair: vector_space_pair scale scale ..
+ interpret g: Vector_Spaces.linear scale scale g
+ unfolding g_def r_def
+ by (intro pair.module_hom_sum pair.linear_compose_scale linear_representation B' conjI module_axioms)
+
+ have g_B: "g b = f b" if "b \<in> B" for b
+ proof -
+ from that have "g b = (\<Sum>b'\<in>{b}. f b)"
+ unfolding g_def using B'
+ by (intro sum.mono_neutral_cong_right) (auto simp: r_def representation_basis)
+ thus "g b = f b"
+ by simp
+ qed
+
+ have g_not_B: "g b = h b" if "b \<in> B' - B" for b
+ proof -
+ from that have "g b = (\<Sum>b'\<in>{b}. h b)"
+ unfolding g_def using B'
+ by (intro sum.mono_neutral_cong_right) (auto simp: r_def representation_basis)
+ thus "g b = h b"
+ by simp
+ qed
+
+ show ?thesis
+ proof (rule exI[of _ g]; safe)
+ have "B'' \<subseteq> range g"
+ proof
+ fix b assume b: "b \<in> B''"
+ thus "b \<in> range g"
+ proof (cases "b \<in> f ` B")
+ case True
+ then obtain b' where b': "b' \<in> B" "f b' = b"
+ by blast
+ thus ?thesis
+ by (auto simp: image_def g_B intro!: exI[of _ b'])
+ next
+ case False
+ with b have "b \<in> B'' - f ` B"
+ by blast
+ then obtain b' where "h b' = b" "b' \<in> B' - B"
+ using h by (metis bij_betw_iff_bijections)
+ thus ?thesis
+ by (intro rev_image_eqI[of b']) (simp_all add: g_not_B)
+ qed
+ qed
+ hence "span B'' \<le> span (range g)"
+ by (intro span_mono)
+ also have "span B'' = UNIV"
+ using B'' by simp
+ finally show "inj g"
+ by (simp add: g.linear_axioms g.span_image local.linear_surj_imp_inj set_eq_subset)
+ qed (use g_B g.linear_axioms in auto)
+qed
+
end
context finite_dimensional_vector_space_pair begin