Theory Algebra_On
theory Algebra_On
imports
"HOL-Types_To_Sets.Linear_Algebra_On"
"Jacobson_Basic_Algebra.Ring_Theory"
begin
section ‹Abstract algebra locales over a \<^class>‹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 : "⟦x∈S; y∈S⟧ ⟹ (a *⇩S x) ⦁ (b *⇩S y) = (a*b) *⇩S (x ⦁ 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 \<^typ>‹'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 -
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: subset_inj_on)
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 : "∃a∈S. ∃b∈S. a≠b" if "0 ≠ 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"
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.
›
locale lie_algebra = algebra_on 𝔤 scale lie_bracket + alternating_bilinear_on 𝔤 scale lie_bracket
for 𝔤
and scale :: "'a::field ⇒ 'b::ab_group_add ⇒ 'b" (infixr ‹*⇩S› 75)
and lie_bracket :: "'b ⇒ 'b ⇒ 'b" (‹[_;_]› 74) +
assumes jacobi: "⟦x∈𝔤; y∈𝔤; z∈𝔤⟧ ⟹ 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∈𝔤" and y: "y∈𝔤" and z: "z∈𝔤"
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: "𝔥⊆𝔤" "m1.subspace 𝔥" and closed: "⋀x y. x ∈ 𝔥 ⟹ y ∈ 𝔥 ⟹ lie_bracket x y ∈ 𝔥"
shows "lie_algebra 𝔥 scale lie_bracket"
proof -
interpret 𝔥: vector_space_on 𝔥 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 𝔥.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"
and divR::"'a⇒'a⇒'a"
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(‹𝟭›)
and a_inv :: "'b⇒'b"
begin
text ‹
The definition \<^locale>‹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 \<^class>‹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› (‹𝟭›)
and a_inv :: ‹'b⇒'b›
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