Theory VS_Modules

(* Title: Examples/Vector_Spaces/VS_Modules.thy
   Author: Mihails Milehins
   Copyright 2021 (C) 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
  by (simp add: comm_ring_1_axioms ab_group_add_axioms)

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)

lemma module_pair_with_overloaded[ud_with]: 
  "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 
  unfolding module_with_overloaded
  ..

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

lemma module_hom_with_overloaded[ud_with]: 
  "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
  unfolding module_with_overloaded
  ..
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"
  by (simp add: ab_diff_conv_add_uminus add_closed' uminus_closed)

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
  by (rule tts_AB_C_transfer[OF add_closed])
    (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 
        add_cancel_right_right scale_left_distrib_on neg_eq_iff_add_eq_0 assms
    )

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
  by unfold_locales (simp_all add: closed_add closed_zero closed_uminus)

sublocale implicit⇩M: module_ow U⇩M ‹(+)› 0 ‹(-)› uminus ‹(*s)›
  by unfold_locales 
    (simp_all add: closed_scale scale_right_distrib_on scale_left_distrib_on)

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" 
    by (simp add: implicit⇩M.module_ow_axioms)
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
  for U⇩M⇩_⇩1:: "'b::ab_group_add set" 
    and U⇩M⇩_⇩2::"'c::ab_group_add set"
    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
  for U⇩M⇩_⇩1 :: "'b::ab_group_add set" and U⇩M⇩_⇩2 :: "'c::ab_group_add set"
    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
  by unfold_locales (simp_all add: hom_closed add scale)
 
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
    and implicit⇩M.ab_group_add_ow_axioms
  eliminating ‹?a ∈ U⇩M› and ‹?B ⊆ U⇩M› through auto
  applying 
    [
      OF 
        implicit⇩M.carrier_ne 
        implicit⇩M.add_closed' 
        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.

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

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.

tts_lemma span_add:
  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_add.

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.

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

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

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
    and implicit⇩M.ab_group_add_ow_axioms
  eliminating ‹?a ∈ U⇩M› and ‹?B ⊆ U⇩M› through clarsimp
  applying 
    [
      OF 
        implicit⇩M.carrier_ne
        implicit⇩M.add_closed' 
        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 M⇩1.implicit⇩M.ab_group_add_ow_axioms
    and M⇩2.implicit⇩M.ab_group_add_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.

tts_lemma module_hom_add:
  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_add.
    
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