Quelle  Algebra_On.thy

(*  Title:       Algebra_On
    Author:      Richard Schmoetten <richard.schmoetten@ed.ac.uk>, 2024
    Maintainer:  Richard Schmoetten <richard.schmoetten@ed.ac.uk>
*)

theory Algebra_On
imports
  "HOL-Types_To_Sets.Linear_Algebra_On"
  "Jacobson_Basic_Algebra.Ring_Theory"
begin

section ‹Abstract algebra locales over a 🍋‹field››
text ‹... with carrier set and some implicit operations
 (only algebraic multiplication, scaling, and derived constants are not implicit).›

text ‹For full generality, one could define an algebra as a ring that is also a module
 (rather than a vector space, i.e. have a (non/commutative) base ring instead of a base field).›

subsection ‹Bilinearity, Jacobi identity›


lemma (in module_hom_on) mem_hom:
  assumes "x ∈ S1"
  shows "f x ∈ S2"
  using scale[OF assms, of 1] m2.mem_scale[of "f x" 1] m2.scale_one_on[of "f x"] oops

locale bilinear_on =
  vector_space_pair_on V W scaleV scaleW +
  vector_space_on X scaleX
  for V:: "'b::ab_group_add set" and W::"'c::ab_group_add set" and X::"'d::ab_group_add set"
    and scaleV::"'a::field==>'b==>'b" (infixr ‹🍋_V› 75)
    and scaleW::"'a==>'c==>'c" (infixr ‹🍋_W› 75)
    and scaleX::"'a==>'d==>'d" (infixr ‹🍋_X› 75) +
  fixes f::"'b==>'c==>'d"
  assumes linearL: "w∈W ==> linear_on V X scaleV scaleX (λv. f v w)"
    and linearR: "v∈V ==> linear_on W X scaleW scaleX (λw. f v w)"
begin

lemma linearL': "[v∈V; w∈W] ==> f (a 🍋_V v) w = a 🍋_X (f v w)"
    "[v∈V; v'∈V; w∈W] ==> f (v + v') w = (f v w) + (f v' w)"
  using linearL unfolding linear_on_def module_hom_on_def module_hom_on_axioms_def
  by simp+

lemma linearR': "[v∈V; w∈W] ==> f v (a 🍋_W w) = a 🍋_X (f v w)"
    "[v∈V; w∈W; w'∈W] ==> f v (w + w') = (f v w) + (f v w')"
  using linearR unfolding linear_on_def module_hom_on_def module_hom_on_axioms_def
  by simp+

lemma bilinear_zero [simp]:
  shows "w∈W ==> f 0 w = 0" "v∈V ==> f v 0 = 0"
  using linearL'(2) m1.mem_zero linearR'(2) m2.mem_zero by fastforce+

lemma bilinear_uminus [simp]:
  assumes v: "v∈V" and w: "w∈W"
  shows "f (-v) w = - (f v w)" "f v (-w) = - (f v w)"
  using v w linearL'(2) m1.mem_uminus bilinear_zero(1) ab_left_minus add_right_imp_eq apply metis
  using v w linearR'(2) m2.mem_uminus bilinear_zero(2) add_left_cancel add.right_inverse by metis


end


text ‹For bilinear maps, "alternating" means the same as "skew-symmetric",
 which is the same as "anti-symmetric".›
locale alternating_bilinear_on = bilinear_on S S S scale scale scale f for S scale f +
  assumes alternating: "x∈S ==> f x x = 0"
begin

lemma antisym:
  assumes "x∈S" "y∈S"
  shows "(f x y) + (f y x) = 0"
proof -
  have "f (x+y) (x+y) = (f x x) + (f x y) + (f y x) + (f y y)"
    using linearL'(2) linearR'(2) by (simp add: assms m1.mem_add)
  thus ?thesis
    using alternating by (simp add: assms m1.mem_add)
qed

lemma antisym':
  assumes "x∈S" "y∈S"
  shows "(f x y) = - (f y x)"
  using antisym[OF assms] by (simp add: eq_neg_iff_add_eq_0)

lemma antisym_uminus:
  assumes "x∈S" "y∈S"
  shows "f (-x) y = f y x""f x (-y) = f y x"
  using bilinear_uminus by (metis antisym' assms)+


end


abbreviation (input) jacobi_identity_with::"'a ==> ('a==>'a==>'a) ==> ('a==>'a==>'a) ==> 'a ==> 'a ==> 'a ==> bool"
  where "jacobi_identity_with zero_add f_add f_mult x y z ≡
      zero_add = f_add (f_add (f_mult x (f_mult y z)) (f_mult y (f_mult z x))) (f_mult z (f_mult x y))"

abbreviation (input) jacobi_identity::"('a::{monoid_add}==>'a==>'a) ==> 'a ==> 'a ==> 'a ==> bool"
  where "jacobi_identity f_mult x y z ≡ jacobi_identity_with 0 (+) f_mult x y z"

lemma (in module_hom_on) mapsto_zero: "f 0 = 0"
  using add m1.mem_zero by fastforce

lemma (in module_hom_on) mapsto_uminus: "a∈S1 ==> f (-a) = - f a"
  by (metis add m1.mem_uminus neg_eq_iff_add_eq_0 mapsto_zero)

lemma (in module_hom_on) mapsto_closed: "a∈S1 ==> f a ∈ S2"
  using mapsto_zero add mapsto_uminus
oops


subsection ‹Unital and associative algebras›

locale algebra_on = bilinear_on S S S scale scale scale amult
  for S
    and scale :: "'a::field ==> 'b::ab_group_add ==> 'b" (infixr ‹*_S› 75)
    and amult (infixr ‹🍋› 74) +
  assumes amult_closed [simp]: "a∈S ==> b∈S ==> amult a b ∈ S"
begin

lemma
    shows distR: "[x∈S; y∈S; z∈S] ==> (x+y) 🍋 z = x 🍋 z + y 🍋 z"
      and distL: "[x∈S; y∈S; z∈S] ==> z 🍋 (x+y) = z 🍋 x + z 🍋 y"
      and scalar_compat (* [simp] *): "\<lbrakk>x\<in>S; y\<in>S\<rbrakk> \<Longrightarrow> (a *\<^sub>S x) \<Zspot> (b *\<^sub>S y) = (a*b) *\<^sub>S (x \<Zspot> y)"
    using algebra_on_axioms unfolding algebra_on_def bilinear_on_def bilinear_on_axioms_def
      linear_on_def module_hom_on_def module_hom_on_axioms_def
    by (blast, blast, metis m1.mem_scale m1.scale_scale_on)

  lemma scalar_compat' [simp]:
    shows "[x∈S; y∈S] ==> (a *_S x) 🍋 y = a *_S (x 🍋 y)"
      and "[x∈S; y∈S] ==> x 🍋 (a *_S y) = a *_S (x 🍋 y)"
      by (simp_all add: linearL' linearR')

end

text‹
 Sometimes an associative algebra is defined as a ring that is also a module (over a comm. ring),
 with the module and scalar multiplication being compatible, and the ring and module addition being the same.
 That definition implies an associative algebra is also unital, i.e. there is a multiplicative identity;
 in contrast, our definition doesn't. This is in agreement with how a 🍋‹'a::ring› needs no identity,
 and an additional type class typ>‹'a::ring_1› is provided (instead of the terminology of rng vs. ring).›
locale assoc_algebra_on = algebra_on +
  assumes amult_assoc: "[x∈S; y∈S; z∈S] ==> (x🍋y)🍋z = x🍋(y🍋z)"


locale unital_algebra_on = algebra_on +
  fixes a_id
  assumes amult_id [simp]: "a_id∈S" "a∈S ==> a🍋a_id=a" "a∈S ==> a_id🍋a=a"
begin

  lemma id_neq_0_iff: "∃a∈S. ∃b∈S. a≠b ⟷ 0 ≠ a_id"
    using amult_id(1) m1.mem_zero by blast

  lemma id_neq_0_if:
    shows "a∈S ==> b∈S ==> a≠b ==> 0 ≠ a_id"
      and "card S ≥ 2 ==> 0 ≠ a_id"
      and "infinite S ==> 0 ≠ a_id"
  proof -

    (* Lifted from HOL-Analysis.Linear_Algebra, which I didn't want to import for one lemma. *)
    have ex_card: "∃S⊆A. card S = n"
      if "n ≤ card A"
      for n and A::"'a set"
    proof (cases "finite A")
      case True
      from ex_bij_betw_nat_finite[OF this] obtain f where f: "bij_betw f {0..<card A} A" ..
      moreover from f ‹n ≤ card A› have "{..< n} ⊆ {..< card A}" "inj_on f {..< n}"
        by (auto simp: bij_betw_def intro: inj_on_subset)
      ultimately have "f ` {..< n} ⊆ A" "card (f ` {..< n}) = n"
        by (auto simp: bij_betw_def card_image)
      then show ?thesis by blast
    next
      case False
      with ‹n ≤ card A› show ?thesis by force
    qed

    show "a∈S ==> b∈S ==> a≠b ==> 0 ≠ a_id"
      using amult_id(2) linearR' m1.mem_zero m1.scale_zero_left by metis
    thus "card S ≥ 2 ==> 0 ≠ a_id"
      by (metis amult_id(2) card_2_iff' ex_card m1.mem_zero m1.scale_zero_left scalar_compat'(2) subset_iff)
    thus "infinite S ==> 0 ≠ a_id"
      using infinite_arbitrarily_large
      by (metis amult_id(2) card_2_iff' linearR'(1) m1.mem_zero m1.scale_zero_left subset_iff)
  qed

  lemma id_neq_0_implies_elements (* [simp] *): "\<exists>a\<in>S. \<exists>b\<in>S. a\<noteq>b" if "0 \<noteq> a_id"
    using amult_id(1) m1.mem_zero that by blast

  lemma id_neq_0_implies_card:
    assumes "0 ≠ a_id"
    obtains "card S ≥ 2" | "infinite S"
    using id_neq_0_implies_elements[OF assms] unfolding numeral_2_eq_2
    using card_le_Suc0_iff_eq not_less_eq_eq by blast

  lemma id_unique [simp]:
    fixes other_id
    assumes "other_id∈S" "∧a. a∈S ==> a🍋other_id=a ∧ other_id🍋a=a"
    shows "other_id = a_id"
    using assms amult_id by fastforce

end


locale assoc_algebra_1_on = assoc_algebra_on + unital_algebra_on +
  assumes id_neq_0 [simp]: "a_id ≠ 0" ― ‹this is as in the class ‹ring_1›, and merely assures ‹S› has at least two elements›
begin

  lemma is_ring_1_axioms:
    shows "∧a b c. a∈S ==> b∈S ==> c∈S ==> a 🍋 b 🍋 c = a 🍋 (b 🍋 c)"
      and "∧a. a∈S ==> a_id 🍋 a = a"
      and "∧a. a∈S ==> a 🍋 a_id = a"
      and "∧a b c. a∈S ==> b∈S ==> c∈S ==> (a + b) 🍋 c = a 🍋 c + b 🍋 c"
      and "∧a b c. a∈S ==> b∈S ==> c∈S ==> a 🍋 (b + c) = a 🍋 b + a 🍋 c"
      by (simp_all add: distR distL algebra_simps)

  lemma inverse_unique [simp]:
    assumes a: "a∈S" "a≠0"
      and x: "x∈S" "a🍋x=a_id ∧ x🍋a=a_id"
      and y: "y∈S" "a🍋y=a_id ∧ y🍋a=a_id"
    shows "x = y"
    using amult_assoc[of x a x] amult_assoc[of x a y]
    by (simp add: assms)

  lemma inverse_unique':
    assumes a: "a∈S" "a≠0"
      and inv_ex: "∃x∈S. a🍋x=a_id ∧ x🍋a=a_id"
    shows "∃!x∈S. a🍋x=a_id ∧ x🍋a=a_id"
    using a inv_ex inverse_unique by (metis (no_types, lifting)) 

end

lemma algebra_onI [intro]:
  fixes scale :: "'a::field ==> 'b::ab_group_add ==> 'b" (infixr ‹*_S› 75)
    and amult (infixr ‹🍋› 74)
  assumes "vector_space_on S scale"
    and distR: "∧x y z. [x∈S; y∈S; z∈S] ==> (x+y) 🍋 z = x 🍋 z + y 🍋 z"
    and distL: "∧x y z. [x∈S; y∈S; z∈S] ==> z 🍋 (x+y) = z 🍋 x + z 🍋 y"
    and scalar_compat: "∧a x y. [x∈S; y∈S] ==> (a *_S x) 🍋 y = a *_S (x 🍋 y) ∧ x 🍋 (a *_S y) = a *_S (x 🍋 y)"
    and closure: "∧x y. [x∈S; y∈S] ==> x 🍋 y ∈ S"
  shows "algebra_on S scale amult"
  unfolding algebra_on_def bilinear_on_def vector_space_pair_on_def bilinear_on_axioms_def
  apply (intro conjI algebra_on_axioms.intro, simp_all add: assms(1))
  unfolding linear_on_def module_hom_on_def module_hom_on_axioms_def
  by (auto simp: assms vector_space_on.axioms)


lemma (in vector_space_on) scalar_compat_iff:
  fixes scale_notation (infixr ‹*_S› 75)
    and amult (infixr ‹🍋› 74)
  defines "scale_notation ≡ scale"
  assumes distR: "∧x y z. [x∈S; y∈S; z∈S] ==> (x+y) 🍋 z = x 🍋 z + y 🍋 z"
    and distL: "∧x y z. [x∈S; y∈S; z∈S] ==> z 🍋 (x+y) = z 🍋 x + z 🍋 y"
  shows "(∀a. ∀x∈S. ∀y∈S. (a *_S x) 🍋 y = a *_S (x 🍋 y) ∧ x 🍋 (a *_S y) = a *_S (x ?? y)) ⟷
      (∀a b. ∀x∈S. ∀y∈S. (a *_S x) 🍋 (b *_S y) = (a*b) *_S (x 🍋 y))"
proof (intro iffI)
  { assume asm: "∧a b x y. x∈S ==> y∈S ==> a *_S x 🍋 b *_S y = (a * b) *_S (x 🍋 y)"
    { fix a x y
      assume S: "x∈S" "y∈S"
      have "a *_S x 🍋 y = a *_S (x 🍋 y)" "x 🍋 a *_S y = a *_S (x 🍋 y)"
        using asm[of x y a 1] S apply (simp add: scale_notation_def)
        using asm[of x y 1 a] S by (simp add: scale_notation_def) }}
  thus "∀a b. ∀x∈S. ∀y∈S. a *_S x 🍋 b *_S y = (a * b) *_S (x 🍋 y) ==>
      ∀a. ∀x∈S. ∀y∈S. a *_S x 🍋 y = a *_S (x 🍋 y) ∧ x 🍋 a *_S y = a *_S (x 🍋 y)"
    by blast
qed (metis mem_scale scale_notation_def scale_scale_on)


lemma (in vector_space_on) algebra_onI:
  fixes scale_notation (infixr ‹*_S› 75)
    and amult (infixr ‹🍋› 74)
  defines "scale_notation ≡ scale"
  assumes distR: "∧x y z. [x∈S; y∈S; z∈S] ==> (x+y) 🍋 z = x 🍋 z + y 🍋 z"
    and distL: "∧x y z. [x∈S; y∈S; z∈S] ==> z 🍋 (x+y) = z 🍋 x + z 🍋 y"
    and scalar_compat: "∧a x y. [x∈S; y∈S] ==> (a *_S x) 🍋 y = a *_S (x 🍋 y) ∧ x 🍋 (a *_S y) = a *_S (x 🍋 y)"
    and closure: "∧x y. [x∈S; y∈S] ==> x 🍋 y ∈ S"
  shows "algebra_on S scale amult"
  using algebra_onI[of S scale amult] assms scale_notation_def vector_space_on_axioms by simp


subsection ‹Lie algebra (locale)›

text ‹
 List syntax interferes with the standard notation for the Lie bracket,
 so it can be disabled it here. Instead, we add a delimiter to the notation for Lie brackets,
 which also helps with unambiguous parsing.
 ›
(*unbundle no list_syntax and no list_enumeration_syntax*)
(*end*)

locale lie_algebra = algebra_on g scale lie_bracket + alternating_bilinear_on g scale lie_bracket
  for g
    and scale :: "'a::field ==> 'b::ab_group_add ==> 'b" (infixr ‹*_S› 75)
    and lie_bracket :: "'b ==> 'b ==> 'b" (‹[_;_]› 74) +
  assumes jacobi: "[x∈g; y∈g; z∈g] ==> 0 = [x;[y;z]] + [y;[z;x]] + [z;[x;y]]"

lemma (in algebra_on) lie_algebraI:
  assumes alternating: "∀x∈S. amult x x = 0"
    and jacobi: "∀x∈S. ∀y∈S. ∀z∈S. jacobi_identity amult x y z"
  shows "lie_algebra S scale amult"
  apply unfold_locales using assms by auto

lemma (in vector_space_on) lie_algebraI:
  fixes lie_bracket :: "'b ==> 'b ==> 'b" (‹[_;_]› 74)
    and scale_notation (infixr ‹*_S› 75)
  defines "scale_notation ≡ scale"
  assumes distributivity:
      "∧x y z. [x∈S; y∈S; z∈S] ==> [(x+y); z] = [x; z] + [y; z] ∧ [z; (x+y)] = [z; x] + [z; y]"
    and scalar_compatibility:
      "∧a x y. [x∈S; y∈S] ==> [(a *_S x); y] = a *_S ([x; y]) ∧ [x; (a *_S y)] = a *_S ([x; y])"
    and closure: "∧x y. [x∈S; y∈S] ==> [x; y] ∈ S"
    and alternating: "∀x∈S. lie_bracket x x = 0"
    and jacobi: "∀x∈S. ∀y∈S. ∀z∈S. jacobi_identity lie_bracket x y z"
  shows "lie_algebra S scale lie_bracket"
  using assms(1,3,6) by (auto simp: assms(2,4,5) intro!: algebra_on.lie_algebraI algebra_onI)

context lie_algebra begin

lemma jacobi_alt:
  assumes x: "x∈g" and y: "y∈g" and z: "z∈g"
  shows "[x;[y;z]] = [[x;y];z] + [y;[x;z]]"
proof -
  have "[x;[y;z]] = - ([y;[z;x]]) + (- ([z;[x;y]]))"
    using jacobi[OF assms] add_implies_diff[of "[x;[y;z]]" "[y;[z;x]] + [z;[x;y]]" 0]
    by (simp add: add.commute add.left_commute)
  moreover have "[[x;y];z] = - ([z;[x;y]])" "- ([y;[z;x]]) = [y;[x;z]]"
    using antisym'[OF amult_closed[OF x y] z] antisym'[OF z x] by (simp_all add: assms)
  ultimately show "[x;[y;z]] = [[x;y];z] + [y;[x;z]]" by simp
qed


lemma lie_subalgebra:
  assumes h: "h⊆g" "m1.subspace h" and closed: "∧x y. x ∈ h ==> y ∈ h ==> lie_bracket x y ∈ h"
  shows "lie_algebra h scale lie_bracket"
proof -
  interpret h: vector_space_on h scale
    apply unfold_locales
    apply (meson h(1) m1.scale_right_distrib_on subset_iff)
    apply (meson h(1) in_mono m1.scale_left_distrib_on)
    using h(1) m1.scale_scale_on m1.scale_one_on apply auto[2]
    by (simp_all add: h m1.subspace_add m1.subspace_0 m1.subspace_scale)

  show ?thesis
    apply (intro h.lie_algebraI)
    using alternating h(1) jacobi linearL' linearR' by (auto simp: closed subset_iff)
qed

end


subsection ‹Division algebras›

abbreviation (in algebra_on) "is_left_divisor x a b ≡ x ∈ S ∧ a = amult x b"
abbreviation (in algebra_on) "is_right_divisor x a b ≡ x ∈ S ∧ a = amult b x"

locale div_algebra_on = algebra_on +
  fixes divL::"'a==>'a==>'a" (* (infix "/\<^sub>L" 74) *)
    and divR::"'a==>'a==>'a" (* (infix "/\<^sub>R" 74) *)
  assumes divL: "[a∈S; b∈S; b≠0] ==> is_left_divisor (divL a b) a b"
      "[a∈S; b∈S; b≠0] ==> is_left_divisor y a b ==> y = (divL a b)"
    and divR: "[a∈S; b∈S; b≠0] ==> is_right_divisor (divR a b) a b"
      "[a∈S; b∈S; b≠0] ==> is_right_divisor y a b ==> y = (divR a b)"
begin
text ‹ In terms of the vocabulary of division rings,
 the expression term‹a = (divL a b) 🍋 b› means that term‹divL a b› is a left divisor of term‹a›,
 and conversely that term‹a› is a right multiple of term‹divL a b›.›
text ‹
 For term‹b=0›, the divisiors still exist as members of the correct type (necessarily),
 but they have no properties. Similarly for correctly-typed input outside the algebra.›

  lemma [simp]:
    assumes "a∈S" "b∈S" "b≠0"
    shows divL': "divL a b ∈ S" "(divL a b) 🍋 b = a" "∀y∈S. a = y 🍋 b ⟶ y = divL a b"
      and divR': "divR a b ∈ S" "b 🍋 (divR a b) = a" "∀y∈S. a = b 🍋 y ⟶ y = divR a b"
    using assms divL divR by simp_all
end

lemma (in algebra_on) div_algebra_onI:
  assumes "∀a∈S. ∀b∈S. b≠0 ⟶ (∃!x∈S. a=b🍋x) ∧ (∃!y∈S. a=y🍋b)"
  shows "div_algebra_on S scale amult (λa b. THE y. y∈S ∧ a=y🍋b) (λa b. THE x. x∈S ∧ a=b🍋x)"
proof (unfold div_algebra_on_def div_algebra_on_axioms_def, intro conjI allI impI)
  fix a b x
  assume "a∈S" "b∈S" "b≠0"
  have exL: "∃!x∈S. a=x🍋b" by (simp add: ‹a ∈ S› ‹b ∈ S› ‹b ≠ 0› assms)
  from theI'[OF this]
    show L: "(THE y. y ∈ S ∧ a = y 🍋 b) ∈ S" "a = (THE y. y ∈ S ∧ a = y 🍋 b) 🍋 b"
    by simp+
  have exR: "∃!x∈S. a=b🍋x" by (simp add: ‹a ∈ S› ‹b ∈ S› ‹b ≠ 0› assms)
  from theI'[OF this]
    show R: "(THE x. x ∈ S ∧ a = b 🍋 x) ∈ S" "a = b 🍋 (THE x. x ∈ S ∧ a = b 🍋 x)"
    by simp+
  { assume "x ∈ S ∧ a = x 🍋 b"
    thus "x = (THE y. y ∈ S ∧ a = y 🍋 b)" using L exL by auto
  } { assume "x ∈ S ∧ a = b 🍋 x"
    thus "x = (THE x. x ∈ S ∧ a = b 🍋 x)" using R exR by auto
  }
qed (simp add: algebra_on_axioms)

lemma (in assoc_algebra_1_on) div_algebra_onI':
  fixes ainv adivL adivR
  defines "ainv a ≡ (THE x. x∈S ∧ a_id=x🍋a ∧ a_id=a🍋x)"
    and "adivL b a ≡ b 🍋 (ainv a)"
    and "adivR b a ≡ (ainv a) 🍋 b"
  assumes "∀a∈S. a≠0 ⟶ (∃x∈S. a_id=x🍋a ∧ a_id=a🍋x)"
  shows "div_algebra_on S scale amult adivL adivR"
proof (unfold_locales)
  fix a b
  assume asm: "a ∈ S" "b ∈ S" "b ≠ 0"
  have inv_ex: "∃!x∈S. a_id=x🍋b ∧ a_id=b🍋x"
    using assms(4) inverse_unique' asm(2,3) by metis
  let ?a = "THE x. x ∈ S ∧ a_id = x 🍋 b ∧ a_id = b 🍋 x"
  from theI'[OF inv_ex] show 1: "adivR a b ∈ S ∧ a = b 🍋 adivR a b"
    unfolding adivR_def ainv_def apply (intro conjI)
    using asm(1) apply simp
    using amult_assoc amult_id(2) asm(1,2) is_ring_1_axioms(2) by (metis (no_types, lifting))
  from theI'[OF inv_ex] show 2: "adivL a b ∈ S ∧ a = adivL a b 🍋 b"
    unfolding adivL_def ainv_def apply (intro conjI)
    apply (simp add: asm(1))
    using amult_assoc asm(1,2) is_ring_1_axioms(3) by presburger
  { fix y assume "y ∈ S ∧ a = y 🍋 b"
    thus "y = adivL a b"
      by (metis inv_ex 2 amult_assoc asm(2) amult_id(2))
  } { fix y assume "y ∈ S ∧ a = b 🍋 y"
    thus "y = adivR a b"
    by (metis 1 amult_assoc asm(2) inv_ex is_ring_1_axioms(2)) }
qed

lemma (in assoc_algebra_on) div_algebra_on_imp_inverse:
  assumes "div_algebra_on S scale amult divL divR" "card S ≥ 2 ∨ infinite S"
  shows "∃a_id∈S. (∀a∈S. a🍋a_id=a ∧ a_id🍋a=a) ∧ (∀a∈S. a≠0 ⟶ divL a_id a = divR a_id a)"
proof -
  obtain x where "x≠0" "x∈S"
    using assms(2) unfolding numeral_2_eq_2
    by (metis card_1_singleton_iff card_gt_0_iff card_le_Suc0_iff_eq insertI1 not_less_eq_eq
      rev_finite_subset subsetI zero_less_Suc)
  let ?id = "divL x x"
  show ?thesis
  proof (intro bexI conjI ballI impI)
    show 1: "?id ∈ S"
      using assms unfolding div_algebra_on_def div_algebra_on_axioms_def
      using ‹x ∈ S› ‹x ≠ 0› by blast
    fix a assume "a∈S"
    show 2: "a 🍋 ?id = a"
      by (smt (verit) 1 ‹a∈S› ‹x∈S› ‹x≠0› amult_assoc amult_closed assms(1) div_algebra_on.divL)
    show 3: "?id 🍋 a = a"
      by (smt (verit) ‹a∈S› ‹x∈S› ‹x≠0› amult_assoc assms(1) div_algebra_on.divL(1) div_algebra_on.divR')
    assume "a≠0"
    show 4: "divL ?id a = divR ?id a"
      by (smt (verit) 1 3 ‹a∈S› ‹a≠0› amult_assoc amult_closed assms(1) div_algebra_on.divL div_algebra_on.divR(2))
  qed
qed

lemma (in assoc_algebra_on) assoc_div_algebra_on_iff:
  assumes "card S ≥ 2 ∨ infinite S"
  shows "(∃divL divR. div_algebra_on S scale amult divL divR) ⟷
      (∃id. unital_algebra_on S scale amult id ∧ (∀a∈S. a≠0 ⟶ (∃x∈S. a🍋x=id ∧ x🍋a=id)))"
  proof (intro iffI)
    assume "∃id. unital_algebra_on S (*_S) (🍋) id ∧ (∀a∈S. a ≠ 0 ⟶ (∃x∈S. a 🍋 x = id ∧ x 🍋 a = id))"
    then obtain id
      where id: "id∈S" "∀a∈S. a🍋id=a ∧ id🍋a=a" and inv: "∀a∈S. a≠0 ⟶ (∃x∈S. a🍋x=id ∧ x🍋a=id)"
      using unital_algebra_on.amult_id by blast
    then have unital: "unital_algebra_on S scale amult id"
      by (unfold_locales, simp_all)
    then have assoc_alg: "assoc_algebra_1_on S scale amult id"
      unfolding assoc_algebra_1_on_def assoc_algebra_1_on_axioms_def
      using assms unital_algebra_on.id_neq_0_if(2,3) assoc_algebra_on_axioms
      by blast
    show "∃divL divR. div_algebra_on S (*_S) (🍋) divL divR"
      using assoc_algebra_1_on.div_algebra_onI'[OF assoc_alg] inv by fastforce
  next
    assume "∃divL divR. div_algebra_on S (*_S) (🍋) divL divR"
    then obtain divL divR where div_alg: "div_algebra_on S (*_S) (🍋) divL divR" by blast
    show "∃id. unital_algebra_on S (*_S) (🍋) id ∧ (∀a∈S. a ≠ 0 ⟶ (∃x∈S. a 🍋 x = id ∧ x 🍋 a = id))"
      using div_algebra_on_imp_inverse[OF div_alg assms] unital_algebra_on_axioms.intro assoc_algebra_on_axioms
      unfolding unital_algebra_on_def unital_algebra_on_axioms_def assoc_algebra_on_def
      by (smt (verit) div_alg div_algebra_on.divL(1) div_algebra_on.divR(1))
qed


locale assoc_div_algebra_on =
  assoc_algebra_1_on S scale amult a_id +
  div_algebra_on S scale amult "λa b. amult a (a_inv b)" "λa b. amult (a_inv b) a"
  for S
    and scale :: "'a::field ==> 'b::ab_group_add ==> 'b" (infixr ‹*_S› 75)
    and amult :: "'b==>'b==>'b" (infixr ‹🍋› 74)
    and a_id  :: 'b(‹1›)
    and a_inv :: "'b==>'b" (* (\<open>_\<^sup>\<Zspot>\<close> 73) *)
begin
text ‹
 The definition 🍋‹assoc_div_algebra_on› is justified by @{thm assoc_div_algebra_on_iff} above:
 If we have an associative algebra already, the only way it can be a division algebra
 is to be unital as well. Since now left and right divisors can be defined through
 multiplicative inverses, we take only the inverse as a locale parameter, and construct
 the divisors.
 The only case we miss here (due to the requirement term‹a_id≠0›) is the trivial algebra,
 which contains only the zero element (which acts as identity as well). This is for compatibility
 with the standard Isabelle/HOL type classes, which are subclasses of 🍋‹zero_neq_one›.
 ›

  abbreviation (input) divL :: "'b==>'b==>'b"
    where "divL a b ≡ amult a (a_inv b)"

  abbreviation (input) divR :: "'b==>'b==>'b"
    where "divR a b ≡ amult (a_inv b) a"

  lemma div_self_eq_id:
    assumes "a∈S" "a≠0"
    shows "divL a a = a_id"
      and "divR a a = a_id"
    apply (metis amult_id(1,3) assms divL'(3))
    by (metis amult_id(1,2) assms divR'(3))

end


locale finite_dimensional_assoc_div_algebra_on =
  assoc_div_algebra_on S scale amult a_id a_inv +
  finite_dimensional_vector_space_on S scale basis
  for S :: ‹'b::ab_group_add set›
    and scale :: ‹'a::field ==> 'b ==> 'b›  (infixr ‹*_S› 75)
    and amult :: ‹'b==>'b==>'b›             (infixr ‹🍋› 74)
    and a_id  :: ‹'b›                   (‹1›)
    and a_inv :: ‹'b==>'b›                (*(\<open>_\<^sup>\<Zspot>\<close> 73)*)
    and basis :: ‹'b set›


lemma (in assoc_div_algebra_on) finite_dimensional_assoc_div_algebra_onI [intro]:
  fixes basis :: "'b set"
  assumes finite_Basis: "finite basis"
    and independent_Basis: "¬ m1.dependent basis"
    and span_Basis: "m1.span basis = S"
    and basis_subset: "basis ⊆ S"
  shows "finite_dimensional_assoc_div_algebra_on S scale amult a_id a_inv basis"
  by (unfold_locales, simp_all add: assms)

end