# Theory VS_Modules

```(* Title: Examples/Vector_Spaces/VS_Modules.thy
Author: Mihails Milehins
*)
section‹Modules›
theory VS_Modules
imports
VS_Groups
Complex_Main
begin

subsection‹\<^text>‹module_with››

locale module_with = ab_group_add plus⇩M zero⇩M minus⇩M uminus⇩M
for plus⇩M :: "['m, 'm] ⇒ 'm" (infixl ‹+⇩M› 65)
and zero⇩M (‹0⇩M›)
and minus⇩M (infixl ‹-⇩M› 65)
and uminus⇩M (‹-⇩M _› [81] 80) +
fixes scale :: "['cr1::comm_ring_1, 'm] ⇒ 'm" (infixr "*s⇩w⇩i⇩t⇩h" 75)
assumes scale_right_distrib[algebra_simps]:
"a *s⇩w⇩i⇩t⇩h (x +⇩M y) = a *s⇩w⇩i⇩t⇩h x +⇩M a *s⇩w⇩i⇩t⇩h y"
and scale_left_distrib[algebra_simps]:
"(a + b) *s⇩w⇩i⇩t⇩h x = a *s⇩w⇩i⇩t⇩h x +⇩M b *s⇩w⇩i⇩t⇩h x"
and scale_scale[simp]: "a *s⇩w⇩i⇩t⇩h (b *s⇩w⇩i⇩t⇩h x) = (a * b) *s⇩w⇩i⇩t⇩h x"
and scale_one[simp]: "1 *s⇩w⇩i⇩t⇩h x = x"

lemma module_with_overloaded[ud_with]: "module = module_with (+) 0 (-) uminus"
unfolding module_def module_with_def module_with_axioms_def

locale module_pair_with =
M⇩1: module_with plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1 +
M⇩2: module_with plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
for plus⇩M⇩_⇩1 :: "['m_1, 'm_1] ⇒ 'm_1" (infixl ‹+⇩M⇩'_⇩1› 65)
and zero⇩M⇩_⇩1 (‹0⇩M⇩'_⇩1›)
and minus⇩M⇩_⇩1 (infixl ‹-⇩M⇩'_⇩1› 65)
and uminus⇩M⇩_⇩1 (‹-⇩M⇩'_⇩1 _› [81] 80)
and scale⇩1 (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩1› 75)
and plus⇩M⇩_⇩2 :: "['m_2, 'm_2] ⇒ 'm_2" (infixl ‹+⇩M⇩'_⇩2› 65)
and zero⇩M⇩_⇩2 (‹0⇩M⇩'_⇩2›)
and minus⇩M⇩_⇩2 (infixl ‹-⇩M⇩'_⇩2› 65)
and uminus⇩M⇩_⇩2 (‹-⇩M⇩'_⇩2 _› [81] 80)
and scale⇩2 (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩2› 75)

"module_pair =
(
λscale⇩1 scale⇩2.
module_pair_with (+) 0 (-) uminus scale⇩1 (+) 0 (-) uminus scale⇩2
)"
unfolding module_pair_def module_pair_with_def
..

locale module_hom_with =
M⇩1: module_with plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1 +
M⇩2: module_with plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
for plus⇩M⇩_⇩1 :: "['m_1, 'm_1] ⇒ 'm_1" (infixl ‹+⇩M⇩'_⇩1› 65)
and zero⇩M⇩_⇩1 (‹0⇩M⇩'_⇩1›)
and minus⇩M⇩_⇩1 (infixl ‹-⇩M⇩'_⇩1› 65)
and uminus⇩M⇩_⇩1 (‹-⇩M⇩'_⇩1 _› [81] 80)
and scale⇩1 (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩1› 75)
and plus⇩M⇩_⇩2 :: "['m_2, 'm_2] ⇒ 'm_2" (infixl ‹+⇩M⇩'_⇩2› 65)
and zero⇩M⇩_⇩2 (‹0⇩M⇩'_⇩2›)
and minus⇩M⇩_⇩2 (infixl ‹-⇩M⇩'_⇩2› 65)
and uminus⇩M⇩_⇩2 (‹-⇩M⇩'_⇩2 _› [81] 80)
and scale⇩2 (infixr ‹*s⇩w⇩i⇩t⇩h⇩'_⇩2› 75) +
fixes f :: "'m_1 ⇒ 'm_2"
assumes add: "f (b1 +⇩M⇩_⇩1 b2) = f b1 +⇩M⇩_⇩2 f b2"
and scale: "f (r *s⇩w⇩i⇩t⇩h⇩_⇩1 b) = r *s⇩w⇩i⇩t⇩h⇩_⇩2 f b"
begin

sublocale module_pair_with ..

end

"module_hom =
(
λscale⇩1 scale⇩2.
module_hom_with (+) 0 (-) uminus scale⇩1 (+) 0 (-) uminus scale⇩2
)"
unfolding
module_hom_def module_hom_axioms_def
module_hom_with_def module_hom_with_axioms_def
..
ud ‹module.subspace› (‹(with _ _ _ : «subspace» _)› [1000, 999, 998, 1000] 10)
ud ‹module.span› (‹(with _ _ _ : «span» _)› [1000, 999, 998, 1000] 10)
ud ‹module.dependent›
(‹(with _ _ _ _ : «dependent» _)› [1000, 999, 998, 997, 1000] 10)
ud ‹module.representation›
(
‹(with _ _ _ _ : «representation» _ _)›
[1000, 999, 998, 997, 1000, 999] 10
)

abbreviation independent_with
(‹(with _ _ _ _ : «independent» _)› [1000, 999, 998, 997, 1000] 10)
where
"(with zero⇩C⇩R⇩1 zero⇩M  scale⇩M plus⇩M : «independent» s) ≡
¬(with zero⇩C⇩R⇩1 zero⇩M scale⇩M plus⇩M : «dependent» s)"

lemma span_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"(
A ===>
(A ===> A ===> A) ===>
((=) ===> A ===> A) ===>
rel_set A ===>
rel_set A
) span.with span.with"
unfolding span.with_def
proof(intro rel_funI)
fix p p' z z' X X' and s s'::"'c ⇒ _"
assume transfer_rules[transfer_rule]:
"(A ===> A ===> A) p p'"
"A z z'"
"((=) ===> A ===> A) s s'"
"rel_set A X X'"
have "Domainp A z" using ‹A z z'› by force
have *: "t ⊆ X ⟹ (∀x∈t. Domainp A x)" for t
by (meson Domainp.DomainI ‹rel_set A X X'› rel_setD1 subsetD)
note swt = sum_with_transfer
[
OF assms(1,2,2),
THEN rel_funD,
THEN rel_funD,
THEN rel_funD,
THEN rel_funD,
OF transfer_rules(1,2)
]
have DsI: "Domainp A (sum_with p z r t)"
if "⋀x. x ∈ t ⟹ Domainp A (r x)" "t ⊆ Collect (Domainp A)" for r t
by (metis that Domainp_sum_with transfer_rules(1,2))
from Domainp_apply2I[OF transfer_rules(3)]
have Domainp_sI: "Domainp A x ⟹ Domainp A (s y x)" for x y by auto
show "rel_set A
{sum_with p z (λa. s (r a) a) t |t r. finite t ∧ t ⊆ X}
{sum_with p' z' (λa. s' (r a) a) t |t r. finite t ∧ t ⊆ X'}"
apply transfer_prover_start
apply transfer_step+
by (insert *) (auto intro!: DsI Domainp_sI)
qed

lemma dependent_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows
"(
(=) ===>
A ===>
(A ===> A ===> A) ===>
((=) ===> A ===> A) ===>
rel_set A ===>
(=)
) dependent.with dependent.with"
unfolding dependent.with_def
proof(intro rel_funI)
fix p p' z z' X X' and zb zb' ::'c and s s'::"'c ⇒ _"
assume [transfer_rule]:
"(A ===> A ===> A) p p'"
"A z z'"
"zb = zb'"
"((=) ===> A ===> A) s s'"
"rel_set A X X'"
have *: "t ⊆ X ⟹ (∀x∈t. Domainp A x)" for t
by (meson Domainp.DomainI ‹rel_set A X X'› rel_setD1 subsetD)
show
"(
∃t u.
finite t ∧
t ⊆ X ∧
sum_with p z (λv. s (u v) v) t = z ∧
(∃v∈t. u v ≠ zb)
) =
(
∃t u.
finite t ∧
t ⊆ X' ∧
sum_with p' z' (λv. s' (u v) v) t = z' ∧
(∃v∈t. u v ≠ zb')
)"
apply transfer_prover_start
apply transfer_step+
by (insert *) (auto intro!: comm_monoid_add_ow.sum_with_closed)
qed

ctr relativization
synthesis ctr_simps
assumes [transfer_rule]: "is_equality A" "bi_unique B"
trp (?'a A) and (?'b B)
in subspace_with: subspace.with_def

subsection‹‹module_ow››

subsubsection‹Definitions and common properties›

text‹Single module.›

locale module_ow = ab_group_add_ow U⇩M plus⇩M zero⇩M minus⇩M uminus⇩M
for U⇩M :: "'m set"
and plus⇩M (infixl ‹+⇩M› 65)
and zero⇩M (‹0⇩M›)
and minus⇩M (infixl ‹-⇩M› 65)
and uminus⇩M (‹-⇩M _› [81] 80) +
fixes scale :: "['cr1::comm_ring_1, 'm] ⇒ 'm" (infixr "*s⇩M" 75)
assumes scale_closed[simp, intro]: "x ∈ U⇩M ⟹ a *s⇩M x ∈ U⇩M"
and scale_right_distrib[algebra_simps]:
"⟦ x ∈ U⇩M; y ∈ U⇩M ⟧ ⟹ a *s⇩M (x +⇩M y) = a *s⇩M x +⇩M a *s⇩M y"
and scale_left_distrib[algebra_simps]:
"x ∈ U⇩M ⟹ (a + b) *s⇩M x = a *s⇩M x +⇩M b *s⇩M x"
and scale_scale[simp]:
"x ∈ U⇩M ⟹ a *s⇩M (b *s⇩M x) = (a * b) *s⇩M x"
and scale_one[simp]: "x ∈ U⇩M ⟹ 1 *s⇩M x = x"
begin

lemma scale_closed'[simp]: "∀a. ∀x∈U⇩M. a *s⇩M x ∈ U⇩M" by simp

lemma minus_closed'[simp]: "∀x∈U⇩M. ∀y∈U⇩M. x -⇩M y ∈ U⇩M"

lemma uminus_closed'[simp]: "∀x∈U⇩M. -⇩M x ∈ U⇩M" by (simp add: uminus_closed)

tts_register_sbts ‹(*s⇩M)› | U⇩M
by (rule tts_AB_C_transfer[OF scale_closed])
(auto simp: bi_unique_eq right_total_eq)

tts_register_sbts plus⇩M | U⇩M
(auto simp: bi_unique_eq right_total_eq)

tts_register_sbts zero⇩M | U⇩M
by (meson Domainp.cases zero_closed)

end

text‹Pair of modules.›

locale module_pair_ow =
M⇩1: module_ow U⇩M⇩_⇩1 plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1 +
M⇩2: module_ow U⇩M⇩_⇩2 plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
for U⇩M⇩_⇩1 :: "'m_1 set"
and plus⇩M⇩_⇩1 (infixl ‹+⇩M⇩'_⇩1› 65)
and zero⇩M⇩_⇩1 (‹0⇩M⇩'_⇩1›)
and minus⇩M⇩_⇩1 (infixl ‹-⇩M⇩'_⇩1› 65)
and uminus⇩M⇩_⇩1 (‹-⇩M⇩'_⇩1 _› [81] 80)
and scale⇩1 :: "['cr1::comm_ring_1, 'm_1] ⇒ 'm_1" (infixr ‹*s⇩M⇩'_⇩1› 75)
and U⇩M⇩_⇩2 :: "'m_2 set"
and plus⇩M⇩_⇩2 (infixl ‹+⇩M⇩'_⇩2› 65)
and zero⇩M⇩_⇩2 (‹0⇩M⇩'_⇩2›)
and minus⇩M⇩_⇩2 (infixl ‹-⇩M⇩'_⇩2› 65)
and uminus⇩M⇩_⇩2 (‹-⇩M⇩'_⇩2 _› [81] 80)
and scale⇩2 :: "['cr1::comm_ring_1, 'm_2] ⇒ 'm_2" (infixr ‹*s⇩M⇩'_⇩2› 75)

text‹Module homomorphisms.›

locale module_hom_ow =
M⇩1: module_ow U⇩M⇩_⇩1 plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1 +
M⇩2: module_ow U⇩M⇩_⇩2 plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
for U⇩M⇩_⇩1 :: "'m_1 set"
and plus⇩M⇩_⇩1 (infixl ‹+⇩M⇩'_⇩1› 65)
and zero⇩M⇩_⇩1 (‹0⇩M⇩'_⇩1›)
and minus⇩M⇩_⇩1 (infixl ‹-⇩M⇩'_⇩1› 65)
and uminus⇩M⇩_⇩1 (‹-⇩M⇩'_⇩1 _› [81] 80)
and scale⇩1 :: "['cr1::comm_ring_1, 'm_1] ⇒ 'm_1" (infixr ‹*s⇩M⇩'_⇩1› 75)
and U⇩M⇩_⇩2 :: "'m_2 set"
and plus⇩M⇩_⇩2 (infixl ‹+⇩M⇩'_⇩2› 65)
and zero⇩M⇩_⇩2 (‹0⇩M⇩'_⇩2›)
and minus⇩M⇩_⇩2 (infixl ‹-⇩M⇩'_⇩2› 65)
and uminus⇩M⇩_⇩2 (‹-⇩M⇩'_⇩2 _› [81] 80)
and scale⇩2 :: "['cr1::comm_ring_1, 'm_2] ⇒ 'm_2" (infixr ‹*s⇩M⇩'_⇩2› 75) +
fixes f :: "'m_1 ⇒ 'm_2"
assumes f_closed[simp]: "f ` U⇩M⇩_⇩1 ⊆ U⇩M⇩_⇩2"
and add: "⟦ b1 ∈ U⇩M⇩_⇩1; b2 ∈ U⇩M⇩_⇩1 ⟧ ⟹ f (b1 +⇩M⇩_⇩1 b2) = f b1 +⇩M⇩_⇩2 f b2"
and scale: "⟦ r ∈ U⇩C⇩R⇩1; b ∈ U⇩M⇩_⇩1 ⟧ ⟹ f (r *s⇩M⇩_⇩1 b) = r *s⇩M⇩_⇩2 f b"
begin

tts_register_sbts f | ‹U⇩M⇩_⇩1› and ‹U⇩M⇩_⇩2› by (rule tts_AB_transfer[OF f_closed])

lemma f_closed'[simp]: "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2" using f_closed by blast

sublocale module_pair_ow ..

end

subsubsection‹Transfer.›

lemma module_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "bi_unique B" "right_total B"
fixes PP lhs
defines
"PP ≡
(
(B ===> B ===> B) ===>
B ===>
(B ===> B ===> B) ===>
(B ===> B) ===>
((=) ===> B ===> B) ===>
(=)
)"
and
"lhs ≡
(
λ plus⇩M zero⇩M minus⇩M uminus⇩M scale.
module_ow (Collect (Domainp B)) plus⇩M zero⇩M minus⇩M uminus⇩M scale
)"
shows "PP lhs (module_with)"
proof-
let ?rhs =
"(
λplus⇩M zero⇩M minus⇩M uminus⇩M scale.
(∀a ∈ UNIV. ∀x ∈ UNIV. scale a x ∈ UNIV) ∧
module_with plus⇩M zero⇩M minus⇩M uminus⇩M scale
)"
have "PP lhs ?rhs"
unfolding
PP_def lhs_def
module_ow_def module_with_def
module_ow_axioms_def module_with_axioms_def
apply transfer_prover_start
apply transfer_step+
by (intro ext) blast
then show ?thesis by simp
qed

lemma module_pair_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]:
"bi_unique B⇩1" "right_total B⇩1" "bi_unique B⇩2" "right_total B⇩2"
fixes PP lhs
defines
"PP ≡
(
(B⇩1 ===> B⇩1 ===> B⇩1) ===>
B⇩1 ===>
(B⇩1 ===> B⇩1 ===> B⇩1) ===>
(B⇩1 ===> B⇩1) ===>
((=) ===> B⇩1 ===> B⇩1) ===>
(B⇩2 ===> B⇩2 ===> B⇩2) ===>
B⇩2 ===>
(B⇩2 ===> B⇩2 ===> B⇩2) ===>
(B⇩2 ===> B⇩2) ===>
((=) ===> B⇩2 ===> B⇩2) ===>
(=)
)"
and
"lhs ≡
(
λ
plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2.
module_pair_ow
(Collect (Domainp B⇩1)) plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
(Collect (Domainp B⇩2)) plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
)"
shows "PP lhs module_pair_with"
unfolding PP_def lhs_def
proof(intro rel_funI)
let ?rhs =
"(
λ
plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2.
(∀a ∈ UNIV. ∀x ∈ UNIV. scale⇩1 a x ∈ UNIV) ∧
(∀a ∈ UNIV. ∀x ∈ UNIV. scale⇩2 a x ∈ UNIV) ∧
module_pair_with
plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
)"
fix
plus⇩M⇩_⇩1 plus⇩M⇩_⇩1'
zero⇩M⇩_⇩1 zero⇩M⇩_⇩1'
minus⇩M⇩_⇩1 minus⇩M⇩_⇩1'
uminus⇩M⇩_⇩1 uminus⇩M⇩_⇩1'
plus⇩M⇩_⇩2 plus⇩M⇩_⇩2'
zero⇩M⇩_⇩2 zero⇩M⇩_⇩2'
minus⇩M⇩_⇩2 minus⇩M⇩_⇩2'
uminus⇩M⇩_⇩2 uminus⇩M⇩_⇩2'
and scale⇩1 :: "'f::comm_ring_1 ⇒ 'a ⇒ 'a" and scale⇩1'
and scale⇩2 :: "'f::comm_ring_1 ⇒ 'c ⇒ 'c" and scale⇩2'
assume [transfer_rule]:
"(B⇩1 ===> B⇩1 ===> B⇩1) plus⇩M⇩_⇩1 plus⇩M⇩_⇩1'"
"B⇩1 zero⇩M⇩_⇩1 zero⇩M⇩_⇩1'"
"(B⇩1 ===> B⇩1 ===> B⇩1) minus⇩M⇩_⇩1 minus⇩M⇩_⇩1'"
"(B⇩1 ===> B⇩1) uminus⇩M⇩_⇩1 uminus⇩M⇩_⇩1'"
"(B⇩2 ===> B⇩2 ===> B⇩2) plus⇩M⇩_⇩2 plus⇩M⇩_⇩2'"
"B⇩2 zero⇩M⇩_⇩2 zero⇩M⇩_⇩2'"
"(B⇩2 ===> B⇩2 ===> B⇩2) minus⇩M⇩_⇩2 minus⇩M⇩_⇩2'"
"(B⇩2 ===> B⇩2) uminus⇩M⇩_⇩2 uminus⇩M⇩_⇩2'"
"((=) ===> B⇩1 ===> B⇩1) scale⇩1 scale⇩1'"
"((=) ===> B⇩2 ===> B⇩2) scale⇩2 scale⇩2'"
show
"module_pair_ow
(Collect (Domainp B⇩1)) plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
(Collect (Domainp B⇩2)) plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
=
module_pair_with
plus⇩M⇩_⇩1' zero⇩M⇩_⇩1' minus⇩M⇩_⇩1' uminus⇩M⇩_⇩1' scale⇩1'
plus⇩M⇩_⇩2' zero⇩M⇩_⇩2' minus⇩M⇩_⇩2' uminus⇩M⇩_⇩2' scale⇩2'"
unfolding module_pair_ow_def module_pair_with_def
apply transfer_prover_start
apply transfer_step+
by simp
qed

lemma module_hom_with_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]:
"bi_unique B⇩1" "right_total B⇩1" "bi_unique B⇩2" "right_total B⇩2"
fixes PP lhs
defines
"PP ≡
(
(B⇩1 ===> B⇩1 ===> B⇩1) ===>
B⇩1 ===>
(B⇩1 ===> B⇩1 ===> B⇩1) ===>
(B⇩1 ===> B⇩1) ===>
((=) ===> B⇩1 ===> B⇩1) ===>
(B⇩2 ===> B⇩2 ===> B⇩2) ===>
B⇩2 ===>
(B⇩2 ===> B⇩2 ===> B⇩2) ===>
(B⇩2 ===> B⇩2) ===>
((=) ===> B⇩2 ===> B⇩2) ===>
(B⇩1 ===> B⇩2) ===>
(=)
)"
and
"lhs ≡
(
λ
plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
f.
module_hom_ow
(Collect (Domainp B⇩1)) plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
(Collect (Domainp B⇩2)) plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
f
)"
shows "PP lhs module_hom_with"
proof-
let ?rhs =
"(
λ
plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
f.
(∀x ∈ UNIV. f x ∈ UNIV) ∧
module_hom_with
plus⇩M⇩_⇩1 zero⇩M⇩_⇩1 minus⇩M⇩_⇩1 uminus⇩M⇩_⇩1 scale⇩1
plus⇩M⇩_⇩2 zero⇩M⇩_⇩2 minus⇩M⇩_⇩2 uminus⇩M⇩_⇩2 scale⇩2
f
)"
have "PP lhs ?rhs"
unfolding
PP_def lhs_def
module_hom_ow_def module_hom_with_def
module_hom_ow_axioms_def module_hom_with_axioms_def
apply transfer_prover_start
apply transfer_step+
by (intro ext) blast
then show ?thesis by simp
qed

subsection‹‹module_on››

subsubsection‹Definitions and common properties›

locale module_on =
fixes U⇩M
and scale :: "'a::comm_ring_1 ⇒ 'b::ab_group_add ⇒ 'b" (infixr "*s" 75)
assumes scale_right_distrib_on[algebra_simps]:
"⟦ x ∈ U⇩M; y ∈ U⇩M ⟧ ⟹ a *s (x + y) = a *s x + a *s y"
and scale_left_distrib_on[algebra_simps]:
"x ∈ U⇩M ⟹ (a + b) *s x = a *s x + b *s x"
and scale_scale_on[simp]: "x ∈ U⇩M ⟹ a *s (b *s x) = (a * b) *s x"
and scale_one_on[simp]: "x ∈ U⇩M ⟹ 1 *s x = x"
and closed_add: "⟦ x ∈ U⇩M; y ∈ U⇩M ⟧ ⟹ x + y ∈ U⇩M"
and closed_zero: "0 ∈ U⇩M"
and closed_scale: "x ∈ U⇩M ⟹ a *s x ∈ U⇩M"
begin

lemma S_ne: "U⇩M ≠ {}" using closed_zero by auto

lemma scale_minus_left_on:
assumes "x ∈ U⇩M"
shows "scale (- a) x = - scale a x"
by
(
metis
)

lemma closed_uminus:
assumes "x ∈ U⇩M"
shows "-x ∈ U⇩M"
by (metis assms closed_scale scale_minus_left_on scale_one_on)

sublocale implicit⇩M: ab_group_add_ow U⇩M ‹(+)› 0 ‹(-)› uminus

sublocale implicit⇩M: module_ow U⇩M ‹(+)› 0 ‹(-)› uminus ‹(*s)›
by unfold_locales

definition subspace :: "'b set ⇒ bool"
where subspace_on_def: "subspace T ⟷
0 ∈ T ∧ (∀x∈T. ∀y∈T. x + y ∈ T) ∧ (∀c. ∀x∈T. c *s x ∈ T)"

definition span :: "'b set ⇒ 'b set"
where span_on_def: "span b = {sum (λa. r a *s  a) t | t r. finite t ∧ t ⊆ b}"

definition dependent :: "'b set ⇒ bool"
where dependent_on_def: "dependent s ⟷
(∃t u. finite t ∧ t ⊆ s ∧ (sum (λv. u v *s v) t = 0 ∧ (∃v∈t. u v ≠ 0)))"

lemma implicit_subspace_with[tts_implicit]: "subspace.with (+) 0 (*s) = subspace"
unfolding subspace_on_def subspace.with_def ..

lemma implicit_dependent_with[tts_implicit]:
"dependent.with 0 0 (+) (*s) = dependent"
unfolding dependent_on_def dependent.with_def sum_with ..

lemma implicit_span_with[tts_implicit]: "span.with 0 (+) (*s) = span"
unfolding span_on_def span.with_def sum_with ..

end

lemma implicit_module_ow[tts_implicit]:
"module_ow U⇩M (+) 0 (-) uminus = module_on U⇩M"
proof (intro ext iffI)
fix s::"'a⇒'b⇒'b" assume "module_on U⇩M s"
then interpret module_on U⇩M s .
show "module_ow U⇩M (+) 0 (-) uminus s"
next
fix s::"'a⇒'b⇒'b" assume "module_ow U⇩M (+) 0 (-) uminus s"
then interpret module_ow U⇩M ‹(+)› 0 ‹(-)› uminus s .
show "module_on U⇩M s"
by (simp add: scale_left_distrib scale_right_distrib module_on.intro)
qed

locale module_pair_on =
M⇩1: module_on U⇩M⇩_⇩1 scale⇩1 + M⇩2: module_on U⇩M⇩_⇩2 scale⇩2
and scale⇩1::"'a::comm_ring_1 ⇒ _ ⇒ _" (infixr ‹*s⇩1› 75)
and scale⇩2::"'a::comm_ring_1 ⇒ _ ⇒ _" (infixr ‹*s⇩2› 75)
begin

sublocale implicit⇩M: module_pair_ow
U⇩M⇩_⇩1 ‹(+)› 0 ‹(-)› uminus scale⇩1 U⇩M⇩_⇩2 ‹(+)› 0 ‹(-)› uminus scale⇩2
by unfold_locales

end

lemma implicit_module_pair_ow[tts_implicit]:
"module_pair_ow U⇩M⇩_⇩1 (+) 0 (-) uminus scale⇩1 U⇩M⇩_⇩2 (+) 0 (-) uminus scale⇩2 =
module_pair_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2"
unfolding module_pair_ow_def implicit_module_ow module_pair_on_def ..

locale module_hom_on = M⇩1: module_on U⇩M⇩_⇩1 scale⇩1 + M⇩2: module_on U⇩M⇩_⇩2 scale⇩2
and scale⇩1 :: "'a::comm_ring_1 ⇒ 'b ⇒ 'b" (infixr ‹*s⇩1› 75)
and scale⇩2 :: "'a::comm_ring_1 ⇒ 'c ⇒ 'c" (infixr ‹*s⇩2› 75) +
fixes f :: "'b ⇒ 'c"
assumes hom_closed: "f ` U⇩M⇩_⇩1 ⊆ U⇩M⇩_⇩2"
and add: "⋀b1 b2. ⟦ b1 ∈ U⇩M⇩_⇩1; b2 ∈ U⇩M⇩_⇩1 ⟧ ⟹ f (b1 + b2) = f b1 + f b2"
and scale: "⋀b. b ∈ U⇩M⇩_⇩1 ⟹ f (r *s⇩1 b) = r *s⇩2 f b"
begin

sublocale module_pair_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2 by unfold_locales

sublocale implicit⇩M: module_hom_ow
U⇩M⇩_⇩1 ‹(+)› 0 ‹(-)› uminus scale⇩1 U⇩M⇩_⇩2 ‹(+)› 0 ‹(-)› uminus scale⇩2

end

lemma implicit_module_hom_ow[tts_implicit]:
"module_hom_ow U⇩M⇩_⇩1 (+) 0 (-) uminus scale⇩1 U⇩M⇩_⇩2 (+) 0 (-) uminus scale⇩2 =
module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 scale⇩1 scale⇩2"
unfolding
module_hom_ow_def
module_hom_on_def
module_hom_ow_axioms_def
module_hom_on_axioms_def
tts_implicit
by (intro ext) auto

subsection‹Relativization.›

context module_on
begin

tts_context
tts: (?'b to ‹U⇩M::'b set›)
rewriting ctr_simps
substituting implicit⇩M.module_ow_axioms
eliminating ‹?a ∈ U⇩M› and ‹?B ⊆ U⇩M› through auto
applying
[
OF
implicit⇩M.carrier_ne
implicit⇩M.minus_closed'
implicit⇩M.uminus_closed'
implicit⇩M.scale_closed',
unfolded tts_implicit
]
begin

tts_lemma scale_left_commute:
assumes "x ∈ U⇩M"
shows "a *s b *s x = b *s a *s x"
is module.scale_left_commute.

tts_lemma scale_zero_left:
assumes "x ∈ U⇩M"
shows "0 *s x = 0"
is module.scale_zero_left.

tts_lemma scale_minus_left:
assumes "x ∈ U⇩M"
shows "- a *s x = - (a *s x)"
is module.scale_minus_left.

tts_lemma scale_left_diff_distrib:
assumes "x ∈ U⇩M"
shows "(a - b) *s x = a *s x - b *s x"
is module.scale_left_diff_distrib.

tts_lemma scale_sum_left:
assumes "x ∈ U⇩M"
shows "sum f A *s x = (∑a∈A. f a *s x)"
is module.scale_sum_left.

tts_lemma scale_zero_right: "a *s 0 = 0"
is module.scale_zero_right.

tts_lemma scale_minus_right:
assumes "x ∈ U⇩M"
shows "a *s - x = - (a *s x)"
is module.scale_minus_right.

tts_lemma scale_right_diff_distrib:
assumes "x ∈ U⇩M" and "y ∈ U⇩M"
shows "a *s (x - y) = a *s x - a *s y"
is module.scale_right_diff_distrib.

tts_lemma scale_sum_right:
assumes "range f ⊆ U⇩M"
shows "a *s sum f A = (∑x∈A. a *s f x)"
is module.scale_sum_right.

tts_lemma sum_constant_scale:
assumes "y ∈ U⇩M"
shows "(∑x∈A. y) = of_nat (card A) *s y"
is module.sum_constant_scale.

tts_lemma subspace_def:
assumes "S ⊆ U⇩M"
shows "subspace S =
(0 ∈ S ∧ (∀x. ∀y∈S. x *s y ∈ S) ∧ (∀x∈S. ∀y∈S. x + y ∈ S))"
is module.subspace_def.

tts_lemma subspaceI:
assumes "S ⊆ U⇩M"
and "0 ∈ S"
and "⋀x y. ⟦x ∈ U⇩M; y ∈ U⇩M; x ∈ S; y ∈ S⟧ ⟹ x + y ∈ S"
and "⋀c x. ⟦x ∈ U⇩M; x ∈ S⟧ ⟹ c *s x ∈ S"
shows "subspace S"
is module.subspaceI.

tts_lemma subspace_single_0: "subspace {0}"
is module.subspace_single_0.

tts_lemma subspace_0:
assumes "S ⊆ U⇩M" and "subspace S"
shows "0 ∈ S"
is module.subspace_0.

assumes "S ⊆ U⇩M" and "subspace S" and "x ∈ S" and "y ∈ S"
shows "x + y ∈ S"

tts_lemma subspace_scale:
assumes "S ⊆ U⇩M" and "subspace S" and "x ∈ S"
shows "c *s x ∈ S"
is module.subspace_scale.

tts_lemma subspace_neg:
assumes "S ⊆ U⇩M" and "subspace S" and "x ∈ S"
shows "- x ∈ S"
is module.subspace_neg.

tts_lemma subspace_diff:
assumes "S ⊆ U⇩M" and "subspace S" and "x ∈ S" and "y ∈ S"
shows "x - y ∈ S"
is module.subspace_diff.

tts_lemma subspace_sum:
assumes "A ⊆ U⇩M"
and "range f ⊆ U⇩M"
and "subspace A"
and "⋀x. x ∈ B ⟹ f x ∈ A"
shows "sum f B ∈ A"
is module.subspace_sum.

tts_lemma subspace_inter:
assumes "A ⊆ U⇩M" and "B ⊆ U⇩M" and "subspace A" and "subspace B"
shows "subspace (A ∩ B)"
is module.subspace_inter.

tts_lemma span_explicit':
assumes "b ⊆ U⇩M"
shows "span b =
{
x ∈ U⇩M. ∃f.
x = (∑v∈{x ∈ U⇩M. f x ≠ 0}. f v *s v) ∧
finite {x ∈ U⇩M. f x ≠ 0} ∧
(∀x∈U⇩M. f x ≠ 0 ⟶ x ∈ b)
}"
is module.span_explicit'.

tts_lemma span_finite:
assumes "S ⊆ U⇩M" and "finite S"
shows "span S = range (λu. ∑v∈S. u v *s v)"
is module.span_finite.

tts_lemma span_induct_alt:
assumes "x ∈ U⇩M"
and "S ⊆ U⇩M"
and "x ∈ span S"
and "h 0"
and "⋀c x y. ⟦x ∈ U⇩M; y ∈ U⇩M; x ∈ S; h y⟧ ⟹ h (c *s x + y)"
shows "h x"
is module.span_induct_alt.

tts_lemma span_mono:
assumes "B ⊆ U⇩M" and "A ⊆ B"
shows "span A ⊆ span B"
is module.span_mono.

tts_lemma span_base:
assumes "S ⊆ U⇩M" and "a ∈ S"
shows "a ∈ span S"
is module.span_base.

tts_lemma span_superset:
assumes "S ⊆ U⇩M"
shows "S ⊆ span S"
is module.span_superset.

tts_lemma span_zero:
assumes "S ⊆ U⇩M"
shows "0 ∈ span S"
is module.span_zero.

assumes "x ∈ U⇩M"
and "S ⊆ U⇩M"
and "y ∈ U⇩M"
and "x ∈ span S"
and "y ∈ span S"
shows "x + y ∈ span S"

tts_lemma span_scale:
assumes "x ∈ U⇩M" and "S ⊆ U⇩M" and "x ∈ span S"
shows "c *s x ∈ span S"
is module.span_scale.

tts_lemma subspace_span:
assumes "S ⊆ U⇩M"
shows "subspace (span S)"
is module.subspace_span.

tts_lemma span_neg:
assumes "x ∈ U⇩M" and "S ⊆ U⇩M" and "x ∈ span S"
shows "- x ∈ span S"
is module.span_neg.

tts_lemma span_diff:
assumes "x ∈ U⇩M"
and "S ⊆ U⇩M"
and "y ∈ U⇩M"
and "x ∈ span S"
and "y ∈ span S"
shows "x - y ∈ span S"
is module.span_diff.

tts_lemma span_sum:
assumes "range f ⊆ U⇩M" and "S ⊆ U⇩M" and "⋀x. x ∈ A ⟹ f x ∈ span S"
shows "sum f A ∈ span S"
is module.span_sum.

tts_lemma span_minimal:
assumes "T ⊆ U⇩M" and "S ⊆ T" and "subspace T"
shows "span S ⊆ T"
is module.span_minimal.

tts_lemma span_subspace_induct:
assumes "x ∈ U⇩M"
and "S ⊆ U⇩M"
and "P ⊆ U⇩M"
and "x ∈ span S"
and "subspace P"
and "⋀x. x ∈ S ⟹ x ∈ P"
shows "x ∈ P"
given module.span_subspace_induct
by simp

tts_lemma span_induct:
assumes "x ∈ U⇩M"
and "S ⊆ U⇩M"
and "x ∈ span S"
and "subspace {x. P x ∧ x ∈ U⇩M}"
and "⋀x. x ∈ S ⟹ P x"
shows "P x"
given module.span_induct by blast

tts_lemma span_empty: "span {} = {0}"
is module.span_empty.

tts_lemma span_subspace:
assumes "B ⊆ U⇩M" and "A ⊆ B" and "B ⊆ span A" and "subspace B"
shows "span A = B"
is module.span_subspace.

tts_lemma span_span:
assumes "A ⊆ U⇩M"
shows "span (span A) = span A"
is module.span_span.

assumes "x ∈ U⇩M" and "S ⊆ U⇩M" and "y ∈ U⇩M" and "x ∈ span S"
shows "(x + y ∈ span S) = (y ∈ span S)"

assumes "y ∈ U⇩M" and "S ⊆ U⇩M" and "x ∈ U⇩M" and "y ∈ span S"
shows "(x + y ∈ span S) = (x ∈ span S)"

tts_lemma span_singleton:
assumes "x ∈ U⇩M"
shows "span {x} = range (λk. k *s x)"
is module.span_singleton.

tts_lemma span_Un:
assumes "S ⊆ U⇩M" and "T ⊆ U⇩M"
shows "span (S ∪ T) =
{x ∈ U⇩M. ∃a∈U⇩M. ∃b∈U⇩M. x = a + b ∧ a ∈ span S ∧ b ∈ span T}"
is module.span_Un.

tts_lemma span_insert:
assumes "a ∈ U⇩M" and "S ⊆ U⇩M"
shows "span (insert a S) = {x ∈ U⇩M. ∃y. x - y *s a ∈ span S}"
is module.span_insert.

tts_lemma span_breakdown:
assumes "S ⊆ U⇩M" and "a ∈ U⇩M" and "b ∈ S" and "a ∈ span S"
shows "∃x. a - x *s b ∈ span (S - {b})"
is module.span_breakdown.

tts_lemma span_breakdown_eq:
assumes "x ∈ U⇩M" and "a ∈ U⇩M" and "S ⊆ U⇩M"
shows "(x ∈ span (insert a S)) = (∃y. x - y *s a ∈ span S)"
is module.span_breakdown_eq.

tts_lemma span_clauses:
"⟦S ⊆ U⇩M; a ∈ S⟧ ⟹ a ∈ span S"
"S ⊆ U⇩M ⟹ 0 ∈ span S"
"⟦x ∈ U⇩M; S ⊆ U⇩M; y ∈ U⇩M; x ∈ span S; y ∈ span S⟧ ⟹ x + y ∈ span S"
"⟦x ∈ U⇩M; S ⊆ U⇩M; x ∈ span S⟧ ⟹ c *s x ∈ span S"
is module.span_clauses.

tts_lemma span_eq_iff:
assumes "s ⊆ U⇩M"
shows "(span s = s) = subspace s"
is module.span_eq_iff.

tts_lemma span_eq:
assumes "S ⊆ U⇩M" and "T ⊆ U⇩M"
shows "(span S = span T) = (S ⊆ span T ∧ T ⊆ span S)"
is module.span_eq.

tts_lemma eq_span_insert_eq:
assumes "x ∈ U⇩M" and "y ∈ U⇩M" and "S ⊆ U⇩M" and "x - y ∈ span S"
shows "span (insert x S) = span (insert y S)"
is module.eq_span_insert_eq.

tts_lemma dependent_mono:
assumes "A ⊆ U⇩M" and "dependent B" and "B ⊆ A"
shows "dependent A"
is module.dependent_mono.

tts_lemma independent_mono:
assumes "A ⊆ U⇩M" and "¬ dependent A" and "B ⊆ A"
shows "¬ dependent B"
is module.independent_mono.

tts_lemma dependent_zero:
assumes "A ⊆ U⇩M" and "0 ∈ A"
shows "dependent A"
is module.dependent_zero.

tts_lemma independent_empty: "¬ dependent {}"
is module.independent_empty.

tts_lemma independentD:
assumes "s ⊆ U⇩M"
and "¬ dependent s"
and "finite t"
and "t ⊆ s"
and "(∑v∈t. u v *s v) = 0"
and "v ∈ t"
shows "u v = 0"
is module.independentD.

tts_lemma independent_Union_directed:
assumes "C ⊆ Pow U⇩M"
and "⋀c d. ⟦c ⊆ U⇩M; d ⊆ U⇩M; c ∈ C; d ∈ C⟧ ⟹ c ⊆ d ∨ d ⊆ c"
and "⋀c. ⟦c ⊆ U⇩M; c ∈ C⟧ ⟹ ¬ dependent c"
shows "¬ dependent (⋃ C)"
is module.independent_Union_directed.

tts_lemma dependent_finite:
assumes "S ⊆ U⇩M" and "finite S"
shows "dependent S = (∃x. (∃y∈S. x y ≠ 0) ∧ (∑v∈S. x v *s v) = 0)"
is module.dependent_finite.

tts_lemma independentD_alt:
assumes "B ⊆ U⇩M"
and "x ∈ U⇩M"
and "¬ dependent B"
and "finite {x ∈ U⇩M. X x ≠ 0}"
and "{x ∈ U⇩M. X x ≠ 0} ⊆ B"
and "(∑x | x ∈ U⇩M ∧ X x ≠ 0. X x *s x) = 0"
shows "X x = 0"
is module.independentD_alt.

tts_lemma spanning_subset_independent:
assumes "A ⊆ U⇩M" and "B ⊆ A" and "¬ dependent A" and "A ⊆ span B"
shows "A = B"
is module.spanning_subset_independent.

tts_lemma unique_representation:
assumes "basis ⊆ U⇩M"
and "¬ dependent basis"
and "⋀v. ⟦v ∈ U⇩M; f v ≠ 0⟧ ⟹ v ∈ basis"
and "⋀v. ⟦v ∈ U⇩M; g v ≠ 0⟧ ⟹ v ∈ basis"
and "finite {x ∈ U⇩M. f x ≠ 0}"
and "finite {x ∈ U⇩M. g x ≠ 0}"
and
"(∑v∈{x ∈ U⇩M. f x ≠ 0}. f v *s v) = (∑v∈{x ∈ U⇩M. g x ≠ 0}. g v *s v)"
shows "∀x∈U⇩M. f x = g x"
is module.unique_representation[unfolded fun_eq_iff].

tts_lemma independentD_unique:
assumes "B ⊆ U⇩M"
and "¬ dependent B"
and "finite {x ∈ U⇩M. X x ≠ 0}"
and "{x ∈ U⇩M. X x ≠ 0} ⊆ B"
and "finite {x ∈ U⇩M. Y x ≠ 0}"
and "{x ∈ U⇩M. Y x ≠ 0} ⊆ B"
and "(∑x | x ∈ U⇩M ∧ X x ≠ 0. X x *s x) =
(∑x | x ∈ U⇩M ∧ Y x ≠ 0. Y x *s x)"
shows "∀x∈U⇩M. X x = Y x"
is module.independentD_unique[unfolded fun_eq_iff].

tts_lemma subspace_UNIV: "subspace U⇩M"
is module.subspace_UNIV.

tts_lemma span_UNIV: "span U⇩M = U⇩M"
is module.span_UNIV.

tts_lemma span_alt:
assumes "B ⊆ U⇩M"
shows
"span B =
{
x ∈ U⇩M. ∃f.
x = (∑x | x ∈ U⇩M ∧ f x ≠ 0. f x *s x) ∧
finite {x ∈ U⇩M. f x ≠ 0} ∧
{x ∈ U⇩M. f x ≠ 0} ⊆ B
}"
is module.span_alt.

tts_lemma dependent_alt:
assumes "B ⊆ U⇩M"
shows "dependent B =
(
∃f.
finite {v ∈ U⇩M. f v ≠ 0} ∧
{v ∈ U⇩M. f v ≠ 0} ⊆ B ∧
(∃v∈U⇩M. f v ≠ 0) ∧
(∑x | x ∈ U⇩M ∧ f x ≠ 0. f x *s x) = 0
)"
is module.dependent_alt.

tts_lemma independent_alt:
assumes "B ⊆ U⇩M"
shows
"(¬ dependent B) =
(
∀f.
finite {x ∈ U⇩M. f x ≠ 0} ⟶
{x ∈ U⇩M. f x ≠ 0} ⊆ B ⟶
(∑x | x ∈ U⇩M ∧ f x ≠ 0. f x *s x) = 0 ⟶
(∀x∈U⇩M. f x = 0)
)"
is module.independent_alt.

tts_lemma subspace_Int:
assumes "range s ⊆ Pow U⇩M" and "⋀i. i ∈ I ⟹ subspace (s i)"
shows "subspace (⋂ (s ` I) ∩ U⇩M)"
is module.subspace_Int.

tts_lemma subspace_Inter:
assumes "f ⊆ Pow U⇩M" and "Ball f subspace"
shows "subspace (⋂ f ∩ U⇩M)"
is module.subspace_Inter.

tts_lemma module_hom_scale_self: "module_hom_on U⇩M U⇩M (*s) (*s) ((*s) c)"
is module.module_hom_scale_self.

tts_lemma module_hom_scale_left:
assumes "x ∈ U⇩M"
shows "module_hom_on UNIV U⇩M (*) (*s) (λr. r *s x)"
is module.module_hom_scale_left.

tts_lemma module_hom_id: "module_hom_on U⇩M U⇩M (*s) (*s) id"
is module.module_hom_id.

tts_lemma module_hom_ident: "module_hom_on U⇩M U⇩M (*s) (*s) (λx. x)"
is module.module_hom_ident.

tts_lemma module_hom_uminus: "module_hom_on U⇩M U⇩M (*s) (*s) uminus"
is module.module_hom_uminus.

end

tts_context
tts: (?'b to ‹U⇩M::'b set›)
rewriting ctr_simps
substituting implicit⇩M.module_ow_axioms
eliminating ‹?a ∈ U⇩M› and ‹?B ⊆ U⇩M› through clarsimp
applying
[
OF
implicit⇩M.carrier_ne
implicit⇩M.minus_closed'
implicit⇩M.uminus_closed'
implicit⇩M.scale_closed',
unfolded tts_implicit
]
begin

tts_lemma span_explicit:
assumes "b ⊆ U⇩M"
shows "span b =
{x ∈ U⇩M. ∃y⊆U⇩M. ∃f. (finite y ∧ y ⊆ b) ∧ x = (∑a∈y. f a *s a)}"
given module.span_explicit by auto

tts_lemma span_unique:
assumes "S ⊆ U⇩M"
and "T ⊆ U⇩M"
and "S ⊆ T"
and "subspace T"
and "⋀T'. ⟦T' ⊆ U⇩M; S ⊆ T'; subspace T'⟧ ⟹ T ⊆ T'"
shows "span S = T"
is module.span_unique.

tts_lemma dependent_explicit:
assumes "V ⊆ U⇩M"
shows "dependent V =
(∃U⊆U⇩M. ∃f. finite U ∧ U ⊆ V ∧ (∃v∈U. f v ≠ 0) ∧ (∑v∈U. f v *s v) = 0)"
given module.dependent_explicit by auto

tts_lemma independent_explicit_module:
assumes "V ⊆ U⇩M"
shows "(¬ dependent V) =
(
∀U⊆U⇩M. ∀f. ∀v∈U⇩M.
finite U ⟶
U ⊆ V ⟶
(∑u∈U. f u *s u) = 0 ⟶
v ∈ U ⟶
f v = 0
)"
given module.independent_explicit_module by auto

end

end

context module_pair_on
begin

tts_context
tts: (?'b to ‹U⇩M⇩_⇩1::'b set›) and (?'c to ‹U⇩M⇩_⇩2::'c set›)
rewriting ctr_simps
substituting M⇩1.implicit⇩M.module_ow_axioms
and M⇩2.implicit⇩M.module_ow_axioms
and implicit⇩M.module_pair_ow_axioms
eliminating through auto
applying [unfolded tts_implicit]
begin

tts_lemma module_hom_zero: "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. 0)"
is module_pair.module_hom_zero.

assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
shows "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. f x + g x)"

tts_lemma module_hom_sub:
assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
shows "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. f x - g x)"
is module_pair.module_hom_sub.

tts_lemma module_hom_neg:
assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2" and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
shows "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. - f x)"
is module_pair.module_hom_neg.

tts_lemma module_hom_scale:
assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2" and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
shows "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. c *s⇩2 f x)"
is module_pair.module_hom_scale.

tts_lemma module_hom_compose_scale:
assumes "c ∈ U⇩M⇩_⇩2" and "module_hom_on U⇩M⇩_⇩1 UNIV (*s⇩1) (*) f"
shows "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. f x *s⇩2 c)"
is module_pair.module_hom_compose_scale.

tts_lemma module_hom_sum:
assumes "∀u. ∀v∈U⇩M⇩_⇩1. f u v ∈ U⇩M⇩_⇩2"
and "⋀i. i ∈ I ⟹ module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (f i)"
and "I = {} ⟹ module_on U⇩M⇩_⇩1 (*s⇩1) ∧ module_on U⇩M⇩_⇩2 (*s⇩2)"
shows "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) (λx. ∑i∈I. f i x)"
is module_pair.module_hom_sum.

tts_lemma module_hom_eq_on_span:
assumes "∀x∈U⇩M⇩_⇩1. f x ∈ U⇩M⇩_⇩2"
and "∀x∈U⇩M⇩_⇩1. g x ∈ U⇩M⇩_⇩2"
and "B ⊆ U⇩M⇩_⇩1"
and "x ∈ U⇩M⇩_⇩1"
and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) f"
and "module_hom_on U⇩M⇩_⇩1 U⇩M⇩_⇩2 (*s⇩1) (*s⇩2) g"
and "⋀x. ⟦x ∈ U⇩M⇩_⇩1; x ∈ B⟧ ⟹ f x = g x"
and "x ∈ M⇩1.span B"
shows "f x = g x"
is module_pair.module_hom_eq_on_span.

end

end

text‹\newpage›

end```