Theory Vector_Space

section ‹Finite-dimensional vector spaces over a field›

theory Vector_Space
  imports Free_Module
begin

text ‹The import of ‹FiniteProduct› (through ‹Module›) re-merges HOL's @{text "+"}/@{text "-"} concrete
  syntax alongside the ring locale's, which is harmless in term positions (type inference disambiguates)
  but ambiguous in a locale-header instantiation argument.›
no_notation plus (infixl ‹+› 65)
no_notation minus (infixl ‹-› 65)
unbundle no uminus_syntax

text ‹A vector space over the field @{term R} (with field operations @{text "+, ⋅, 𝟬, 𝟭"}):
  an abelian group of vectors @{term V} under @{text "⊕"} with zero @{text "𝟬⇩_V"}, together with a
  scalar multiplication @{text "⊙"} satisfying the module axioms.  The purpose of this layer is the
  structural theorem that a finite field has prime-power order: such a field is a
  finite-dimensional vector space over its prime subfield, so its cardinality is
  @{text "¦F¦⇗^dim⇖"}.›

locale Vector_Space = Field +
  fixes vadd :: "'b ⇒ 'b ⇒ 'b" (infixl ‹⊕› 65)
    and vzero :: "'b" (‹𝟬⇩_V›)
    and vcarrier :: "'b set" (‹V›)
    and scale :: "'a ⇒ 'b ⇒ 'b" (infixr ‹⊙› 75)
  assumes vadd_group: "Abelian_Group V (⊕) 𝟬⇩_V"
    and scale_closed: "⟦ a ∈ R; v ∈ V ⟧ ⟹ a ⊙ v ∈ V"
    and scale_distrib_vadd: "⟦ a ∈ R; u ∈ V; v ∈ V ⟧ ⟹ a ⊙ (u ⊕ v) = (a ⊙ u) ⊕ (a ⊙ v)"
    and scale_distrib_add: "⟦ a ∈ R; b ∈ R; v ∈ V ⟧ ⟹ (a + b) ⊙ v = (a ⊙ v) ⊕ (b ⊙ v)"
    and scale_scale: "⟦ a ∈ R; b ∈ R; v ∈ V ⟧ ⟹ (a ⋅ b) ⊙ v = a ⊙ (b ⊙ v)"
    and scale_one: "v ∈ V ⟹ 𝟭 ⊙ v = v"
begin

text ‹The vector additive group, available through the @{text vadd} prefix.›
sublocale vadd: Abelian_Group V "(⊕)" "𝟬⇩_V"
  by (rule vadd_group)

text ‹Every vector space is a module (its scalar ring being a field is the additional constraint).
  This makes the module-level constructions --- ‹lincomb›, ‹span›, and the
  submodule/quotient machinery --- available inside the @{locale Vector_Space} locale under the
  ‹vadd›-prefixed operations.›
sublocale mod: Module R "(+)" "(⋅)" 𝟬 𝟭 "(⊕)" "𝟬⇩_V" V "(⊙)"
  by unfold_locales
     (auto simp: vadd_group scale_closed scale_distrib_vadd scale_distrib_add scale_scale scale_one)

text ‹Every submodule of a vector space is itself a vector space under the restricted carrier
  and the same operations.  This bridge lets the module-level kernel, image, and quotient
  constructions reuse the vector-space basis and dimension API.›

lemma submodule_vector_space:
  assumes N: "mod.submodule N"
  shows "Vector_Space R (+) (⋅) 𝟬 𝟭 (⊕) 𝟬⇩_V N (⊙)"
proof (intro Vector_Space.intro Vector_Space_axioms.intro)
  show "Field R (+) (⋅) 𝟬 𝟭" by unfold_locales
  have N_subgroup: "Subgroup N V (⊕) 𝟬⇩_V"
  proof (intro vadd.subgroupI mod.submodule_subset mod.submodule_zero mod.submodule_add mod.submodule_neg)
    fix v assume v: "v ∈ N"
    then show "vadd.invertible v"
      using N mod.submodule_def by auto
  qed (use N in auto)
  interpret Nadd: Subgroup N V "(⊕)" "𝟬⇩_V" by (rule N_subgroup)
  have comm: "u ⊕ v = v ⊕ u" if "u ∈ N" "v ∈ N" for u v
    using N that mod.submodule_subset vadd.commutative by blast
  show "Abelian_Group N (⊕) 𝟬⇩_V"
    by (simp add: Abelian_Group_def Nadd.sub.Group_axioms Nadd.sub.Monoid_axioms comm
        commutative_monoid.intro commutative_monoid_axioms.intro)
  show "⋀a v. ⟦a ∈ R; v ∈ N⟧ ⟹ a ⊙ v ∈ N"
    using N by (rule mod.submodule_scale)
  show "⋀a u v. ⟦a ∈ R; u ∈ N; v ∈ N⟧ ⟹
      a ⊙ (u ⊕ v) = (a ⊙ u) ⊕ (a ⊙ v)"
    using N mod.submodule_subset by (blast intro: scale_distrib_vadd)
  show "⋀v. v ∈ N ⟹ 𝟭 ⊙ v = v"
    using N mod.submodule_subset by (blast intro: scale_one)
  fix a b v
  assume "a ∈ R" "b ∈ R" "v ∈ N"
  then show "(a + b) ⊙ v = (a ⊙ v) ⊕ (b ⊙ v)" "(a ⋅ b) ⊙ v = a ⊙ (b ⊙ v)"
    using N mod.submodule_subset by (blast intro: scale_distrib_add scale_scale)+
qed

text ‹Basic closure and unit facts.›
lemma vzero_closed [simp, intro]: "𝟬⇩_V ∈ V" by simp

lemma vadd_closed [simp, intro]: "⟦ u ∈ V; v ∈ V ⟧ ⟹ u ⊕ v ∈ V"
  by simp

lemma scale_zero_vec:
  assumes "a ∈ R"
  shows "a ⊙ 𝟬⇩_V = 𝟬⇩_V"
proof -
  have w: "a ⊙ 𝟬⇩_V ∈ V" using assms by (simp add: scale_closed)
  then have "(a ⊙ 𝟬⇩_V) ⊕ 𝟬⇩_V = (a ⊙ 𝟬⇩_V) ⊕ (a ⊙ 𝟬⇩_V)"
    by (metis assms scale_distrib_vadd vadd.right_unit vzero_closed)
  then show ?thesis
    using vadd.invertible_left_cancel[OF vadd.invertible[OF w] w vzero_closed w] by simp
qed

text ‹∗‹Linear combinations and spans come from the module layer.›  The ‹mod› sublocale above
  already supplies ‹mod.lincomb› and ‹mod.span› on @{term V}, with definitions
  identical to the ones this theory used to repeat verbatim.  We introduce local abbreviations so
  existing proofs continue to read ‹lincomb› and ‹span› unqualified, and re-export the two facts
  those proofs cite by name.›
abbreviation lincomb :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'b"
  where "lincomb ≡ mod.lincomb"

abbreviation span :: "'b set ⇒ 'b set"
  where "span ≡ mod.span"

lemmas lincomb_def = mod.lincomb_def
lemmas span_def = mod.span_def

lemma lincomb_closed:
  assumes B: "B ⊆ V" and c: "⋀v. v ∈ B ⟹ c v ∈ R"
  shows "lincomb c B ∈ V"
  using B c by (rule mod.lincomb_closed)

text ‹∗‹Spanning and linear independence: the finite-dimensional forms.›  The module layer defines
  ‹mod.spanning› and ‹mod.lin_indep› for arbitrary subsets (see ‹Free_Module›).  This
  theory is about the finite-dimensional case --- its basis and dimension results count coordinate
  vectors --- so we keep ∗‹finite› variants phrased with a total coefficient function
  @{term "c ∈ B →⇩_E R"}, which is what the coordinate map needs, and relate them to the general
  notions by the bridging lemmas below.›
definition spanning :: "'b set ⇒ bool"
  where "spanning B ≡ finite B ∧ B ⊆ V ∧ (∀v∈V. ∃c∈B →⇩_E R. v = lincomb c B)"

definition lin_indep :: "'b set ⇒ bool"
  where "lin_indep B ≡ finite B ∧ B ⊆ V ∧ (∀c∈B →⇩_E R. lincomb c B = 𝟬⇩_V ⟶ (∀v∈B. c v = 𝟬))"

text ‹A set @{term B} is a ∗‹basis› of @{term V} when it is a finite subset whose coordinate map
  --- sending each coefficient vector @{term "c ∈ B →⇩_E R"} to the linear combination
  @{term "lincomb c B"} --- is a bijection onto @{term V}.  This packages spanning (surjectivity)
  and linear independence (injectivity) in exactly the form the cardinality count needs.›
definition basis :: "'b set ⇒ bool"
  where "basis B ≡ finite B ∧ B ⊆ V ∧ bij_betw (λc. lincomb c B) (B →⇩_E R) V"

text ‹∗‹Bridge: the finite forms agree with the module-level notions.›  On a finite set the two
  spanning conditions coincide: ‹mod.spanning› says every vector lies in the span, and on a
  finite @{term B} a span membership is realised by a coefficient function on @{term B} itself
  (extended by @{term 𝟬} where the witnessing subset omits an element).›
lemma spanning_iff_mod_spanning:
  assumes finB: "finite B" and BV: "B ⊆ V"
  shows "spanning B ⟷ mod.spanning B"
proof
  assume "spanning B"
  show "mod.spanning B"
  proof (rule mod.spanningI[OF BV])
    fix v assume v: "v ∈ V"
    with ‹spanning B› mod.Module_axioms show "v ∈ mod.span B"
      using mod.spanI Module.spanI finB mod.coeffs_on_def 
      by (fastforce simp: PiE_iff spanning_def)
  qed
next
  assume ms: "mod.spanning B"
  have "∀v∈V. ∃c∈B →⇩_E R. v = lincomb c B"
  proof (rule ballI)
    fix v assume "v ∈ V"
    then obtain c A where A: "finite A" "A ⊆ B" "mod.coeffs_on c A" "v = lincomb c A"
      using mod.spanE mod.spanning_def ms by metis
    ― ‹Extend @{term c} by @{term 𝟬} off @{term A} and make it extensional on @{term B}.›
    define c' where "c' ≡ (λu. if u ∈ A then c u else 𝟬)"
    have c'R: "mod.coeffs_on c' B"
      using A(3) c'_def mod.coeffs_on_def by force
    have "lincomb c' A = lincomb c' B"
      using ‹A ⊆ B› BV c'R c'_def finB mod.lincomb_mono_zero by force
    moreover have "lincomb c' A = lincomb c A"
      using ‹A ⊆ B› BV mod.coeffs_onD[OF A(3)]
      by (intro mod.lincomb_cong) (auto simp: c'_def intro!: mod.coeffs_onI)
    ultimately have vc': "v = lincomb c' B" using A(4) by simp
    ― ‹Make it extensional on @{term B}; that changes no value on @{term B}.›
    have "lincomb (restrict c' B) B = lincomb c' B"
      by (rule mod.lincomb_cong[OF BV]) (use c'R in simp_all)
    with vc' have "v = lincomb (restrict c' B) B" by simp
    moreover have "restrict c' B ∈ B →⇩_E R"
      using mod.coeffs_onD[OF c'R] by auto
    ultimately show "∃c∈B →⇩_E R. v = lincomb c B" by blast
  qed
  with finB BV show "spanning B" unfolding spanning_def by blast
qed

text ‹Likewise for independence.  The finite form quantifies over total coefficient functions on
  @{term B}; the module form over coefficient functions on finite subsets.  On a finite @{term B}
  these agree: restrict to the subset in one direction, extend by @{term 𝟬} in the other.›
lemma lin_indep_iff_mod_lin_indep:
  assumes finB: "finite B" and BV: "B ⊆ V"
  shows "lin_indep B ⟷ mod.lin_indep B"
proof
  assume li: "lin_indep B"
  show "mod.lin_indep B"
  proof (rule mod.lin_indepI[OF BV])
    fix c A v
    assume "finite A" "A ⊆ B" and cA: "mod.coeffs_on c A"
      and zero: "lincomb c A = 𝟬⇩_V" and vA: "v ∈ A"
    define c' where "c' = restrict (λu. if u ∈ A then c u else 𝟬) B"
    have c'R: "mod.coeffs_on c' B"
      by (rule mod.coeffs_onI) (use mod.coeffs_onD[OF cA] in ‹simp add: c'_def›)
    have c'PiE: "c' ∈ B →⇩_E R" using mod.coeffs_onD[OF c'R] by (auto simp: c'_def)
    have "lincomb c' A = lincomb c A"
      using ‹A ⊆ B› BV mod.coeffs_onD[OF cA]
      by (intro mod.lincomb_cong) (auto simp: c'_def intro!: mod.coeffs_onI)
    moreover have "lincomb c' A = lincomb c' B"
      using ‹A ⊆ B› BV c'R c'_def finB mod.lincomb_mono_zero by force
    ultimately have "lincomb c' B = 𝟬⇩_V" using zero by simp
    then have "c' v = 𝟬" using c'PiE li  using ‹A ⊆ B› vA by (auto simp: lin_indep_def)
    then show "c v = 𝟬" using ‹A ⊆ B› c'_def vA by auto
  qed
next
  assume ms: "mod.lin_indep B"
  ― ‹@{method rule} twice, not @{method intro}: ‹intro› is greedy and would also strip the inner
    bounded quantifier, leaving a goal the @{command show} below cannot match.›
  have "∀c∈B →⇩_E R. lincomb c B = 𝟬⇩_V ⟶ (∀v∈B. c v = 𝟬)"
    using finB mod.coeffs_on_def mod.lin_indepD ms by (meson PiE_mem subset_refl)
  with finB BV show "lin_indep B" unfolding lin_indep_def by blast
qed

text ‹A basis spans: surjectivity of the coordinate map.›
lemma basis_spanning:
  assumes "basis B" shows "spanning B"
  unfolding spanning_def
  using assms basis_def by (metis (no_types, lifting) bij_betw_def imageE)

text ‹∗‹The dimension counting theorem.›  Over a finite field, a space with a basis of size
  @{term n} has exactly @{term "card R ^ n"} elements: its coordinate map is a bijection onto
  the @{term "card R ^ n"} coefficient vectors @{term "B →⇩_E R"}.›
theorem card_eq_card_base_pow_dim:
  assumes "basis B"
  shows "card V = card R ^ card B"
  by (metis assms basis_def bij_betw_same_card card_funcsetE)

text ‹∗‹Over a finite field, any two bases have the same size› --- so the dimension is well defined.
  (Both give @{term "card V = card R ^ card B⇩_i"}, and @{term "card R ≥ 2"} is injective as a base of
  exponentiation.)›
theorem basis_card_unique_finite:
  assumes finR: "finite R" and B1: "basis B⇩₁" and B2: "basis B⇩₂"
  shows "card B⇩₁ = card B⇩₂"
proof -
  have "card R ^ card B⇩₁ = card V" using card_eq_card_base_pow_dim[OF B1] by simp
  also have "… = card R ^ card B⇩₂" using card_eq_card_base_pow_dim[OF B2] by simp
  finally have eq: "card R ^ card B⇩₁ = card R ^ card B⇩₂" .
  ― ‹The field has at least two elements (@{term "𝟭 ≠ 𝟬"}), so exponentiation is injective.›
  have "card R ≥ 2" using nontrivial card_mono[OF finR, of "{𝟭,𝟬}"] by auto
  then show ?thesis using eq by simp
qed

text ‹The dimension of the space: the size of a basis (well defined over a finite field).›
definition dimension :: nat
  where "dimension = card (SOME B. basis B)"

lemma dimension_eq:
  assumes finR: "finite R" and B: "basis B" shows "dimension = card B"
  by (metis B basis_card_unique_finite dimension_def finR someI)

end

text ‹A vector subspace packages a module-level submodule of a vector space and exposes the
  induced vector-space structure under the prefix ‹sub›.›

locale vector_subspace = Vector_Space +
  fixes W :: "'b set"
  assumes W_submodule: "mod.submodule W"
begin

sublocale sub: Vector_Space R "(+)" "(⋅)" "𝟬" "𝟭" "(⊕)" "𝟬⇩_V" W "(⊙)"
  by (rule submodule_vector_space[OF W_submodule])

end

text ‹Following the @{text field_TC} pattern of ‹Ring_Theory›, we bridge
  the locale-based @{locale Vector_Space} to Isabelle's type-class arithmetic.  A type-class field
  @{typ "'a :: field"} plays the scalar role, and a type-class abelian additive group
  @{typ "'b :: ab_group_add"} plays the vector role; a scale operation
  @{term "scale :: 'a ⇒ 'b ⇒ 'b"} satisfying the four vector-space axioms then witnesses
  @{locale Vector_Space} on the whole types as carriers.›

lemma vector_space_TC:
  fixes scale :: "'a::field ⇒ 'b::ab_group_add ⇒ 'b"
  assumes scale_add_right: "⋀a x y. scale a (plus x y) = plus (scale a x) (scale a y)"
    and scale_add_left:    "⋀a b x. scale (plus a b) x = plus (scale a x) (scale b x)"
    and scale_scale:       "⋀a b x. scale a (scale b x) = scale (a * b) x"
    and scale_one:         "⋀x. scale 1 x = x"
  shows "Vector_Space (UNIV :: 'a set) plus (*) 0 1 plus 0 (UNIV :: 'b set) scale"
proof -
  interpret F: Field "UNIV :: 'a set" "plus" "(*)" 0 1 by (rule field_TC.Field_axioms)
  show ?thesis
  proof (intro Vector_Space.intro Vector_Space_axioms.intro)
    show "Field (UNIV :: 'a set) plus (*) 0 1" by (rule field_TC.Field_axioms)
    show "Abelian_Group (UNIV :: 'b set) plus 0" by (rule add_abelian_TC)
  qed (simp_all add: scale_add_right scale_add_left scale_scale scale_one)
qed

text ‹Concrete specialisations to Isabelle's built-in ‹real_vector› and ‹complex_vector› classes
   can be added by any consumer.›

end