# Theory Isomorphisms

Up to index of Isabelle/HOL/Free-Groups

theory Isomorphisms
imports UnitGroup IntRing FreeGroups C2 Cardinal_Order_Relation
`header {* Isomorphisms of Free Groups *}theory "Isomorphisms"imports   "UnitGroup"   "~~/src/HOL/Algebra/IntRing"   "FreeGroups"   C2   "~~/src/HOL/Cardinals/Cardinal_Order_Relation"beginsubsection {* The Free Group over the empty set *}text {* The Free Group over an empty set of generators is isomorphic to the trivialgroup. *}lemma free_group_over_empty_set: "∃h. h ∈ \<F>⇘{}⇙ ≅ unit_group"proof(rule group.unit_group_unique)  show "group \<F>⇘{}⇙" by (rule free_group_is_group)next  have "carrier \<F>⇘{}::'a set⇙ = {[]}"    by (auto simp add:free_group_def)  thus "card (carrier \<F>⇘{}::'a set⇙) = 1"    by simpqedsubsection {* The Free Group over one generator *}text {* The Free Group over one generator is isomorphic to the free abelian groupover one element, also known as the integers. *}abbreviation "int_group"  where "int_group ≡ (| carrier = carrier \<Z>, mult = op +, one = 0::int |)),"lemma replicate_set_eq[simp]: "∀x ∈ set xs. x = y ==> xs = replicate (length xs) y"  by(induct xs)autolemma int_group_gen_by_one: "⟨{1}⟩⇘int_group⇙ = carrier int_group"proof  show "⟨{1}⟩⇘int_group⇙ ⊆ carrier int_group"    by auto  show "carrier int_group ⊆ ⟨{1}⟩⇘int_group⇙"  proof    interpret int: group int_group by (simp add: int.a_group)    fix x    have plus1: "1 ∈ ⟨{1}⟩⇘int_group⇙"      by (auto intro:gen_span.gen_gens)    hence "inv⇘int_group⇙ 1 ∈ ⟨{1}⟩⇘int_group⇙"      by (auto intro:gen_span.gen_inv)    moreover    have "-1 = inv⇘int_group⇙ 1"       using int.inv_equality by auto    ultimately    have minus1: "-1 ∈ ⟨{1}⟩⇘int_group⇙"      by (simp)    show "x ∈ ⟨{1::int}⟩⇘int_group⇙" (*    It does not work directly, unfortunately:    apply(induct x rule:int_induct[of _ "0::int"])    apply (auto simp add: int_arith_rules intro:gen_span.intros[of int_group])    *)    proof(induct x rule:int_induct[of _ "0::int"])    case base      have "\<one>⇘int_group⇙ ∈ ⟨{1::int}⟩⇘int_group⇙"        by (rule gen_span.gen_one)      thus"0 ∈ ⟨{1}⟩⇘int_group⇙"        by simp    next    case (step1 i)      from `i ∈ ⟨{1}⟩⇘int_group⇙` and plus1      have "i ⊗⇘int_group⇙ 1 ∈ ⟨{1}⟩⇘int_group⇙"         by (rule gen_span.gen_mult)      thus "i + 1 ∈ ⟨{1}⟩⇘int_group⇙" by simp    next    case (step2 i)      from `i ∈ ⟨{1}⟩⇘int_group⇙` and minus1      have "i ⊗⇘int_group⇙ -1 ∈ ⟨{1}⟩⇘int_group⇙"         by (rule gen_span.gen_mult)      thus "i - 1 ∈ ⟨{1}⟩⇘int_group⇙"         by (simp add: int_arith_rules)    qed  qedqedlemma free_group_over_one_gen: "∃h. h ∈ \<F>⇘{()}⇙ ≅ int_group"proof-  interpret int: group int_group by (simp add: int.a_group)  def f ≡ "λ(x::unit).(1::int)"  have "f ∈ {()} -> carrier int_group"    by auto  hence "int.lift f ∈ hom \<F>⇘{()}⇙ int_group"    by (rule int.lift_is_hom)  then  interpret hom: group_hom "\<F>⇘{()}⇙" int_group "int.lift f"    unfolding group_hom_def group_hom_axioms_def    by(auto intro: int.a_group free_group_is_group)      { (* This shows injectiveness of the given map *)    fix x    assume "x ∈ carrier \<F>⇘{()}⇙"    hence "canceled x" by (auto simp add:free_group_def)    assume "int.lift f x = (0::int)"    have "x = []"     proof(rule ccontr)      assume "x ≠ []"      then obtain a and xs where "x = a # xs" by (cases x, auto)      hence "length (takeWhile (λy. y = a) x) > 0" by auto      then obtain i where i: "length (takeWhile (λy. y = a) x) = Suc i"         by (cases "length (takeWhile (λy. y = a) x)", auto)      have "Suc i ≥ length x"      proof(rule ccontr)        assume "¬ length x ≤ Suc i"        hence "length (takeWhile (λy. y = a) x) < length x" using i by simp        hence "¬ (λy. y = a) (x ! length (takeWhile (λy. y = a) x))"          by (rule nth_length_takeWhile)        hence "¬ (λy. y = a) (x ! Suc i)" using i by simp        hence "fst (x ! Suc i) ≠ fst a" by (cases "x ! Suc i", cases "a", auto)        moreover        {          have "takeWhile (λy. y = a) x ! i = x ! i"            using i by (auto intro: takeWhile_nth)          moreover          have "(takeWhile (λy. y = a) x) ! i ∈ set (takeWhile (λy. y = a) x)"            using i by auto          ultimately          have "(λy. y = a) (x ! i)"            by (auto dest:set_takeWhileD)        }        hence "fst (x ! i) = fst a" by auto        moreover        have "snd (x ! i) = snd (x ! Suc i)" by simp        ultimately        have "canceling (x ! i) (x ! Suc i)" unfolding canceling_def by auto        hence "cancels_to_1_at i x (cancel_at i x)"          using `¬ length x ≤ Suc i` unfolding cancels_to_1_at_def           by (auto simp add:length_takeWhile_le)        hence "cancels_to_1 x (cancel_at i x)" unfolding cancels_to_1_def by auto        hence "¬ canceled x" unfolding canceled_def by auto        thus False using `canceled x` by contradiction      qed      hence "length (takeWhile (λy. y = a) x) = length x"        using i[THEN sym] by (auto dest:le_antisym simp add:length_takeWhile_le)      hence "takeWhile (λy. y = a) x = x"        by (subst takeWhile_eq_take, simp)      moreover      have "∀y ∈ set (takeWhile (λy. y = a) x). y = a"        by (auto dest: set_takeWhileD)      ultimately      have "∀y ∈ set x. y = a" by auto      hence "x = replicate (length x) a" by simp      hence "int.lift f x = int.lift f (replicate (length x) a)" by simp      also have "... = pow int_group (int.lift_gi f a) (length x)"        by (induct x,auto simp add:int.lift_def [simplified])      also have "... = (int.lift_gi f a) * int (length x)"        by (induct ("length x"), auto simp add:int_distrib)      finally have "… = 0" using `int.lift f x = 0` by simp      hence "nat (abs (group.lift_gi int_group f a * int (length x))) = 0" by simp      hence "nat (abs (group.lift_gi int_group f a)) * length x = 0" by simp      hence "nat (abs (group.lift_gi int_group f a)) = 0"        using `x ≠ []` by auto      moreover      have "inv⇘int_group⇙ 1 = -1"         using int.inv_equality by auto      hence "abs (group.lift_gi int_group f a) = 1"      using `group int_group`        by(auto simp add: group.lift_gi_def f_def)      ultimately      show False by simp    qed  }  hence "∀x∈carrier \<F>⇘{()}⇙. int.lift f x = \<one>⇘int_group⇙ --> x = \<one>⇘\<F>⇘{()}⇙⇙"    by (auto simp add:free_group_def)  moreover  {    have "carrier \<F>⇘{()}⇙ = ⟨insert`{()}⟩⇘\<F>⇘{()}⇙⇙"      by (rule gens_span_free_group[THEN sym])    moreover    have "carrier int_group = ⟨{1}⟩⇘int_group⇙"      by (rule int_group_gen_by_one[THEN sym])    moreover    have "int.lift f ` insert ` {()} = {1}"      by (auto simp add: int.lift_def [simplified] insert_def f_def int.lift_gi_def [simplified])    moreover    have  "int.lift f ` ⟨insert`{()}⟩⇘\<F>⇘{()}⇙⇙ = ⟨int.lift f ` (insert `{()})⟩⇘int_group⇙"      by (rule hom.hom_span, auto intro:insert_closed)    ultimately    have "int.lift f ` carrier \<F>⇘{()}⇙ = carrier int_group"      by simp  }  ultimately  have "int.lift f ∈ \<F>⇘{()}⇙ ≅ int_group"    using `int.lift f ∈ hom \<F>⇘{()}⇙ int_group`    using hom.hom_mult int.is_group    by (auto intro:group_isoI simp add: free_group_is_group)  thus ?thesis by autoqedsubsection {* Free Groups over isomorphic sets of generators *}text {* Free Groups are isomorphic if their set of generators are isomorphic. *}definition lift_generator_function :: "('a => 'b) => (bool × 'a) list => (bool × 'b) list"where "lift_generator_function f = map (map_pair id f)"theorem isomorphic_free_groups:  assumes "bij_betw f gens1 gens2"  shows "lift_generator_function f ∈ \<F>⇘gens1⇙ ≅ \<F>⇘gens2⇙"unfolding lift_generator_function_defproof(rule group_isoI)  show "∀x∈carrier \<F>⇘gens1⇙.       map (map_pair id f) x = \<one>⇘\<F>⇘gens2⇙⇙ --> x = \<one>⇘\<F>⇘gens1⇙⇙"    by(auto simp add:free_group_def)next  from `bij_betw f gens1 gens2` have "inj_on f gens1" by (auto simp:bij_betw_def)  show "map (map_pair id f) ` carrier \<F>⇘gens1⇙ = carrier \<F>⇘gens2⇙"  proof(rule Set.set_eqI,rule iffI)    from `bij_betw f gens1 gens2` have "f ` gens1 = gens2" by (auto simp:bij_betw_def)    fix x :: "(bool × 'b) list"    assume "x ∈ image (map (map_pair id f)) (carrier \<F>⇘gens1⇙)"    then obtain y :: "(bool × 'a) list" where "x = map (map_pair id f) y"                    and "y ∈ carrier \<F>⇘gens1⇙" by auto    from `y ∈ carrier \<F>⇘gens1⇙`    have "canceled y" and "y ∈ lists(UNIV×gens1)" by (auto simp add:free_group_def)    from `y ∈ lists (UNIV×gens1)`      and `x = map (map_pair id f) y`      and `image f gens1 = gens2`    have "x ∈ lists (UNIV×gens2)"      by (auto iff:lists_eq_set)    moreover    from `x = map (map_pair id f) y`     and `y ∈ lists (UNIV×gens1)`     and `canceled y`     and `inj_on f gens1`    have "canceled x"      by (auto intro!:rename_gens_canceled subset_inj_on[OF `inj_on f gens1`] iff:lists_eq_set)    ultimately    show "x ∈ carrier \<F>⇘gens2⇙" by (simp add:free_group_def)  next    fix x    assume "x ∈ carrier \<F>⇘gens2⇙"    hence "canceled x" and "x ∈ lists (UNIV×gens2)"      unfolding free_group_def by auto    def y ≡ "map (map_pair id (the_inv_into gens1 f)) x"    have "map (map_pair id f) y =          map (map_pair id f) (map (map_pair id (the_inv_into gens1 f)) x)"      by (simp add:y_def)    also have "… = map (map_pair id f o map_pair id (the_inv_into gens1 f)) x"      by simp    also have "… = map (map_pair id (f o the_inv_into gens1 f)) x"      by auto    also have "… = map id x"    proof(rule map_ext, rule impI)      fix xa :: "bool × 'b"      assume "xa ∈ set x"      from `x ∈ lists (UNIV×gens2)`      have "set (map snd x) ⊆ gens2"  by auto      hence "snd ` set x ⊆ gens2" by (simp add: set_map)      with `xa ∈ set x` have "snd xa ∈ gens2" by auto      with `bij_betw f gens1 gens2` have "snd xa ∈ f`gens1"        by (auto simp add: bij_betw_def)      have "map_pair id (f o the_inv_into gens1 f) xa            = map_pair id (f o the_inv_into gens1 f) (fst xa, snd xa)" by simp      also have "… = (fst xa, f (the_inv_into gens1 f (snd xa)))"        by (auto simp del:pair_collapse)      also with `snd xa ∈ image f gens1` and `inj_on f gens1`           have "… = (fst xa, snd xa)"           by (auto elim:f_the_inv_into_f simp del:pair_collapse)      also have "… = id xa" by simp      finally show "map_pair id (f o the_inv_into gens1 f) xa = id xa".    qed    also have "… = x" unfolding id_def by auto    finally have "map (map_pair id f) y = x".    moreover    {      from `bij_betw f gens1 gens2`      have "bij_betw (the_inv_into gens1 f) gens2 gens1" by (rule bij_betw_the_inv_into)      hence "inj_on (the_inv_into gens1 f) gens2" by (rule bij_betw_imp_inj_on)      with `canceled x`             and `x ∈ lists (UNIV×gens2)`      have "canceled y"        by (auto intro!:rename_gens_canceled[OF subset_inj_on] simp add:y_def)      moreover      {        from `bij_betw (the_inv_into gens1 f) gens2 gens1`         and `x∈lists(UNIV×gens2)`        have "y ∈ lists(UNIV×gens1)"          unfolding y_def and bij_betw_def          by (auto iff:lists_eq_set dest!:subsetD)      }      ultimately      have "y ∈ carrier \<F>⇘gens1⇙" by (simp add:free_group_def)    }    ultimately    show "x ∈ map (map_pair id f) ` carrier \<F>⇘gens1⇙" by auto  qednext  from `bij_betw f gens1 gens2` have "inj_on f gens1" by (auto simp:bij_betw_def)  {  fix x  assume "x ∈ carrier \<F>⇘gens1⇙"  fix y  assume "y ∈ carrier \<F>⇘gens1⇙"  from `x ∈ carrier \<F>⇘gens1⇙` and `y ∈ carrier \<F>⇘gens1⇙`  have "x ∈ lists(UNIV×gens1)" and "y ∈ lists(UNIV×gens1)"    by (auto simp add:occuring_gens_in_element)(*  hence "occuring_generators (x@y) ⊆ gens1"    by(auto simp add:occuring_generators_def)  with `inj_on f gens1` have "inj_on f (occuring_generators (x@y))"    by (rule subset_inj_on) *)  have "map (map_pair id f) (x ⊗⇘\<F>⇘gens1⇙⇙ y)       = map (map_pair id f) (normalize (x@y))" by (simp add:free_group_def)  also (* from `inj_on f (occuring_generators (x@y))` *)       from `x ∈ lists(UNIV×gens1)` and `y ∈ lists(UNIV×gens1)`        and `inj_on f gens1`       have "… = normalize (map (map_pair id f) (x@y))"         by -(rule rename_gens_normalize[THEN sym],              auto intro!: subset_inj_on[OF `inj_on f gens1`] iff:lists_eq_set)  also have "… = normalize (map (map_pair id f) x @ map (map_pair id f) y)"       by (auto)  also have "… = map (map_pair id f) x ⊗⇘\<F>⇘gens2⇙⇙ map (map_pair id f) y"       by (simp add:free_group_def)  finally have "map (map_pair id f) (x ⊗⇘\<F>⇘gens1⇙⇙ y) =                map (map_pair id f) x ⊗⇘\<F>⇘gens2⇙⇙ map (map_pair id f) y".  }  thus "∀x∈carrier \<F>⇘gens1⇙.       ∀y∈carrier \<F>⇘gens1⇙.          map (map_pair id f) (x ⊗⇘\<F>⇘gens1⇙⇙ y) =          map (map_pair id f) x ⊗⇘\<F>⇘gens2⇙⇙ map (map_pair id f) y"   by autoqed (auto intro: free_group_is_group)subsection {* Bases of isomorphic free groups *}text {* Isomorphic free groups have bases of same cardinality. The proof is very differentfor infinite bases and for finite bases.The proof for the finite case uses the set of of homomorphisms from the freegroup to the group with two elements, as suggested by Christian Sievers. Thedefinition of @{term hom} is not suitable for proofs about the cardinality of thatset, as its definition does not require extensionality. This is amended by thefollowing definition:*}definition homr  where "homr G H = {h. h ∈ hom G H ∧ h ∈ extensional (carrier G)}"lemma (in group_hom) restrict_hom[intro!]:  shows "restrict h (carrier G) ∈ homr G H"  unfolding homr_def and hom_def  by (auto)lemma hom_F_C2_Powerset:  "∃ f. bij_betw f (Pow X) (homr (\<F>⇘X⇙) C2)"proof  interpret F: group "\<F>⇘X⇙" by (rule free_group_is_group)  interpret C2: group C2 by (rule C2_is_group)  let ?f = "λS . restrict (C2.lift (λx. x ∈ S)) (carrier \<F>⇘X⇙)"  let ?f' = "λh . X ∩ Collect(h o insert)"  show "bij_betw ?f (Pow X) (homr (\<F>⇘X⇙) C2)"  proof(induct rule: bij_betwI[of ?f _ _ ?f'])  case 1 show ?case    proof      fix S assume "S ∈ Pow X"      interpret h: group_hom "\<F>⇘X⇙" C2 "C2.lift (λx. x ∈ S)"        by unfold_locales (auto intro: C2.lift_is_hom)      show "?f S ∈ homr \<F>⇘X⇙ C2"        by (rule h.restrict_hom)     qed  next  case 2 show ?case by auto next  case (3 S) show ?case    proof (induct rule: Set.set_eqI)      case (1 x) show ?case      proof(cases "x ∈ X")      case True thus ?thesis using insert_closed[of x X]         by (auto simp add:insert_def C2.lift_def C2.lift_gi_def)      next case False thus ?thesis using 3 by auto    qed  qed  next  case (4 h)    hence hom: "h ∈ hom \<F>⇘X⇙ C2"      and extn: "h ∈ extensional (carrier \<F>⇘X⇙)"      unfolding homr_def by auto    have "∀x ∈ carrier \<F>⇘X⇙ . h x = group.lift C2 (λz. z ∈ X & (h o FreeGroups.insert) z) x"     by (rule C2.lift_is_unique[OF C2_is_group _ hom, of "(λz. z ∈ X & (h o FreeGroups.insert) z)"],             auto)    thus ?case    by -(rule extensionalityI[OF restrict_extensional extn], auto)  qedqedlemma group_iso_betw_hom:  assumes "group G1" and "group G2"      and iso: "i ∈ G1 ≅ G2"  shows   "∃ f . bij_betw f (homr G2 H) (homr G1 H)"proof-  interpret G2: group G2 by (rule `group G2`)  let ?i' = "restrict (inv_into (carrier G1) i) (carrier G2)"  have "inv_into (carrier G1) i ∈ G2 ≅ G1" by (rule group.iso_sym[OF `group G1` iso])  hence iso': "?i' ∈ G2 ≅ G1"    by (auto simp add:Group.iso_def hom_def G2.m_closed)  show ?thesis  proof(rule, induct rule: bij_betwI[of "(λh. compose (carrier G1) h i)" _ _ "(λh. compose (carrier G2) h ?i')"])  case 1    show ?case    proof      fix h assume "h ∈ homr G2 H"      hence "compose (carrier G1) h i ∈ hom G1 H"        using iso        by (auto intro: group.hom_compose[OF `group G1`, of _ G2] simp add:Group.iso_def homr_def)      thus "compose (carrier G1) h i ∈ homr G1 H"        unfolding homr_def by simp     qed  next  case 2    show ?case    proof      fix h assume "h ∈ homr G1 H"      hence "compose (carrier G2) h ?i' ∈ hom G2 H"        using iso'        by (auto intro: group.hom_compose[OF `group G2`, of _ G1] simp add:Group.iso_def homr_def)      thus "compose (carrier G2) h ?i' ∈ homr G2 H"        unfolding homr_def by simp     qed  next  case (3 x)    hence "compose (carrier G2) (compose (carrier G1) x i) ?i'          = compose (carrier G2) x (compose (carrier G2) i ?i')"      using iso iso'      by (auto intro: compose_assoc[THEN sym]   simp add:Group.iso_def hom_def homr_def)    also have "… = compose (carrier G2) x (λy∈carrier G2. y)"      using iso      by (subst compose_id_inv_into, auto simp add:Group.iso_def hom_def bij_betw_def)    also have "… = x"      using 3      by (auto intro:compose_Id simp add:homr_def)    finally    show ?case .  next  case (4 y)    hence "compose (carrier G1) (compose (carrier G2) y ?i') i          = compose (carrier G1) y (compose (carrier G1) ?i' i)"      using iso iso'      by (auto intro: compose_assoc[THEN sym] simp add:Group.iso_def hom_def homr_def)    also have "… = compose (carrier G1) y (λx∈carrier G1. x)"      using iso      by (subst compose_inv_into_id, auto simp add:Group.iso_def hom_def bij_betw_def)    also have "… = y"      using 4      by (auto intro:compose_Id simp add:homr_def)    finally    show ?case .  qedqedlemma isomorphic_free_groups_bases_finite:  assumes iso: "i ∈ \<F>⇘X⇙ ≅ \<F>⇘Y⇙"      and finite: "finite X"  shows "∃f. bij_betw f X Y"proof-  obtain f    where "bij_betw f (homr \<F>⇘Y⇙ C2) (homr \<F>⇘X⇙ C2)"    using group_iso_betw_hom[OF free_group_is_group free_group_is_group iso]    by auto  moreover  obtain g'    where "bij_betw g' (Pow X) (homr (\<F>⇘X⇙) C2)"    using hom_F_C2_Powerset by auto  then obtain g    where "bij_betw g (homr (\<F>⇘X⇙) C2) (Pow X)"    by (auto intro: bij_betw_inv_into)  moreover  obtain h    where "bij_betw h (Pow Y) (homr (\<F>⇘Y⇙) C2)"    using hom_F_C2_Powerset by auto  ultimately  have "bij_betw (g o f o h) (Pow Y) (Pow X)"    by (auto intro: bij_betw_trans)  hence eq_card: "card (Pow Y) = card (Pow X)"    by (rule bij_betw_same_card)  with finite  have "finite (Pow Y)"   by -(rule card_ge_0_finite, auto simp add:card_Pow)  hence finite': "finite Y" by simp  with eq_card finite  have "card X = card Y"   by (auto simp add:card_Pow)  with finite finite'  show ?thesis   by (rule finite_same_card_bij)qedtext {*The proof for the infinite case is trivial once the fact that the free groupover an infinite set has the same cardinality is established.*}lemma free_group_card_infinite:  assumes "infinite X"  shows "|X| =o |carrier \<F>⇘X⇙|"proof-  have "inj_on insert X"   and "insert ` X ⊆ carrier \<F>⇘X⇙"    by (auto intro:insert_closed inj_onI simp add:insert_def)  hence "|X| ≤o |carrier \<F>⇘X⇙|"    by (subst card_of_ordLeq[THEN sym], auto)  moreover  have "|carrier \<F>⇘X⇙| ≤o |lists ((UNIV::bool set)×X)|"    by (auto intro!:card_of_mono1 simp add:free_group_def)  moreover  have "|lists ((UNIV::bool set)×X)| =o |(UNIV::bool set)×X|"    using `infinite X`    by (auto intro:card_of_lists_infinite dest!:finite_cartesian_productD2)  moreover  have  "|(UNIV::bool set)×X| =o |X|"    using `infinite X`    by (auto intro: card_of_Times_infinite[OF _ _ ordLess_imp_ordLeq[OF finite_ordLess_infinite2], THEN conjunct2])  ultimately  show "|X| =o |carrier \<F>⇘X⇙|"    by (subst ordIso_iff_ordLeq, auto intro: ord_trans)qedtheorem isomorphic_free_groups_bases:  assumes iso: "i ∈ \<F>⇘X⇙ ≅ \<F>⇘Y⇙"  shows "∃f. bij_betw f X Y"proof(cases "finite X")case True  thus ?thesis using iso by -(rule isomorphic_free_groups_bases_finite)nextcase False show ?thesis  proof(cases "finite Y")  case True  from iso obtain i' where "i' ∈ \<F>⇘Y⇙ ≅ \<F>⇘X⇙"       by (auto intro: group.iso_sym[OF free_group_is_group])  with `finite Y`  have "∃f. bij_betw f Y X" by -(rule isomorphic_free_groups_bases_finite)  thus "∃f. bij_betw f X Y" by (auto intro: bij_betw_the_inv_into) nextcase False  from `infinite X` have "|X| =o |carrier \<F>⇘X⇙|"     by (rule free_group_card_infinite)  moreover  from `infinite Y` have "|Y| =o |carrier \<F>⇘Y⇙|"     by (rule free_group_card_infinite)  moreover  from iso have "|carrier \<F>⇘X⇙| =o |carrier \<F>⇘Y⇙|"    by (auto simp add:Group.iso_def iff:card_of_ordIso[THEN sym])  ultimately  have "|X| =o |Y|" by (auto intro: ordIso_equivalence)  thus ?thesis by (subst card_of_ordIso)qedqedend`