# Theory Weak_Morphisms

```(*  Title:      HOL/Algebra/Weak_Morphisms.thy
Author:     Paulo Emílio de Vilhena
*)

theory Weak_Morphisms
imports QuotRing

begin

section ‹Weak Morphisms›

text ‹The definition of ring isomorphism, as well as the definition of group isomorphism, doesn't
enforce any algebraic constraint to the structure of the schemes involved. This seems
unnatural, but it turns out to be very useful: in order to prove that a scheme B satisfy
certain algebraic constraints, it's sufficient to prove those for a scheme A and show
the existence of an isomorphism between A and B. In this section, we explore this idea
in a different way: given a scheme A and a function f, we build a scheme B with an
algebraic structure of same strength as A where f is an homomorphism from A to B.›

subsection ‹Definitions›

locale weak_group_morphism = normal H G for f and H and G (structure) +
assumes inj_mod_subgroup: "⟦ a ∈ carrier G; b ∈ carrier G ⟧ ⟹ f a = f b ⟷ a ⊗ (inv b) ∈ H"

locale weak_ring_morphism = ideal I R for f and I and R (structure) +
assumes inj_mod_ideal: "⟦ a ∈ carrier R; b ∈ carrier R ⟧ ⟹ f a = f b ⟷ a ⊖ b ∈ I"

definition image_group :: "('a ⇒ 'b) ⇒ ('a, 'c) monoid_scheme ⇒ 'b monoid"
where "image_group f G ≡
⦇ carrier = f ` (carrier G),
mult = (λa b. f ((inv_into (carrier G) f a) ⊗⇘G⇙ (inv_into (carrier G) f b))),
one = f 𝟭⇘G⇙ ⦈"

definition image_ring :: "('a ⇒ 'b) ⇒ ('a, 'c) ring_scheme ⇒ 'b ring"
where "image_ring f R ≡ monoid.extend (image_group f R)
⦇ zero = f 𝟬⇘R⇙,
add = (λa b. f ((inv_into (carrier R) f a) ⊕⇘R⇙ (inv_into (carrier R) f b))) ⦈"

subsection ‹Weak Group Morphisms›

lemma image_group_carrier: "carrier (image_group f G) = f ` (carrier G)"
unfolding image_group_def by simp

lemma image_group_one: "one (image_group f G) = f 𝟭⇘G⇙"
unfolding image_group_def by simp

lemma weak_group_morphismsI:
assumes "H ⊲ G" and "⋀a b. ⟦ a ∈ carrier G; b ∈ carrier G ⟧ ⟹ f a = f b ⟷ a ⊗⇘G⇙ (inv⇘G⇙ b) ∈ H"
shows "weak_group_morphism f H G"
using assms unfolding weak_group_morphism_def weak_group_morphism_axioms_def by auto

lemma image_group_truncate:
fixes R :: "('a, 'b) monoid_scheme"
shows "monoid.truncate (image_group f R) = image_group f (monoid.truncate R)"

lemma image_ring_truncate: "monoid.truncate (image_ring f R) = image_group f R"

assumes "weak_ring_morphism f I R" shows "weak_group_morphism f I (add_monoid R)"
proof -
have is_normal: "I ⊲ (add_monoid R)"
using ideal_is_normal[OF  weak_ring_morphism.axioms(1)[OF assms]] .
show ?thesis
using weak_group_morphism.intro[OF is_normal]
weak_ring_morphism.inj_mod_ideal[OF assms]
unfolding weak_group_morphism_axioms_def a_minus_def a_inv_def
by auto
qed

lemma (in group) weak_group_morphism_range:
assumes "weak_group_morphism f H G" and "a ∈ carrier G" shows "f ` (H #> a) = { f a }"
proof -
interpret H: subgroup H G
using weak_group_morphism.axioms(1)[OF assms(1)] unfolding normal_def by simp
show ?thesis
proof
show "{ f a } ⊆ f ` (H #> a)"
using H.one_closed assms(2) unfolding r_coset_def by force
next
show "f ` (H #> a) ⊆ { f a }"
proof
fix b assume "b ∈ f ` (H #> a)" then obtain h where "h ∈ H" "h ∈ carrier G" "b = f (h ⊗ a)"
unfolding r_coset_def using H.subset by auto
thus "b ∈ { f a }"
using weak_group_morphism.inj_mod_subgroup[OF assms(1)] assms(2)
by (metis inv_solve_right m_closed singleton_iff)
qed
qed
qed

lemma (in group) vimage_eq_rcoset:
assumes "weak_group_morphism f H G" and "a ∈ carrier G"
shows "{ b ∈ carrier G. f b = f a } = H #> a" and "{ b ∈ carrier G. f b = f a } = a <# H"
proof -
interpret H: normal H G
using weak_group_morphism.axioms(1)[OF assms(1)] by simp
show "{ b ∈ carrier G. f b = f a } = H #> a"
proof
show "H #> a ⊆ { b ∈ carrier G. f b = f a }"
using r_coset_subset_G[OF H.subset assms(2)] weak_group_morphism_range[OF assms] by auto
next
show "{ b ∈ carrier G. f b = f a } ⊆ H #> a"
proof
fix b assume b: "b ∈ { b ∈ carrier G. f b = f a }" then obtain h where "h ∈ H" "b ⊗ (inv a) = h"
using weak_group_morphism.inj_mod_subgroup[OF assms(1)] assms(2) by fastforce
thus "b ∈ H #> a"
using H.rcos_module[OF is_group] b assms(2) by blast
qed
qed
thus "{ b ∈ carrier G. f b = f a } = a <# H"
qed

lemma (in group) weak_group_morphism_ker:
assumes "weak_group_morphism f H G" shows "kernel G (image_group f G) f = H"
using vimage_eq_rcoset(1)[OF assms one_closed] weak_group_morphism.axioms(1)[OF assms(1)]
by (simp add: image_group_def kernel_def normal_def subgroup.subset)

lemma (in group) weak_group_morphism_inv_into:
assumes "weak_group_morphism f H G" and "a ∈ carrier G"
obtains h h' where "h  ∈ H" "inv_into (carrier G) f (f a) = h ⊗ a"
and "h' ∈ H" "inv_into (carrier G) f (f a) = a ⊗ h'"
proof -
have "inv_into (carrier G) f (f a) ∈ { b ∈ carrier G. f b = f a }"
using assms(2) by (auto simp add: inv_into_into f_inv_into_f)
thus thesis
using that vimage_eq_rcoset[OF assms] unfolding r_coset_def l_coset_def by blast
qed

proposition (in group) weak_group_morphism_is_iso:
assumes "weak_group_morphism f H G" shows "(λx. the_elem (f ` x)) ∈ iso (G Mod H) (image_group f G)"
proof (auto simp add: iso_def hom_def image_group_def)
interpret H: normal H G
using weak_group_morphism.axioms(1)[OF assms] .

show "⋀x. x ∈ carrier (G Mod H) ⟹ the_elem (f ` x) ∈ f ` carrier G"
unfolding FactGroup_def RCOSETS_def using weak_group_morphism_range[OF assms] by auto

thus  "bij_betw (λx. the_elem (f ` x)) (carrier (G Mod H)) (f ` carrier G)"
unfolding bij_betw_def
proof (auto)
fix a assume "a ∈ carrier G"
hence "the_elem (f ` (H #> a)) = f a" and "H #> a ∈ carrier (G Mod H)"
using weak_group_morphism_range[OF assms] unfolding FactGroup_def RCOSETS_def by auto
thus "f a ∈ (λx. the_elem (f ` x)) ` carrier (G Mod H)"
using image_iff by fastforce
next
show "inj_on (λx. the_elem (f ` x)) (carrier (G Mod H))"
proof (rule inj_onI)
fix x y assume "x ∈ (carrier (G Mod H))" and "y ∈ (carrier (G Mod H))"
then obtain a b where a: "a ∈ carrier G" "x = H #> a" and b: "b ∈ carrier G" "y = H #> b"
unfolding FactGroup_def RCOSETS_def by auto
assume "the_elem (f ` x) = the_elem (f ` y)"
hence "a ⊗ (inv b) ∈ H"
using weak_group_morphism.inj_mod_subgroup[OF assms]
weak_group_morphism_range[OF assms] a b by auto
thus "x = y"
using a(1) b(1) unfolding a b
by (meson H.rcos_const H.subset group.coset_mult_inv1 is_group)
qed
qed

fix x y assume "x ∈ carrier (G Mod H)" "y ∈ carrier (G Mod H)"
then obtain a b where a: "a ∈ carrier G" "x = H #> a" and b: "b ∈ carrier G" "y = H #> b"
unfolding FactGroup_def RCOSETS_def by auto

show "the_elem (f ` (x <#> y)) = f (inv_into (carrier G) f (the_elem (f ` x)) ⊗
inv_into (carrier G) f (the_elem (f ` y)))"
proof (simp add: weak_group_morphism_range[OF assms] a b)
obtain h1 h2
where h1: "h1 ∈ H" "inv_into (carrier G) f (f a) = a ⊗ h1"
and h2: "h2 ∈ H" "inv_into (carrier G) f (f b) = h2 ⊗ b"
using weak_group_morphism_inv_into[OF assms] a(1) b(1) by metis
have "the_elem (f ` ((H #> a) <#> (H #> b))) = the_elem (f ` (H #> (a ⊗ b)))"
by (simp add: a b H.rcos_sum)
hence "the_elem (f ` ((H #> a) <#> (H #> b))) = f (a ⊗ b)"
using weak_group_morphism_range[OF assms] a(1) b(1) by auto
moreover
have "(a ⊗ h1) ⊗ (h2 ⊗ b) = a ⊗ (h1 ⊗ h2 ⊗ b)"
by (simp add: a(1) b(1) h1(1) h2(1) H.subset m_assoc)
hence "(a ⊗ h1) ⊗ (h2 ⊗ b) ∈ a <# (H #> b)"
using h1(1) h2(1) unfolding l_coset_def r_coset_def by auto
hence "(a ⊗ h1) ⊗ (h2 ⊗ b) ∈ (a ⊗ b) <# H"
by (simp add: H.subset H.coset_eq a(1) b(1) lcos_m_assoc)
hence "f (inv_into (carrier G) f (f a) ⊗ inv_into (carrier G) f (f b)) = f (a ⊗ b)"
using vimage_eq_rcoset(2)[OF assms] a(1) b(1) unfolding h1 h2 by auto
ultimately
show "the_elem (f ` ((H #> a) <#> (H #> b))) = f (inv_into (carrier G) f (f a) ⊗
inv_into (carrier G) f (f b))"
by simp
qed
qed

corollary (in group) image_group_is_group:
assumes "weak_group_morphism f H G" shows "group (image_group f G)"
proof -
interpret H: normal H G
using weak_group_morphism.axioms(1)[OF assms] .

have "group ((image_group f G) ⦇ one := the_elem (f ` 𝟭⇘G Mod H⇙) ⦈)"
using group.iso_imp_img_group[OF H.factorgroup_is_group weak_group_morphism_is_iso[OF assms]] .
moreover have "𝟭⇘G Mod H⇙ = H #> 𝟭"
unfolding FactGroup_def using H.subset by force
hence "the_elem (f ` 𝟭⇘G Mod H⇙) = f 𝟭"
using weak_group_morphism_range[OF assms one_closed] by simp
ultimately show ?thesis by (simp add: image_group_def)
qed

corollary (in group) weak_group_morphism_is_hom:
assumes "weak_group_morphism f H G" shows "f ∈ hom G (image_group f G)"
proof -
interpret H: normal H G
using weak_group_morphism.axioms(1)[OF assms] .

have the_elem_hom: "(λx. the_elem (f ` x)) ∈ hom (G Mod H) (image_group f G)"
using weak_group_morphism_is_iso[OF assms] by (simp add: iso_def)
have hom: "(λx. the_elem (f ` x)) ∘ (#>) H ∈ hom G (image_group f G)"
using hom_compose[OF H.r_coset_hom_Mod the_elem_hom]
using Group.hom_compose H.r_coset_hom_Mod the_elem_hom by blast
have restrict: "⋀a. a ∈ carrier G ⟹ ((λx. the_elem (f ` x)) ∘ (#>) H) a = f a"
using weak_group_morphism_range[OF assms] by auto
show ?thesis
using hom_restrict[OF hom restrict] by simp
qed

corollary (in group) weak_group_morphism_group_hom:
assumes "weak_group_morphism f H G" shows "group_hom G (image_group f G) f"
using image_group_is_group[OF assms] weak_group_morphism_is_hom[OF assms] group_axioms
unfolding group_hom_def group_hom_axioms_def by simp

subsection ‹Weak Ring Morphisms›

lemma image_ring_carrier: "carrier (image_ring f R) = f ` (carrier R)"
unfolding image_ring_def image_group_def by (simp add: monoid.defs)

lemma image_ring_one: "one (image_ring f R) = f 𝟭⇘R⇙"
unfolding image_ring_def image_group_def by (simp add: monoid.defs)

lemma image_ring_zero: "zero (image_ring f R) = f 𝟬⇘R⇙"
unfolding image_ring_def image_group_def by (simp add: monoid.defs)

lemma weak_ring_morphismI:
assumes "ideal I R" and "⋀a b. ⟦ a ∈ carrier R; b ∈ carrier R ⟧ ⟹ f a = f b ⟷ a ⊖⇘R⇙ b ∈ I"
shows "weak_ring_morphism f I R"
using assms unfolding weak_ring_morphism_def weak_ring_morphism_axioms_def by auto

lemma (in ring) weak_ring_morphism_range:
assumes "weak_ring_morphism f I R" and "a ∈ carrier R" shows "f ` (I +> a) = { f a }"
unfolding a_r_coset_def .

lemma (in ring) vimage_eq_a_rcoset:
assumes "weak_ring_morphism f I R" and "a ∈ carrier R" shows "{ b ∈ carrier R. f b = f a } = I +> a"
unfolding a_r_coset_def by simp

lemma (in ring) weak_ring_morphism_ker:
assumes "weak_ring_morphism f I R" shows "a_kernel R (image_ring f R) f = I"
unfolding kernel_def a_kernel_def' image_ring_def image_group_def by (simp add: monoid.defs)

lemma (in ring) weak_ring_morphism_inv_into:
assumes "weak_ring_morphism f I R" and "a ∈ carrier R"
obtains i where "i ∈ I" "inv_into (carrier R) f (f a) = i ⊕ a"

proposition (in ring) weak_ring_morphism_is_iso:
assumes "weak_ring_morphism f I R" shows "(λx. the_elem (f ` x)) ∈ ring_iso (R Quot I) (image_ring f R)"
proof (rule ring_iso_memI)
show "bij_betw (λx. the_elem (f ` x)) (carrier (R Quot I)) (carrier (image_ring f R))"
and add_hom: "⋀x y. ⟦ x ∈ carrier (R Quot I); y ∈ carrier (R Quot I) ⟧ ⟹
the_elem (f ` (x ⊕⇘R Quot I⇙ y)) = the_elem (f ` x) ⊕⇘image_ring f R⇙ the_elem (f ` y)"
unfolding iso_def hom_def FactGroup_def FactRing_def A_RCOSETS_def set_add_def
by (auto simp add: image_ring_def image_group_def monoid.defs)
next
interpret I: ideal I R
using weak_ring_morphism.axioms(1)[OF assms] .

show "the_elem (f ` 𝟭⇘R Quot I⇙) = 𝟭⇘image_ring f R⇙"
and "⋀x. x ∈ carrier (R Quot I) ⟹ the_elem (f ` x) ∈ carrier (image_ring f R)"
using weak_ring_morphism_range[OF assms] one_closed I.Icarr
by (auto simp add: image_ring_def image_group_def monoid.defs FactRing_def A_RCOSETS_def')

fix x y assume "x ∈ carrier (R Quot I)" "y ∈ carrier (R Quot I)"
then obtain a b where a: "a ∈ carrier R" "x = I +> a" and b: "b ∈ carrier R" "y = I +> b"
unfolding FactRing_def A_RCOSETS_def' by auto
hence prod: "x ⊗⇘R Quot I⇙ y = I +> (a ⊗ b)"

show "the_elem (f ` (x ⊗⇘R Quot I⇙ y)) = the_elem (f ` x) ⊗⇘image_ring f R⇙ the_elem (f ` y)"
unfolding prod
proof (simp add: weak_ring_morphism_range[OF assms] a b image_ring_def image_group_def monoid.defs)
obtain i j
where i: "i ∈ I" "inv_into (carrier R) f (f a) = i ⊕ a"
and j: "j ∈ I" "inv_into (carrier R) f (f b) = j ⊕ b"
using weak_ring_morphism_inv_into[OF assms] a(1) b(1) by metis
have "i ∈ carrier R" and "j ∈ carrier R"
using I.Icarr i(1) j(1) by auto
hence "(i ⊕ a) ⊗ (j ⊕ b) = (i ⊕ a) ⊗ j ⊕ (i ⊗ b) ⊕ (a ⊗ b)"
using a(1) b(1) by algebra
hence "(i ⊕ a) ⊗ (j ⊕ b) ∈ I +> (a ⊗ b)"
using i(1) j(1) a(1) b(1) unfolding a_r_coset_def'
thus "f (a ⊗ b) = f (inv_into (carrier R) f (f a) ⊗ inv_into (carrier R) f (f b))"
unfolding i j using weak_ring_morphism_range[OF assms m_closed[OF a(1) b(1)]]
by (metis imageI singletonD)
qed
qed

corollary (in ring) image_ring_zero':
assumes "weak_ring_morphism f I R" shows "the_elem (f ` 𝟬⇘R Quot I⇙) = 𝟬⇘image_ring f R⇙"
proof -
interpret I: ideal I R
using weak_ring_morphism.axioms(1)[OF assms] .

have "𝟬⇘R Quot I⇙ = I +> 𝟬"
unfolding FactRing_def a_r_coset_def' by force
thus ?thesis
using weak_ring_morphism_range[OF assms zero_closed] unfolding image_ring_zero by simp
qed

corollary (in ring) image_ring_is_ring:
assumes "weak_ring_morphism f I R" shows "ring (image_ring f R)"
proof -
interpret I: ideal I R
using weak_ring_morphism.axioms(1)[OF assms] .

have "ring ((image_ring f R) ⦇ zero := the_elem (f ` 𝟬⇘R Quot I⇙) ⦈)"
using ring.ring_iso_imp_img_ring[OF I.quotient_is_ring weak_ring_morphism_is_iso[OF assms]] by simp
thus ?thesis
unfolding image_ring_zero'[OF assms] by simp
qed

corollary (in ring) image_ring_is_field:
assumes "weak_ring_morphism f I R" and "field (R Quot I)" shows "field (image_ring f R)"
using field.ring_iso_imp_img_field[OF assms(2) weak_ring_morphism_is_iso[OF assms(1)]]
unfolding image_ring_zero'[OF assms(1)] by simp

corollary (in ring) weak_ring_morphism_is_hom:
assumes "weak_ring_morphism f I R" shows "f ∈ ring_hom R (image_ring f R)"
proof -
interpret I: ideal I R
using weak_ring_morphism.axioms(1)[OF assms] .

have the_elem_hom: "(λx. the_elem (f ` x)) ∈ ring_hom (R Quot I) (image_ring f R)"
using weak_ring_morphism_is_iso[OF assms] by (simp add: ring_iso_def)
have ring_hom: "(λx. the_elem (f ` x)) ∘ (+>) I ∈ ring_hom R (image_ring f R)"
using ring_hom_trans[OF I.rcos_ring_hom the_elem_hom] .
have restrict: "⋀a. a ∈ carrier R ⟹ ((λx. the_elem (f ` x)) ∘ (+>) I) a = f a"
using weak_ring_morphism_range[OF assms] by auto
show ?thesis
using ring_hom_restrict[OF ring_hom restrict] by simp
qed

corollary (in ring) weak_ring_morphism_ring_hom:
assumes "weak_ring_morphism f I R" shows "ring_hom_ring R (image_ring f R) f"
using ring_hom_ringI2[OF ring_axioms image_ring_is_ring[OF assms] weak_ring_morphism_is_hom[OF assms]] .

subsection ‹Injective Functions›

text ‹If the fuction is injective, we don't need to impose any algebraic restriction to the input
scheme in order to state an isomorphism.›

lemma inj_imp_image_group_iso:
assumes "inj_on f (carrier G)" shows "f ∈ iso G (image_group f G)"
using assms by (auto simp add: image_group_def iso_def bij_betw_def hom_def)

lemma inj_imp_image_group_inv_iso:
assumes "inj f" shows "Hilbert_Choice.inv f ∈ iso (image_group f G) G"
using assms by (auto simp add: image_group_def iso_def bij_betw_def hom_def inj_on_def)

lemma inj_imp_image_ring_iso:
assumes "inj_on f (carrier R)" shows "f ∈ ring_iso R (image_ring f R)"
using assms by (auto simp add: image_ring_def image_group_def ring_iso_def
bij_betw_def ring_hom_def monoid.defs)

lemma inj_imp_image_ring_inv_iso:
assumes "inj f" shows "Hilbert_Choice.inv f ∈ ring_iso (image_ring f R) R"
using assms by (auto simp add: image_ring_def image_group_def ring_iso_def
bij_betw_def ring_hom_def inj_on_def monoid.defs)

lemma (in group) inj_imp_image_group_is_group:
assumes "inj_on f (carrier G)" shows "group (image_group f G)"
using iso_imp_img_group[OF inj_imp_image_group_iso[OF assms]] by (simp add: image_group_def)

lemma (in ring) inj_imp_image_ring_is_ring:
assumes "inj_on f (carrier R)" shows "ring (image_ring f R)"
using ring_iso_imp_img_ring[OF inj_imp_image_ring_iso[OF assms]]
by (simp add: image_ring_def image_group_def monoid.defs)

lemma (in domain) inj_imp_image_ring_is_domain:
assumes "inj_on f (carrier R)" shows "domain (image_ring f R)"
using ring_iso_imp_img_domain[OF inj_imp_image_ring_iso[OF assms]]
by (simp add: image_ring_def image_group_def monoid.defs)

lemma (in field) inj_imp_image_ring_is_field:
assumes "inj_on f (carrier R)" shows "field (image_ring f R)"
using ring_iso_imp_img_field[OF inj_imp_image_ring_iso[OF assms]]
by (simp add: image_ring_def image_group_def monoid.defs)

section ‹Examples›

text ‹In a lot of different contexts, the lack of dependent types make some definitions quite
complicated. The tools developed in this theory give us a way to change the type of a
scheme and preserve all of its algebraic properties. We show, in this section, how to
make use of this feature in order to solve the problem mentioned above. ›

subsection ‹Direct Product›

abbreviation nil_monoid :: "('a list) monoid"
where "nil_monoid ≡ ⦇ carrier = { [] }, mult = (λa b. []), one = [] ⦈"

definition DirProd_list :: "(('a, 'b) monoid_scheme) list ⇒ ('a list) monoid"
where "DirProd_list Gs = foldr (λG H. image_group (λ(x, xs). x # xs) (G ×× H)) Gs nil_monoid"

subsubsection ‹Basic Properties›

lemma DirProd_list_carrier:
shows "carrier (DirProd_list (G # Gs)) = (λ(x, xs). x # xs) ` (carrier G × carrier (DirProd_list Gs))"
unfolding DirProd_list_def image_group_def by auto

lemma DirProd_list_one:
shows "one (DirProd_list Gs) = foldr (λG tl. (one G) # tl) Gs []"
unfolding DirProd_list_def DirProd_def image_group_def by (induct Gs) (auto)

lemma DirProd_list_carrier_mem:
assumes "gs ∈ carrier (DirProd_list Gs)"
shows "length gs = length Gs" and "⋀i. i < length Gs ⟹ (gs ! i) ∈ carrier (Gs ! i)"
proof -
let ?same_length = "λxs ys. length xs = length ys"
let ?in_carrier = "λi gs Gs. (gs ! i) ∈ carrier (Gs ! i)"
from assms have "?same_length gs Gs ∧ (∀i < length Gs. ?in_carrier i gs Gs)"
proof (induct Gs arbitrary: gs, simp add: DirProd_list_def)
case (Cons G Gs)
then obtain g' gs'
where g': "g' ∈ carrier G" and gs': "gs' ∈ carrier (DirProd_list Gs)" and gs: "gs = g' # gs'"
unfolding DirProd_list_carrier by auto
hence "?same_length gs (G # Gs)" and "⋀i. i ∈ {(Suc 0)..< length (G # Gs)} ⟹ ?in_carrier i gs (G # Gs)"
using Cons(1) by auto
moreover have "?in_carrier 0 gs (G # Gs)"
unfolding gs using g' by simp
ultimately show ?case
by (metis atLeastLessThan_iff eq_imp_le less_Suc0 linorder_neqE_nat nat_less_le)
qed
thus "?same_length gs Gs" and "⋀i. i < length Gs ⟹ ?in_carrier i gs Gs"
by simp+
qed

lemma DirProd_list_carrier_memI:
assumes "length gs = length Gs" and "⋀i. i < length Gs ⟹ (gs ! i) ∈ carrier (Gs ! i)"
shows "gs ∈ carrier (DirProd_list Gs)"
using assms
proof (induct Gs arbitrary: gs, simp add: DirProd_list_def)
case (Cons G Gs)
then obtain g' gs' where gs: "gs = g' # gs'"
by (metis length_Suc_conv)
have "g' ∈ carrier G"
using Cons(3)[of 0] unfolding gs by auto
moreover have "gs' ∈ carrier (DirProd_list Gs)"
using Cons unfolding gs by force
ultimately show ?case
unfolding DirProd_list_carrier gs by blast
qed

lemma inj_on_DirProd_carrier:
shows "inj_on (λ(g, gs). g # gs) (carrier (G ×× (DirProd_list Gs)))"
unfolding DirProd_def inj_on_def by auto

lemma DirProd_list_is_group:
assumes "⋀i. i < length Gs ⟹ group (Gs ! i)" shows "group (DirProd_list Gs)"
using assms
proof (induct Gs)
case Nil thus ?case
unfolding DirProd_list_def by (unfold_locales, auto simp add: Units_def)
next
case (Cons G Gs)
hence is_group: "group (G ×× (DirProd_list Gs))"
using DirProd_group[of G "DirProd_list Gs"] by force
show ?case
using group.inj_imp_image_group_is_group[OF is_group inj_on_DirProd_carrier]
unfolding DirProd_list_def by auto
qed

lemma DirProd_list_iso:
"(λ(g, gs). g # gs) ∈ iso (G ×× (DirProd_list Gs)) (DirProd_list (G # Gs))"
using inj_imp_image_group_iso[OF inj_on_DirProd_carrier] unfolding DirProd_list_def by auto

end```