# HG changeset patch # User Manuel Eberl # Date 1748956734 -7200 # Node ID a6cfe84d0dddd627ea7c7cecfd366a67c49ca81c # Parent 71304514891e1587e19f431e2e722e639841de8a HOL: minor additions regarding linear algebra diff -r 71304514891e -r a6cfe84d0ddd src/HOL/Analysis/Linear_Algebra.thy --- 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 \ span Basis" unfolding span_Basis .. +lemma representation_euclidean_space: + "representation Basis x = (\b. if b \ Basis then inner x b else 0)" +proof (rule representation_eqI) + have "(\b | (if b \ Basis then inner x b else 0) \ 0. (if b \ Basis then inner x b else 0) *\<^sub>R b) = + (\b\Basis. inner x b *\<^sub>R b)" + by (intro sum.mono_neutral_cong_left) auto + also have "\ = x" + by (simp add: euclidean_representation) + finally show "(\b | (if b \ Basis then inner x b else 0) \ 0. + (if b \ Basis then inner x b else 0) *\<^sub>R b) = x" . +qed (insert independent_Basis span_Basis, auto split: if_splits) + subsection\<^marker>\tag unimportant\ \Linearity and Bilinearity continued\ diff -r 71304514891e -r a6cfe84d0ddd src/HOL/Library/Disjoint_Sets.thy --- 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 \ (\r. equiv A r \ 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 (\B. F g B) A" +proof - + have "finite A" + using assms finite_UnionD partition_onD1 by auto + have [intro]: "finite B" if "B \ A" for B + by (rule finite_subset[OF _ assms(1)]) + (use assms that in \auto simp: partition_on_def\) + have "F g X = F g (\A)" + using assms by (simp add: partition_on_def) + also have "\ = (F \ F) g A" + by (rule Union_disjoint) (use assms \finite A\ in \auto simp: partition_on_def disjoint_def\) + finally show ?thesis + by simp +qed + + +text \ + 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)\}$. +\ +lemma sum_involution_eq_0: + assumes f_h: "\x. x \ X \ f (h x) + f x = 0" + assumes h: "\x. x \ X \ h x \ X" "\x. x \ X \ h (h x) = x" "\x. x \ X \ h x \ x" + shows "(\x\X. f x) = 0" +proof (cases "finite X") + assume fin: "finite X" + define R where "R = {(x,y). x \ X \ y \ X \ (x = y \ 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 "(\x\X. f x) = (\B\A. \x\B. f x)" + by (subst sum.partition[OF fin partition]) auto + also have "\ = (\B\A. 0)" + proof (rule sum.cong) + fix B assume B: "B \ A" + then obtain x where x: "x \ X" and [simp]: "B = R `` {x}" + using R by (metis A_def quotientE) + have "R `` {x} = {x, h x}" "h x \ x" + using h x(1) by (auto simp: R_def) + thus "(\x\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 \Refinement of partitions\ definition refines :: "'a set \ 'a set set \ 'a set set \ bool" diff -r 71304514891e -r a6cfe84d0ddd src/HOL/Vector_Spaces.thy --- 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 "\g. linear s1 s2 g \ bij g \ 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 \card B = card B'\ 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' \ 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 "\g. linear s1 s2 g \ bij g \ 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 "\g. linear scale scale g \ inj g \ (\x\B. g x = f x)" +proof - + obtain B' where B': "span B' = UNIV" "B \ 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 \ 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 \inj_on f B\]) + hence "\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 = (\v. \b\B'. scale (r v b) (if b \ 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 \ B" for b + proof - + from that have "g b = (\b'\{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 \ B' - B" for b + proof - + from that have "g b = (\b'\{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'' \ range g" + proof + fix b assume b: "b \ B''" + thus "b \ range g" + proof (cases "b \ f ` B") + case True + then obtain b' where b': "b' \ 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 \ B'' - f ` B" + by blast + then obtain b' where "h b' = b" "b' \ 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'' \ 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