Quelle Homology_Groups.thy Sprache: Isabelle

section\<open>Homology, II: Homology Groups\<close>

theory Homology_Groups
  imports Simplices "HOL-Algebra.Exact_Sequence"

begin
subsection\<open>Homology Groups\<close>

text\<open>Now actually connect to group theory and set up homology groups. Note that we define homomogy
groups for all \emph{integers} @{term p}, since this seems to avoid some special-case reasoning,
though they are trivial for @{term"p < 0"}.\<close>

definition chain_group :: "nat \ 'a topology \ 'a chain monoid"
  where "chain_group p X \ free_Abelian_group (singular_simplex_set p X)"

lemma carrier_chain_group [simp]: "carrier(chain_group p X) = singular_chain_set p X"
  by (auto simp: chain_group_def singular_chain_def free_Abelian_group_def)

lemma one_chain_group [simp]: "one(chain_group p X) = 0"
  by (auto simp: chain_group_def free_Abelian_group_def)

lemma mult_chain_group [simp]: "monoid.mult(chain_group p X) = (+)"
  by (auto simp: chain_group_def free_Abelian_group_def)

lemma m_inv_chain_group [simp]: "Poly_Mapping.keys a \ singular_simplex_set p X \ inv\<^bsub>chain_group p X\<^esub> a = -a"
  unfolding chain_group_def by simp

lemma group_chain_group [simp]: "Group.group (chain_group p X)"
  by (simp add: chain_group_def)

lemma abelian_chain_group: "comm_group(chain_group p X)"
  by (simp add: free_Abelian_group_def group.group_comm_groupI [OF group_chain_group])

lemma subgroup_singular_relcycle:
     "subgroup (singular_relcycle_set p X S) (chain_group p X)"
proof
  show "x \\<^bsub>chain_group p X\<^esub> y \ singular_relcycle_set p X S"
    if "x \ singular_relcycle_set p X S" and "y \ singular_relcycle_set p X S" for x y
    using that by (simp add: singular_relcycle_add)
next
  show "inv\<^bsub>chain_group p X\<^esub> x \ singular_relcycle_set p X S"
    if "x \ singular_relcycle_set p X S" for x
    using that
    by clarsimp (metis m_inv_chain_group singular_chain_def singular_relcycle singular_relcycle_minus)
qed (auto simp: singular_relcycle)

definition relcycle_group :: "nat \ 'a topology \ 'a set \ ('a chain) monoid"
  where "relcycle_group p X S \
        subgroup_generated (chain_group p X) (Collect(singular_relcycle p X S))"

lemma carrier_relcycle_group [simp]:
  "carrier (relcycle_group p X S) = singular_relcycle_set p X S"
proof -
  have "carrier (chain_group p X) \ singular_relcycle_set p X S = singular_relcycle_set p X S"
    using subgroup.subset subgroup_singular_relcycle by blast
  moreover have "generate (chain_group p X) (singular_relcycle_set p X S) \ singular_relcycle_set p X S"
    by (simp add: group.generate_subgroup_incl group_chain_group subgroup_singular_relcycle)
  ultimately show ?thesis
    by (auto simp: relcycle_group_def subgroup_generated_def generate.incl)
qed

lemma one_relcycle_group [simp]: "one(relcycle_group p X S) = 0"
  by (simp add: relcycle_group_def)

lemma mult_relcycle_group [simp]: "(\\<^bsub>relcycle_group p X S\<^esub>) = (+)"
  by (simp add: relcycle_group_def)

lemma abelian_relcycle_group [simp]:
   "comm_group(relcycle_group p X S)"
  unfolding relcycle_group_def
  by (intro group.abelian_subgroup_generated group_chain_group) (auto simp: abelian_chain_group singular_relcycle)

lemma group_relcycle_group [simp]: "group(relcycle_group p X S)"
  by (simp add: comm_group.axioms(2))

lemma relcycle_group_restrict [simp]:
   "relcycle_group p X (topspace X \ S) = relcycle_group p X S"
  by (metis relcycle_group_def singular_relcycle_restrict)

definition relative_homology_group :: "int \ 'a topology \ 'a set \ ('a chain) set monoid"
  where
    "relative_homology_group p X S \
        if p < 0 then singleton_group undefined else
        (relcycle_group (nat p) X S) Mod (singular_relboundary_set (nat p) X S)"

abbreviation homology_group
  where "homology_group p X \ relative_homology_group p X {}"

lemma relative_homology_group_restrict [simp]:
   "relative_homology_group p X (topspace X \ S) = relative_homology_group p X S"
  by (simp add: relative_homology_group_def)

lemma nontrivial_relative_homology_group:
  fixes p::nat
  shows "relative_homology_group p X S
       = relcycle_group p X S Mod singular_relboundary_set p X S"
  by (simp add: relative_homology_group_def)

lemma singular_relboundary_ss:
  "singular_relboundary p X S x \ Poly_Mapping.keys x \ singular_simplex_set p X"
    using singular_chain_def singular_relboundary_imp_chain by blast

lemma trivial_relative_homology_group [simp]:
  "p < 0 \ trivial_group(relative_homology_group p X S)"
  by (simp add: relative_homology_group_def)

lemma subgroup_singular_relboundary:
     "subgroup (singular_relboundary_set p X S) (chain_group p X)"
  unfolding chain_group_def
proof unfold_locales
  show "singular_relboundary_set p X S
        \<subseteq> carrier (free_Abelian_group (singular_simplex_set p X))"
    using singular_chain_def singular_relboundary_imp_chain by fastforce
next
  fix x
  assume "x \ singular_relboundary_set p X S"
  then show "inv\<^bsub>free_Abelian_group (singular_simplex_set p X)\<^esub> x
             \<in> singular_relboundary_set p X S"
    by (simp add: singular_relboundary_ss singular_relboundary_minus)
qed (auto simp: free_Abelian_group_def singular_relboundary_add)

lemma subgroup_singular_relboundary_relcycle:
  "subgroup (singular_relboundary_set p X S) (relcycle_group p X S)"
  unfolding relcycle_group_def
  by (simp add: Collect_mono group.subgroup_of_subgroup_generated singular_relboundary_imp_relcycle subgroup_singular_relboundary)

lemma normal_subgroup_singular_relboundary_relcycle:
   "(singular_relboundary_set p X S) \ (relcycle_group p X S)"
  by (simp add: comm_group.normal_iff_subgroup subgroup_singular_relboundary_relcycle)

lemma group_relative_homology_group [simp]:
  "group (relative_homology_group p X S)"
  by (simp add: relative_homology_group_def normal.factorgroup_is_group
                normal_subgroup_singular_relboundary_relcycle)

lemma right_coset_singular_relboundary:
  "r_coset (relcycle_group p X S) (singular_relboundary_set p X S)
  = (\<lambda>a. {b. homologous_rel p X S a b})"
  using singular_relboundary_minus
  by (force simp: r_coset_def homologous_rel_def relcycle_group_def subgroup_generated_def)

lemma carrier_relative_homology_group:
   "carrier(relative_homology_group (int p) X S)
= (homologous_rel_set p X S) ` singular_relcycle_set p X S"
  by (auto simp: set_eq_iff image_iff relative_homology_group_def FactGroup_def RCOSETS_def right_coset_singular_relboundary)

lemma carrier_relative_homology_group_0:
   "carrier(relative_homology_group 0 X S)
= (homologous_rel_set 0 X S) ` singular_relcycle_set 0 X S"
  using carrier_relative_homology_group [of 0 X S] by simp

lemma one_relative_homology_group [simp]:
  "one(relative_homology_group (int p) X S) = singular_relboundary_set p X S"
  by (simp add: relative_homology_group_def FactGroup_def)

lemma mult_relative_homology_group:
  "(\\<^bsub>relative_homology_group (int p) X S\<^esub>) = (\R S. (\r\R. \s\S. {r + s}))"
  unfolding relcycle_group_def subgroup_generated_def chain_group_def free_Abelian_group_def set_mult_def relative_homology_group_def FactGroup_def
  by force

lemma inv_relative_homology_group:
  assumes "R \ carrier (relative_homology_group (int p) X S)"
  shows "m_inv(relative_homology_group (int p) X S) R = uminus ` R"
proof (rule group.inv_equality [OF group_relative_homology_group _ assms])
  obtain c where c: "R = homologous_rel_set p X S c" "singular_relcycle p X S c"
    using assms by (auto simp: carrier_relative_homology_group)
  have "singular_relboundary p X S (b - a)"
    if "a \ R" and "b \ R" for a b
    using c that
    by clarify (metis homologous_rel_def homologous_rel_eq)
  moreover
  have "x \ (\x\R. \y\R. {y - x})"
    if "singular_relboundary p X S x" for x
    using c
    by simp (metis diff_eq_eq homologous_rel_def homologous_rel_refl homologous_rel_sym that)
  ultimately
  have "(\x\R. \xa\R. {xa - x}) = singular_relboundary_set p X S"
    by auto
  then show "uminus ` R \\<^bsub>relative_homology_group (int p) X S\<^esub> R =
        \<one>\<^bsub>relative_homology_group (int p) X S\<^esub>"
    by (auto simp: carrier_relative_homology_group mult_relative_homology_group)
  have "singular_relcycle p X S (-c)"
    using c by (simp add: singular_relcycle_minus)
  moreover have "homologous_rel p X S c x \ homologous_rel p X S (-c) (- x)" for x
    by (metis homologous_rel_def homologous_rel_sym minus_diff_eq minus_diff_minus)
  moreover have "homologous_rel p X S (-c) x \ x \ uminus ` homologous_rel_set p X S c" for x
    by (clarsimp simp: image_iff) (metis add.inverse_inverse diff_0 homologous_rel_diff homologous_rel_refl)
  ultimately show "uminus ` R \ carrier (relative_homology_group (int p) X S)"
    using c by (auto simp: carrier_relative_homology_group)
qed

lemma homologous_rel_eq_relboundary:
     "homologous_rel p X S c = singular_relboundary p X S
  \<longleftrightarrow> singular_relboundary p X S c" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    unfolding homologous_rel_def
    by (metis diff_zero singular_relboundary_0)
next
  assume R: ?rhs
  show ?lhs
    unfolding homologous_rel_def
    using singular_relboundary_diff R by fastforce
qed

lemma homologous_rel_set_eq_relboundary:
     "homologous_rel_set p X S c = singular_relboundary_set p X S \ singular_relboundary p X S c"
  by (auto simp flip: homologous_rel_eq_relboundary)

text\<open>Lift the boundary and induced maps to homology groups. We totalize both
quite aggressively to the appropriate group identity in all "undefined"
situations, which makes several of the properties cleaner and simpler.\<close>

lemma homomorphism_chain_boundary:
   "chain_boundary p \ hom (relcycle_group p X S) (relcycle_group(p - Suc 0) (subtopology X S) {})"
    (is "?h \ hom ?G ?H")
proof (rule homI)
  show "\x. x \ carrier ?G \ ?h x \ carrier ?H"
    by (auto simp: singular_relcycle_def mod_subset_def chain_boundary_boundary)
qed (simp add: relcycle_group_def subgroup_generated_def chain_boundary_add)

lemma hom_boundary1:
    "\d. \p X S.
          d p X S \<in> hom (relative_homology_group (int p) X S)
                        (homology_group (int (p - Suc 0)) (subtopology X S))
       \<and> (\<forall>c. singular_relcycle p X S c
              \<longrightarrow> d p X S (homologous_rel_set p X S c)
                = homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c))"
    (is "\d. \p X S. ?\ (d p X S) p X S")
proof ((subst choice_iff [symmetric])+, clarify)
  fix p X and S :: "'a set"
  define \<theta> where "\<theta> \<equiv> r_coset (relcycle_group(p - Suc 0) (subtopology X S) {})
                       (singular_relboundary_set (p - Suc 0) (subtopology X S) {}) \<circ> chain_boundary p"
  define H where "H \ relative_homology_group (int (p - Suc 0)) (subtopology X S) {}"
  define J where "J \ relcycle_group (p - Suc 0) (subtopology X S) {}"

  have \<theta>: "\<theta> \<in> hom (relcycle_group p X S) H"
    unfolding \<theta>_def
  proof (rule hom_compose)
    show "chain_boundary p \ hom (relcycle_group p X S) J"
      by (simp add: J_def homomorphism_chain_boundary)
    show "(#>\<^bsub>relcycle_group (p - Suc 0) (subtopology X S) {}\<^esub>)
         (singular_relboundary_set (p - Suc 0) (subtopology X S) {}) \<in> hom J H"
      by (simp add: H_def J_def nontrivial_relative_homology_group
           normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle)
  qed
  have *: "singular_relboundary (p - Suc 0) (subtopology X S) {} (chain_boundary p c)"
    if "singular_relboundary p X S c" for c
  proof (cases "p=0")
    case True
    then show ?thesis
      by (metis chain_boundary_def singular_relboundary_0)
  next
    case False
    with that have "\d. singular_chain p (subtopology X S) d \ chain_boundary p d = chain_boundary p c"
      by (metis add.left_neutral chain_boundary_add chain_boundary_boundary_alt singular_relboundary)
    with that False show ?thesis
      by (auto simp: singular_boundary)
  qed
  have \<theta>_eq: "\<theta> x = \<theta> y"
    if x: "x \ singular_relcycle_set p X S" and y: "y \ singular_relcycle_set p X S"
      and eq: "singular_relboundary_set p X S #>\<^bsub>relcycle_group p X S\<^esub> x
             = singular_relboundary_set p X S #>\<^bsub>relcycle_group p X S\<^esub> y" for x y
  proof -
    have "singular_relboundary p X S (x-y)"
      by (metis eq homologous_rel_def homologous_rel_eq mem_Collect_eq right_coset_singular_relboundary)
    with * have "(singular_relboundary (p - Suc 0) (subtopology X S) {}) (chain_boundary p (x-y))"
      by blast
  then show ?thesis
    unfolding \<theta>_def comp_def
    by (metis chain_boundary_diff homologous_rel_def homologous_rel_eq right_coset_singular_relboundary)
qed
  obtain d
    where "d \ hom ((relcycle_group p X S) Mod (singular_relboundary_set p X S)) H"
      and d: "\u. u \ singular_relcycle_set p X S \ d (homologous_rel_set p X S u) = \ u"
    by (metis FactGroup_universal [OF \<theta> normal_subgroup_singular_relboundary_relcycle \<theta>_eq] right_coset_singular_relboundary carrier_relcycle_group)
  then have "d \ hom (relative_homology_group p X S) H"
    by (simp add: nontrivial_relative_homology_group)
  then show  "\d. ?\ d p X S"
    by (force simp: H_def right_coset_singular_relboundary d \<theta>_def)
qed

lemma hom_boundary2:
  "\d. (\p X S.
           (d p X S) \<in> hom (relative_homology_group p X S)
                           (homology_group (p-1) (subtopology X S)))
     \<and> (\<forall>p X S c. singular_relcycle p X S c \<and> Suc 0 \<le> p
            \<longrightarrow> d p X S (homologous_rel_set p X S c)
              = homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c))"
  (is "\d. ?\ d")
proof -
  have *: "\f. \(\p. if p \ 0 then \q r t. undefined else f(nat p)) \ \f. \ f" for \
    by blast
  show ?thesis
    apply (rule * [OF ex_forward [OF hom_boundary1]])
    apply (simp add: not_le relative_homology_group_def nat_diff_distrib' int_eq_iff nat_diff_distrib flip: nat_1)
    by (simp add: hom_def singleton_group_def)
qed

lemma hom_boundary3:
  "\d. ((\p X S c. c \ carrier(relative_homology_group p X S)
              \<longrightarrow> d p X S c = one(homology_group (p-1) (subtopology X S))) \<and>
       (\<forall>p X S.
          d p X S \<in> hom (relative_homology_group p X S)
                        (homology_group (p-1) (subtopology X S))) \<and>
       (\<forall>p X S c.
            singular_relcycle p X S c \<and> 1 \<le> p
            \<longrightarrow> d p X S (homologous_rel_set p X S c)
              = homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)) \<and>
       (\<forall>p X S. d p X S = d p X (topspace X \<inter> S))) \<and>
       (\<forall>p X S c. d p X S c \<in> carrier(homology_group (p-1) (subtopology X S))) \<and>
       (\<forall>p. p \<le> 0 \<longrightarrow> d p = (\<lambda>q r t. undefined))"
  (is "\x. ?P x \ ?Q x \ ?R x")
proof -
  have "\x. ?Q x \ ?R x"
    by (erule all_forward) (force simp: relative_homology_group_def)
  moreover have "\x. ?P x \ ?Q x"
  proof -
    obtain d:: "[int, 'a topology, 'a set, ('a chain) set] \ ('a chain) set"
      where 1: "\p X S. d p X S \ hom (relative_homology_group p X S)
                                      (homology_group (p-1) (subtopology X S))"
        and 2: "\n X S c. singular_relcycle n X S c \ Suc 0 \ n
                  \<Longrightarrow> d n X S (homologous_rel_set n X S c)
                    = homologous_rel_set (n - Suc 0) (subtopology X S) {} (chain_boundary n c)"
      using hom_boundary2 by blast
    have 4: "c \ carrier (relative_homology_group p X S) \
        d p X (topspace X \<inter> S) c \<in> carrier (relative_homology_group (p-1) (subtopology X S) {})"
      for p X S c
      using hom_carrier [OF 1 [of p X "topspace X \ S"]]
      by (simp add: image_subset_iff subtopology_restrict)
    show ?thesis
      apply (rule_tac x="\p X S c.
               if c \<in> carrier(relative_homology_group p X S)
               then d p X (topspace X \<inter> S) c
               else one(homology_group (p-1) (subtopology X S))" in exI)
      apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
          group.is_monoid group.restrict_hom_iff 4 cong: if_cong)
      by (metis "1" "2" homologous_rel_restrict relative_homology_group_restrict singular_relcycle_def subtopology_restrict)
  qed
  ultimately show ?thesis
    by auto
qed

consts hom_boundary :: "[int,'a topology,'a set,'a chain set] \ 'a chain set"
specification (hom_boundary)
  hom_boundary:
      "((\p X S c. c \ carrier(relative_homology_group p X S)
              \<longrightarrow> hom_boundary p X S c = one(homology_group (p-1) (subtopology X (S::'a set)))) \<and>
       (\<forall>p X S.
          hom_boundary p X S \<in> hom (relative_homology_group p X S)
                        (homology_group (p-1) (subtopology X (S::'a set)))) \
       (\<forall>p X S c.
            singular_relcycle p X S c \<and> 1 \<le> p
            \<longrightarrow> hom_boundary p X S (homologous_rel_set p X S c)
              = homologous_rel_set (p - Suc 0) (subtopology X (S::'a set)) {} (chain_boundary p c)) \
       (\<forall>p X S. hom_boundary p X S = hom_boundary p X (topspace X \<inter> (S::'a set)))) \<and>
       (\<forall>p X S c. hom_boundary p X S c \<in> carrier(homology_group (p-1) (subtopology X (S::'a set)))) \<and>
       (\<forall>p. p \<le> 0 \<longrightarrow> hom_boundary p = (\<lambda>q r. \<lambda>t::'a chain set. undefined))"
  by (fact hom_boundary3)

lemma hom_boundary_default:
  "c \ carrier(relative_homology_group p X S)
      \<Longrightarrow> hom_boundary p X S c = one(homology_group (p-1) (subtopology X S))"
  and hom_boundary_hom: "hom_boundary p X S \ hom (relative_homology_group p X S) (homology_group (p-1) (subtopology X S))"
  and hom_boundary_restrict [simp]: "hom_boundary p X (topspace X \ S) = hom_boundary p X S"
  and hom_boundary_carrier: "hom_boundary p X S c \ carrier(homology_group (p-1) (subtopology X S))"
  and hom_boundary_trivial: "p \ 0 \ hom_boundary p = (\q r t. undefined)"
  by (metis hom_boundary)+

lemma hom_boundary_chain_boundary:
  "\singular_relcycle p X S c; 1 \ p\
    \<Longrightarrow> hom_boundary (int p) X S (homologous_rel_set p X S c) =
        homologous_rel_set (p - Suc 0) (subtopology X S) {} (chain_boundary p c)"
  by (metis hom_boundary)+

lemma hom_chain_map:
   "\continuous_map X Y f; f \ S \ T\
        \<Longrightarrow> (chain_map p f) \<in> hom (relcycle_group p X S) (relcycle_group p Y T)"
  by (simp add: chain_map_add hom_def singular_relcycle_chain_map)

lemma hom_induced1:
  "\hom_relmap.
    (\<forall>p X S Y T f.
        continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T
        \<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group (int p) X S)
                               (relative_homology_group (int p) Y T)) \<and>
    (\<forall>p X S Y T f c.
        continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
        singular_relcycle p X S c
        \<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
            homologous_rel_set p Y T (chain_map p f c))"
proof -
  have "\y. (y \ hom (relative_homology_group (int p) X S) (relative_homology_group (int p) Y T)) \
           (\<forall>c. singular_relcycle p X S c \<longrightarrow>
                y (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c))"
    if contf: "continuous_map X Y f" and fim: "f \ (topspace X \ S) \ T"
    for p X S Y T and f :: "'a \ 'b"
  proof -
    let ?f = "(#>\<^bsub>relcycle_group p Y T\<^esub>) (singular_relboundary_set p Y T) \ chain_map p f"
    let ?F = "\x. singular_relboundary_set p X S #>\<^bsub>relcycle_group p X S\<^esub> x"
    have "chain_map p f \ hom (relcycle_group p X S) (relcycle_group p Y T)"
      by (metis contf fim hom_chain_map relcycle_group_restrict)
    then have 1: "?f \ hom (relcycle_group p X S) (relative_homology_group (int p) Y T)"
      by (simp add: hom_compose normal.r_coset_hom_Mod normal_subgroup_singular_relboundary_relcycle relative_homology_group_def)
    have 2: "singular_relboundary_set p X S \ relcycle_group p X S"
      using normal_subgroup_singular_relboundary_relcycle by blast
    have 3: "?f x = ?f y"
      if "singular_relcycle p X S x" "singular_relcycle p X S y" "?F x = ?F y" for x y
    proof -
      have "homologous_rel p X S x y"
        by (metis (no_types) homologous_rel_set_eq right_coset_singular_relboundary that(3))
      then have "singular_relboundary p Y T (chain_map p f (x - y))"
        using  singular_relboundary_chain_map [OF _ contf fim] by (simp add: homologous_rel_def)
      then have "singular_relboundary p Y T (chain_map p f x - chain_map p f y)"
        by (simp add: chain_map_diff)
      with that
      show ?thesis
        by (metis comp_apply homologous_rel_def homologous_rel_set_eq right_coset_singular_relboundary)
    qed
    obtain g where "g \ hom (relcycle_group p X S Mod singular_relboundary_set p X S)
                            (relative_homology_group (int p) Y T)"
                   "\x. x \ singular_relcycle_set p X S \ g (?F x) = ?f x"
      using FactGroup_universal [OF 1 2 3, unfolded carrier_relcycle_group] by blast
    then show ?thesis
      by (force simp: right_coset_singular_relboundary nontrivial_relative_homology_group)
  qed
  then show ?thesis
    apply (simp flip: all_conj_distrib)
    apply ((subst choice_iff [symmetric])+)
    apply metis
    done
qed

lemma hom_induced2:
    "\hom_relmap.
      (\<forall>p X S Y T f.
          continuous_map X Y f \<and>
          f \<in> (topspace X \<inter> S) \<rightarrow> T
          \<longrightarrow> (hom_relmap p X S Y T f) \<in> hom (relative_homology_group p X S)
                                 (relative_homology_group p Y T)) \<and>
      (\<forall>p X S Y T f c.
          continuous_map X Y f \<and>
          f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
          singular_relcycle p X S c
          \<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
              homologous_rel_set p Y T (chain_map p f c)) \<and>
      (\<forall>p. p < 0 \<longrightarrow> hom_relmap p = (\<lambda>X S Y T f c. undefined))"
  (is "\d. ?\ d")
proof -
  have *: "\f. \(\p. if p < 0 then \X S Y T f c. undefined else f(nat p)) \ \f. \ f" for \
    by blast
  show ?thesis
    apply (rule * [OF ex_forward [OF hom_induced1]])
    apply (simp add: not_le relative_homology_group_def nat_diff_distrib' int_eq_iff nat_diff_distrib flip: nat_1)
    done
qed

lemma hom_induced3:
  "\hom_relmap.
    ((\<forall>p X S Y T f c.
        ~(continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
          c \<in> carrier(relative_homology_group p X S))
        \<longrightarrow> hom_relmap p X S Y T f c = one(relative_homology_group p Y T)) \<and>
    (\<forall>p X S Y T f.
        hom_relmap p X S Y T f \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)) \<and>
    (\<forall>p X S Y T f c.
        continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and> singular_relcycle p X S c
        \<longrightarrow> hom_relmap p X S Y T f (homologous_rel_set p X S c) =
            homologous_rel_set p Y T (chain_map p f c)) \<and>
    (\<forall>p X S Y T.
        hom_relmap p X S Y T =
        hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T))) \<and>
    (\<forall>p X S Y f T c.
        hom_relmap p X S Y T f c \<in> carrier(relative_homology_group p Y T)) \<and>
    (\<forall>p. p < 0 \<longrightarrow> hom_relmap p = (\<lambda>X S Y T f c. undefined))"
  (is "\x. ?P x \ ?Q x \ ?R x")
proof -
  have "\x. ?Q x \ ?R x"
    by (erule all_forward) (fastforce simp: relative_homology_group_def)
  moreover have "\x. ?P x \ ?Q x"
  proof -
    obtain hom_relmap:: "[int,'a topology,'a set,'b topology,'b set,'a \ 'b,('a chain) set] \ ('b chain) set"
      where 1: "\p X S Y T f. \continuous_map X Y f; f \ (topspace X \ S) \ T\ \
                   hom_relmap p X S Y T f
                   \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)"
        and 2: "\p X S Y T f c.
                   \<lbrakk>continuous_map X Y f; f \<in> (topspace X \<inter> S) \<rightarrow> T; singular_relcycle p X S c\<rbrakk>
                   \<Longrightarrow>
                   hom_relmap (int p) X S Y T f (homologous_rel_set p X S c) =
                   homologous_rel_set p Y T (chain_map p f c)"
        and 3: "(\p. p < 0 \ hom_relmap p = (\X S Y T f c. undefined))"
      using hom_induced2 [where ?'a='a and ?'b='b]
      by (fastforce simp: Pi_iff)
    have 4: "\continuous_map X Y f; f \ (topspace X \ S) \ T; c \ carrier (relative_homology_group p X S)\ \
        hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
           \<in> carrier (relative_homology_group p Y T)"
      for p X S Y f T c
      using hom_carrier [OF 1 [of X Y f "topspace X \ S" "topspace Y \ T" p]]
            continuous_map_image_subset_topspace by fastforce
    have inhom: "(\c. if continuous_map X Y f \ f \ (topspace X \ S) \ T \
                      c \<in> carrier (relative_homology_group p X S)
            then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
            else \<one>\<^bsub>relative_homology_group p Y T\<^esub>)
       \<in> hom (relative_homology_group p X S) (relative_homology_group p Y T)" (is "?h \<in> hom ?GX ?GY")
      for p X S Y T f
    proof (rule homI)
      show "\x. x \ carrier ?GX \ ?h x \ carrier ?GY"
        by (auto simp: 4 group.is_monoid)
      show "?h (x \\<^bsub>?GX\<^esub> y) = ?h x \\<^bsub>?GY\<^esub>?h y" if "x \ carrier ?GX" "y \ carrier ?GX" for x y
      proof (cases "p < 0")
        case True
        with that show ?thesis
          by (simp add: relative_homology_group_def singleton_group_def 3)
      next
        case False
        show ?thesis
        proof (cases "continuous_map X Y f")
          case True
          then have "f \ (topspace X \ S) \ topspace Y"
            using continuous_map_image_subset_topspace by blast
          then show ?thesis
            using True False that
            using 1 [of X Y f "topspace X \ S" "topspace Y \ T" p]
            by (simp add: 4 Pi_iff continuous_map_funspace hom_mult not_less group.is_monoid monoid.m_closed Int_left_absorb)
        qed (simp add: group.is_monoid)
      qed
    qed
    have hrel: "\continuous_map X Y f; f \ (topspace X \ S) \ T; singular_relcycle p X S c\
            \<Longrightarrow> hom_relmap (int p) X (topspace X \<inter> S) Y (topspace Y \<inter> T)
              f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
        for p X S Y T f c
      using 2 [of X Y f "topspace X \ S" "topspace Y \ T" p c]
            continuous_map_image_subset_topspace by fastforce
    show ?thesis
      apply (rule_tac x="\p X S Y T f c.
               if continuous_map X Y f \<and> f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
                  c \<in> carrier(relative_homology_group p X S)
               then hom_relmap p X (topspace X \<inter> S) Y (topspace Y \<inter> T) f c
               else one(relative_homology_group p Y T)" in exI)
      apply (simp add: Int_left_absorb subtopology_restrict carrier_relative_homology_group
          group.is_monoid group.restrict_hom_iff 4 inhom hrel split: if_splits)
      apply (intro ext strip)
      apply (auto simp: continuous_map_def)
      done
  qed
  ultimately show ?thesis
    by auto
qed

consts hom_induced:: "[int,'a topology,'a set,'b topology,'b set,'a \ 'b,('a chain) set] \ ('b chain) set"
specification (hom_induced)
  hom_induced:
    "((\p X S Y T f c.
        ~(continuous_map X Y f \<and>
          f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
          c \<in> carrier(relative_homology_group p X S))
        \<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f c =
            one(relative_homology_group p Y T)) \<and>
    (\<forall>p X S Y T f.
        (hom_induced p X (S::'a set) Y (T::'b set) f) \<in> hom (relative_homology_group p X S)
                           (relative_homology_group p Y T)) \<and>
    (\<forall>p X S Y T f c.
        continuous_map X Y f \<and>
        f \<in> (topspace X \<inter> S) \<rightarrow> T \<and>
        singular_relcycle p X S c
        \<longrightarrow> hom_induced p X (S::'a set) Y (T::'b set) f (homologous_rel_set p X S c) =
            homologous_rel_set p Y T (chain_map p f c)) \<and>
    (\<forall>p X S Y T.
        hom_induced p X (S::'a set) Y (T::'b set) =
        hom_induced p X (topspace X \<inter> S) Y (topspace Y \<inter> T))) \<and>
    (\<forall>p X S Y f T c.
        hom_induced p X (S::'a set) Y (T::'b set) f c \<in>
        carrier(relative_homology_group p Y T)) \<and>
    (\<forall>p. p < 0 \<longrightarrow> hom_induced p = (\<lambda>X S Y T. \<lambda>f::'a\<Rightarrow>'b. \<lambda>c. undefined))"
  by (fact hom_induced3)

lemma hom_induced_default:
    "~(continuous_map X Y f \ f \ (topspace X \ S) \ T \ c \ carrier(relative_homology_group p X S))
          \<Longrightarrow> hom_induced p X S Y T f c = one(relative_homology_group p Y T)"
  and hom_induced_hom:
    "hom_induced p X S Y T f \ hom (relative_homology_group p X S) (relative_homology_group p Y T)"
  and hom_induced_restrict [simp]:
    "hom_induced p X (topspace X \ S) Y (topspace Y \ T) = hom_induced p X S Y T"
  and hom_induced_carrier:
    "hom_induced p X S Y T f c \ carrier(relative_homology_group p Y T)"
  and hom_induced_trivial: "p < 0 \ hom_induced p = (\X S Y T f c. undefined)"
  by (metis hom_induced)+

lemma hom_induced_chain_map_gen:
  "\continuous_map X Y f; f \ (topspace X \ S) \ T; singular_relcycle p X S c\
  \<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c) = homologous_rel_set p Y T (chain_map p f c)"
  by (metis hom_induced)

lemma hom_induced_chain_map:
   "\continuous_map X Y f; f \ S \ T; singular_relcycle p X S c\
    \<Longrightarrow> hom_induced p X S Y T f (homologous_rel_set p X S c)
      = homologous_rel_set p Y T (chain_map p f c)"
  by (simp add: Pi_iff hom_induced_chain_map_gen)

lemma hom_induced_eq:
  assumes "\x. x \ topspace X \ f x = g x"
  shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof -
  consider "p < 0" | n where "p = int n"
    by (metis int_nat_eq not_less)
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      by (simp add: hom_induced_trivial)
  next
    case 2
    have "hom_induced n X S Y T f C = hom_induced n X S Y T g C" for C
    proof -
      have "continuous_map X Y f \ f \ (topspace X \ S) \ T \ C \ carrier (relative_homology_group n X S)
        \<longleftrightarrow> continuous_map X Y g \<and> g \<in> (topspace X \<inter> S) \<rightarrow> T \<and> C \<in> carrier (relative_homology_group n X S)"
        (is "?P = ?Q")
        using assms Pi_iff continuous_map_eq [of X Y]
        by (smt (verit, ccfv_SIG) Int_iff)
      then consider "\ ?P \ \ ?Q" | "?P \ ?Q"
        by blast
      then show ?thesis
      proof cases
        case 1
        then show ?thesis
          by (simp add: hom_induced_default)
      next
        case 2
        have "homologous_rel_set n Y T (chain_map n f c) = homologous_rel_set n Y T (chain_map n g c)"
          if "continuous_map X Y f" "f \ (topspace X \ S) \ T"
             "continuous_map X Y g" "g \ (topspace X \ S) \ T"
             "C = homologous_rel_set n X S c" "singular_relcycle n X S c"
          for c
        proof -
          have "chain_map n f c = chain_map n g c"
            using assms chain_map_eq singular_relcycle that by metis
          then show ?thesis
            by simp
        qed
        with 2 show ?thesis
          by (force simp: relative_homology_group_def carrier_FactGroup
              right_coset_singular_relboundary hom_induced_chain_map_gen)
      qed
    qed
    with 2 show ?thesis
      by auto
  qed
qed

subsection\<open>Towards the Eilenberg-Steenrod axioms\<close>

text\<open>First prove we get functors into abelian groups with the boundary map
being a natural transformation between them, and prove Eilenberg-Steenrod
axioms (we also prove additivity a bit later on if one counts that). \<close>
(*1. Exact sequence from the inclusions and boundary map
    H_{p+1} X --(j')\<longlongrightarrow> H_{p+1}X (A) --(d')\<longlongrightarrow> H_p A --(i')\<longlongrightarrow> H_p X
2. Dimension axiom: H_p X is trivial for one-point X and p =/= 0
3. Homotopy invariance of the induced map
4. Excision: inclusion (X - U,A - U) --(i')\<longlongrightarrow> X (A) induces an isomorphism
when cl U \<subseteq> int A*)

lemma abelian_relative_homology_group [simp]:
   "comm_group(relative_homology_group p X S)"
  by (simp add: comm_group.abelian_FactGroup relative_homology_group_def subgroup_singular_relboundary_relcycle)

lemma abelian_homology_group: "comm_group(homology_group p X)"
  by simp

lemma hom_induced_id_gen:
  assumes contf: "continuous_map X X f" and feq: "\x. x \ topspace X \ f x = x"
    and c: "c \ carrier (relative_homology_group p X S)"
  shows "hom_induced p X S X S f c = c"
proof -
  consider "p < 0" | n where "p = int n"
    by (metis int_nat_eq not_less)
  then show ?thesis
  proof cases
    case 1
    with c show ?thesis
      by (simp add: hom_induced_trivial relative_homology_group_def)
  next
    case 2
    have cm: "chain_map n f d = d" if "singular_relcycle n X S d" for d
      using that assms by (auto simp: chain_map_id_gen singular_relcycle)
    have "f ` (topspace X \ S) \ S"
      using feq by auto
    with 2 c show ?thesis
      by (auto simp: nontrivial_relative_homology_group carrier_FactGroup
          cm right_coset_singular_relboundary hom_induced_chain_map_gen assms)
  qed
qed

lemma hom_induced_id:
   "c \ carrier (relative_homology_group p X S) \ hom_induced p X S X S id c = c"
  by (rule hom_induced_id_gen) auto

lemma hom_induced_compose:
  assumes "continuous_map X Y f" "f \ S \ T" "continuous_map Y Z g" "g \ T \ U"
  shows "hom_induced p X S Z U (g \ f) = hom_induced p Y T Z U g \ hom_induced p X S Y T f"
proof -
  consider (neg) "p < 0" | (int) n where "p = int n"
    by (metis int_nat_eq not_less)
  then show ?thesis
  proof cases
    case int
    have gf: "continuous_map X Z (g \ f)"
      using assms continuous_map_compose by fastforce
    have gfim: "(g \ f) \ S \ U"
      unfolding o_def using assms by blast
    have sr: "\a. singular_relcycle n X S a \ singular_relcycle n Y T (chain_map n f a)"
      by (simp add: assms singular_relcycle_chain_map)
    show ?thesis
    proof
      fix c
      show "hom_induced p X S Z U (g \ f) c = (hom_induced p Y T Z U g \ hom_induced p X S Y T f) c"
      proof (cases "c \ carrier(relative_homology_group p X S)")
        case True
        with gfim show ?thesis
          unfolding int
          by (auto simp: carrier_relative_homology_group gf gfim assms
              sr chain_map_compose hom_induced_chain_map)
      next
        case False
        then show ?thesis
          by (simp add: hom_induced_default hom_one [OF hom_induced_hom])
      qed
    qed
  qed (force simp: hom_induced_trivial)
qed

lemma hom_induced_compose':
  assumes "continuous_map X Y f" "f \ S \ T" "continuous_map Y Z g" "g \ T \ U"
  shows "hom_induced p Y T Z U g (hom_induced p X S Y T f x) = hom_induced p X S Z U (g \ f) x"
  using hom_induced_compose [OF assms] by simp

lemma naturality_hom_induced:
  assumes "continuous_map X Y f" "f \ S \ T"
  shows "hom_boundary q Y T \ hom_induced q X S Y T f
       = hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f \<circ> hom_boundary q X S"
proof (cases "q \ 0")
  case False
  then obtain p where p1: "p \ Suc 0" and q: "q = int p"
    using zero_le_imp_eq_int by force
  show ?thesis
  proof
    fix c
    show "(hom_boundary q Y T \ hom_induced q X S Y T f) c =
          (hom_induced (q - 1) (subtopology X S) {} (subtopology Y T) {} f \<circ> hom_boundary q X S) c"
    proof (cases "c \ carrier(relative_homology_group p X S)")
      case True
      then obtain a where ceq: "c = homologous_rel_set p X S a" and a: "singular_relcycle p X S a"
        by (force simp: carrier_relative_homology_group)
      then have sr: "singular_relcycle p Y T (chain_map p f a)"
        using assms singular_relcycle_chain_map by fastforce
      then have sb: "singular_relcycle (p - Suc 0) (subtopology X S) {} (chain_boundary p a)"
        by (metis One_nat_def a chain_boundary_boundary singular_chain_0 singular_relcycle)
      have p1_eq: "int p - 1 = int (p - Suc 0)"
        using p1 by auto
      have cbm: "(chain_boundary p (chain_map p f a))
               = (chain_map (p - Suc 0) f (chain_boundary p a))"
        using a chain_boundary_chain_map singular_relcycle by metis
      have contf: "continuous_map (subtopology X S) (subtopology Y T) f"
        using assms
        by (auto simp: continuous_map_in_subtopology continuous_map_from_subtopology)
      show ?thesis
        unfolding q using assms p1 a
        by (simp add: cbm ceq contf hom_boundary_chain_boundary hom_induced_chain_map p1_eq sb sr
                 del: of_nat_diff)
    next
      case False
      with assms show ?thesis
        unfolding q o_def using assms
        apply (simp add: hom_induced_default hom_boundary_default)
        by (metis group_relative_homology_group hom_boundary hom_induced hom_one one_relative_homology_group)
    qed
  qed
qed (force simp: hom_induced_trivial hom_boundary_trivial)

lemma homology_exactness_axiom_1:
   "exact_seq ([homology_group (p-1) (subtopology X S), relative_homology_group p X S, homology_group p X],
              [hom_boundary p X S,hom_induced p X {} X S id])"
proof -
  consider (neg) "p < 0" | (int) n where "p = int n"
    by (metis int_nat_eq not_less)
  then have "(hom_induced p X {} X S id) ` carrier (homology_group p X)
           = kernel (relative_homology_group p X S) (homology_group (p-1) (subtopology X S))
                    (hom_boundary p X S)"
  proof cases
    case neg
    then show ?thesis
      unfolding kernel_def singleton_group_def relative_homology_group_def
      by (auto simp: hom_induced_trivial hom_boundary_trivial)
  next
    case int
    have "hom_induced (int m) X {} X S id ` carrier (relative_homology_group (int m) X {})
        = carrier (relative_homology_group (int m) X S) \<inter>
          {c. hom_boundary (int m) X S c = \<one>\<^bsub>relative_homology_group (int m - 1) (subtopology X S) {}\<^esub>}" for m
    proof (cases m)
      case 0
      have "hom_induced 0 X {} X S id ` carrier (relative_homology_group 0 X {})
          = carrier (relative_homology_group 0 X S)" (is "?lhs = ?rhs")
      proof
        show "?lhs \ ?rhs"
          using hom_induced_hom [of 0 X "{}" X S id]
          by (simp add: hom_induced_hom hom_carrier)
        show "?rhs \ ?lhs"
          apply (clarsimp simp add: image_iff carrier_relative_homology_group [of 0, simplified] singular_relcycle)
          apply (force simp: chain_map_id_gen chain_boundary_def singular_relcycle
              hom_induced_chain_map [of concl: 0, simplified])
          done
      qed
      with 0 show ?thesis
        by (simp add: hom_boundary_trivial relative_homology_group_def [of "-1"] singleton_group_def)
    next
      case (Suc n)
      have "(hom_induced (int (Suc n)) X {} X S id \
            homologous_rel_set (Suc n) X {}) ` singular_relcycle_set (Suc n) X {}
          = homologous_rel_set (Suc n) X S `
            (singular_relcycle_set (Suc n) X S \<inter>
             {c. hom_boundary (int (Suc n)) X S (homologous_rel_set (Suc n) X S c)
               = singular_relboundary_set n (subtopology X S) {}})"
        (is "?lhs = ?rhs")
      proof -
        have 1: "(\x. x \ A \ x \ B \ x \ C) \ f ` (A \ B) = f ` (A \ C)" for f A B C
          by blast
        have 2: "\\x. x \ A \ \y. y \ B \ f x = f y; \x. x \ B \ \y. y \ A \ f x = f y\
    \<Longrightarrow> f ` A = f ` B" for f A B
          by blast
        have "?lhs = homologous_rel_set (Suc n) X S ` singular_relcycle_set (Suc n) X {}"
          using hom_induced_chain_map chain_map_ident [of _ X] singular_relcycle
          by (smt (verit, best) comp_apply continuous_map_id empty_iff funcsetI
              image_cong mem_Collect_eq)
        also have "\ = homologous_rel_set (Suc n) X S `
                         (singular_relcycle_set (Suc n) X S \<inter>
                          {c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)})"
        proof (rule 2)
          fix c
          assume "c \ singular_relcycle_set (Suc n) X {}"
          then show "\y. y \ singular_relcycle_set (Suc n) X S \
                         {c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)} \<and>
                    homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
            using singular_cycle singular_relcycle
            by (metis Int_Collect mem_Collect_eq singular_chain_0
                singular_relboundary_0)
        next
          fix c
          assume c: "c \ singular_relcycle_set (Suc n) X S \
                      {c. singular_relboundary n (subtopology X S) {} (chain_boundary (Suc n) c)}"
          then obtain d where d: "singular_chain (Suc n) (subtopology X S) d"
            "chain_boundary (Suc n) d = chain_boundary (Suc n) c"
            by (auto simp: singular_boundary)
          with c have "c - d \ singular_relcycle_set (Suc n) X {}"
            by (auto simp: singular_cycle chain_boundary_diff singular_chain_subtopology singular_relcycle singular_chain_diff)
          moreover have "homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S (c - d)"
          proof (simp add: homologous_rel_set_eq)
            show "homologous_rel (Suc n) X S c (c - d)"
              using d by (simp add: homologous_rel_def singular_chain_imp_relboundary)
          qed
          ultimately show "\y. y \ singular_relcycle_set (Suc n) X {} \
                    homologous_rel_set (Suc n) X S c = homologous_rel_set (Suc n) X S y"
            by blast
        qed
        also have "\ = ?rhs"
          by (rule 1) (simp add: hom_boundary_chain_boundary homologous_rel_set_eq_relboundary del: of_nat_Suc)
        finally show "?lhs = ?rhs" .
      qed
      with Suc show ?thesis
        unfolding carrier_relative_homology_group image_comp id_def by auto
    qed
    then show ?thesis
      by (auto simp: kernel_def int)
  qed
  then show ?thesis
    using hom_boundary_hom hom_induced_hom
    by (force simp: group_hom_def group_hom_axioms_def)
qed

lemma homology_exactness_axiom_2:
   "exact_seq ([homology_group (p-1) X, homology_group (p-1) (subtopology X S), relative_homology_group p X S],
              [hom_induced (p-1) (subtopology X S) {} X {} id, hom_boundary p X S])"
proof -
  consider (neg) "p \ 0" | (int) n where "p = int (Suc n)"
    by (metis linear not0_implies_Suc of_nat_0 zero_le_imp_eq_int)
  then have "kernel (relative_homology_group (p-1) (subtopology X S) {})
                     (relative_homology_group (p-1) X {})
                     (hom_induced (p-1) (subtopology X S) {} X {} id)
            = hom_boundary p X S ` carrier (relative_homology_group p X S)"
  proof cases
    case neg
    obtain x where "x \ carrier (relative_homology_group p X S)"
      using group_relative_homology_group group.is_monoid by blast
    with neg show ?thesis
      unfolding kernel_def singleton_group_def relative_homology_group_def
      by (force simp: hom_induced_trivial hom_boundary_trivial)
  next
    case int
    have "hom_boundary (int (Suc n)) X S ` carrier (relative_homology_group (int (Suc n)) X S)
        = carrier (relative_homology_group n (subtopology X S) {}) \<inter>
          {c. hom_induced n (subtopology X S) {} X {} id c =
           \<one>\<^bsub>relative_homology_group n X {}\<^esub>}"
        (is "?lhs = ?rhs")
    proof -
      have 1: "(\x. x \ A \ x \ B \ x \ C) \ f ` (A \ B) = f ` (A \ C)" for f A B C
        by blast
      have 2: "(\x. x \ A \ x \ B \ x \ f -` C) \ f ` (A \ B) = f ` A \ C" for f A B C
        by blast
      have "?lhs = homologous_rel_set n (subtopology X S) {}
                   ` (chain_boundary (Suc n) ` singular_relcycle_set (Suc n) X S)"
        unfolding carrier_relative_homology_group image_comp
        by (rule image_cong [OF refl]) (simp add: o_def hom_boundary_chain_boundary del: of_nat_Suc)
      also have "\ = homologous_rel_set n (subtopology X S) {} `
                       (singular_relcycle_set n (subtopology X S) {} \<inter> singular_relboundary_set n X {})"
        by (force simp: singular_relcycle singular_boundary chain_boundary_boundary_alt)
      also have "\ = ?rhs"
        unfolding carrier_relative_homology_group vimage_def
        by (intro 2) (auto simp: hom_induced_chain_map chain_map_ident homologous_rel_set_eq_relboundary singular_relcycle)
      finally show ?thesis .
    qed
    then show ?thesis
      by (auto simp: kernel_def int)
  qed
  then show ?thesis
    using hom_boundary_hom hom_induced_hom
    by (force simp: group_hom_def group_hom_axioms_def)
qed

lemma homology_exactness_axiom_3:
   "exact_seq ([relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)],
              [hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])"
proof (cases "p < 0")
  case True
  then show ?thesis
    unfolding relative_homology_group_def
    by (simp add: group_hom.kernel_to_trivial_group group_hom_axioms_def group_hom_def hom_induced_trivial)
next
  case False
  then obtain n where peq: "p = int n"
    by (metis int_ops(1) linorder_neqE_linordered_idom pos_int_cases)
  have "hom_induced n (subtopology X S) {} X {} id `
        (homologous_rel_set n (subtopology X S) {} `
        singular_relcycle_set n (subtopology X S) {})
      = {c \<in> homologous_rel_set n X {} ` singular_relcycle_set n X {}.
         hom_induced n X {} X S id c = singular_relboundary_set n X S}"
        (is "?lhs = ?rhs")
  proof -
    have 2: "\\x. x \ A \ \y. y \ B \ f x = f y; \x. x \ B \ \y. y \ A \ f x = f y\
    \<Longrightarrow> f ` A = f ` B" for f A B
      by blast
    have "\f. singular_chain n (subtopology X S) f \
         singular_chain (n - Suc 0) trivial_topology (chain_boundary n f) \<Longrightarrow>
         hom_induced (int n) (subtopology X S) {} X {} id (homologous_rel_set n (subtopology X S) {} f) =
         homologous_rel_set n X {} f"
      by (auto simp: chain_map_ident hom_induced_chain_map singular_relcycle)
    then have "?lhs = homologous_rel_set n X {} ` (singular_relcycle_set n (subtopology X S) {})"
      by (simp add: singular_relcycle image_comp)
    also have "\ = homologous_rel_set n X {} ` (singular_relcycle_set n X {} \ singular_relboundary_set n X S)"
    proof (rule 2)
      fix c
      assume "c \ singular_relcycle_set n (subtopology X S) {}"
      then show "\y. y \ singular_relcycle_set n X {} \ singular_relboundary_set n X S \
            homologous_rel_set n X {} c = homologous_rel_set n X {} y"
        using singular_chain_imp_relboundary singular_relboundary_imp_chain
        by (fastforce simp: singular_cycle)
    next
      fix c
      assume "c \ singular_relcycle_set n X {} \ singular_relboundary_set n X S"
      then obtain d e where c: "singular_relcycle n X {} c" "singular_relboundary n X S c"
        and d:  "singular_chain n (subtopology X S) d"
        and e: "singular_chain (Suc n) X e" "chain_boundary (Suc n) e = c + d"
        using singular_relboundary_alt by blast
      then have "chain_boundary n (c + d) = 0"
        using chain_boundary_boundary_alt by fastforce
      then have "chain_boundary n c + chain_boundary n d = 0"
        by (metis chain_boundary_add)
      with c have "singular_relcycle n (subtopology X S) {} (- d)"
        by (metis (no_types) d eq_add_iff singular_cycle singular_relcycle_minus)
      moreover have "homologous_rel n X {} c (- d)"
        using c
        by (metis diff_minus_eq_add e homologous_rel_def singular_boundary)
      ultimately
      show "\y. y \ singular_relcycle_set n (subtopology X S) {} \
            homologous_rel_set n X {} c = homologous_rel_set n X {} y"
        by (force simp: homologous_rel_set_eq)
    qed
    also have "\ = homologous_rel_set n X {} `
                  (singular_relcycle_set n X {} \<inter> homologous_rel_set n X {} -` {x. hom_induced n X {} X S id x = singular_relboundary_set n X S})"
      by (rule 2) (auto simp: hom_induced_chain_map homologous_rel_set_eq_relboundary chain_map_ident [of _ X] singular_cycle cong: conj_cong)
    also have "\ = ?rhs"
      by blast
    finally show ?thesis .
  qed
  then have "kernel (relative_homology_group p X {}) (relative_homology_group p X S) (hom_induced p X {} X S id)
      = hom_induced p (subtopology X S) {} X {} id ` carrier (relative_homology_group p (subtopology X S) {})"
    by (simp add: kernel_def carrier_relative_homology_group peq)
  then show ?thesis
    by (simp add: not_less group_hom_def group_hom_axioms_def hom_induced_hom)
qed

lemma homology_dimension_axiom:
  assumes X: "topspace X = {a}" and "p \ 0"
  shows "trivial_group(homology_group p X)"
proof (cases "p < 0")
  case True
  then show ?thesis
    by simp
next
  case False
  then obtain n where peq: "p = int n" "n > 0"
    by (metis assms(2) neq0_conv nonneg_int_cases not_less of_nat_0)
  have "homologous_rel_set n X {} ` singular_relcycle_set n X {} = {singular_relcycle_set n X {}}"
        (is "?lhs = ?rhs")
  proof
    show "?lhs \ ?rhs"
      using peq assms
      by (auto simp: image_subset_iff homologous_rel_set_eq_relboundary simp flip: singular_boundary_set_eq_cycle_singleton)
    have "singular_relboundary n X {} 0"
      by simp
    with peq assms
    show "?rhs \ ?lhs"
      by (auto simp: image_iff simp flip: homologous_rel_eq_relboundary singular_boundary_set_eq_cycle_singleton)
  qed
  with peq assms show ?thesis
    unfolding trivial_group_def
    by (simp add:  carrier_relative_homology_group singular_boundary_set_eq_cycle_singleton [OF X])
qed

proposition homology_homotopy_axiom:
  assumes "homotopic_with (\h. h \ S \ T) X Y f g"
  shows "hom_induced p X S Y T f = hom_induced p X S Y T g"
proof (cases "p < 0")
  case True
  then show ?thesis
    by (simp add: hom_induced_trivial)
next
  case False
  then obtain n where peq: "p = int n"
    by (metis int_nat_eq not_le)
  have cont: "continuous_map X Y f" "continuous_map X Y g"
    using assms homotopic_with_imp_continuous_maps by blast+
  have im: "f \ (topspace X \ S) \ T" "g \ (topspace X \ S) \ T"
    using homotopic_with_imp_property assms by blast+
  show ?thesis
  proof
    fix c show "hom_induced p X S Y T f c = hom_induced p X S Y T g c"
    proof (cases "c \ carrier(relative_homology_group p X S)")
      case True
      then obtain a where a: "c = homologous_rel_set n X S a" "singular_relcycle n X S a"
        unfolding carrier_relative_homology_group peq by auto
      with assms homotopic_imp_homologous_rel_chain_maps show ?thesis
        by (force simp add: peq hom_induced_chain_map_gen cont im homologous_rel_set_eq)
    qed (simp add: hom_induced_default)
  qed
qed

proposition homology_excision_axiom:
  assumes "X closure_of U \ X interior_of T" "T \ S"
  shows
   "hom_induced p (subtopology X (S - U)) (T - U) (subtopology X S) T id
    \<in> iso (relative_homology_group p (subtopology X (S - U)) (T - U))
          (relative_homology_group p (subtopology X S) T)"
proof (cases "p < 0")
  case True
  then show ?thesis
    unfolding iso_def bij_betw_def relative_homology_group_def by (simp add: hom_induced_trivial)
next
  case False
  then obtain n where peq: "p = int n"
    by (metis int_nat_eq not_le)
  have cont: "continuous_map (subtopology X (S - U)) (subtopology X S) id"
    by (meson Diff_subset continuous_map_from_subtopology_mono continuous_map_id)
  have TU: "topspace X \ (S - U) \ (T - U) \ T"
    by auto
  show ?thesis
  proof (simp add: iso_def peq carrier_relative_homology_group bij_betw_def hom_induced_hom, intro conjI)
    show "inj_on (hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id)
         (homologous_rel_set n (subtopology X (S - U)) (T - U) `
          singular_relcycle_set n (subtopology X (S - U)) (T - U))"
      unfolding inj_on_def
    proof (clarsimp simp add: homologous_rel_set_eq)
      fix c d
      assume c: "singular_relcycle n (subtopology X (S - U)) (T - U) c"
        and d: "singular_relcycle n (subtopology X (S - U)) (T - U) d"
        and hh: "hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
                   (homologous_rel_set n (subtopology X (S - U)) (T - U) c)
               = hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id
                   (homologous_rel_set n (subtopology X (S - U)) (T - U) d)"
      then obtain scc: "singular_chain n (subtopology X (S - U)) c"
           and  scd: "singular_chain n (subtopology X (S - U)) d"
        using singular_relcycle by metis
      have "singular_relboundary n (subtopology X (S - U)) (T - U) c"
        if srb: "singular_relboundary n (subtopology X S) T c"
          and src: "singular_relcycle n (subtopology X (S - U)) (T - U) c" for c
      proof -
        have [simp]: "(S - U) \ (T - U) = T - U" "S \ T = T"
          using \<open>T \<subseteq> S\<close> by blast+
        have c: "singular_chain n (subtopology X (S - U)) c"
             "singular_chain (n - Suc 0) (subtopology X (T - U)) (chain_boundary n c)"
          using that by (auto simp: singular_relcycle_def mod_subset_def subtopology_subtopology)
        obtain d e where d: "singular_chain (Suc n) (subtopology X S) d"
          and e: "singular_chain n (subtopology X T) e"
          and dce: "chain_boundary (Suc n) d = c + e"
          using srb by (auto simp: singular_relboundary_alt subtopology_subtopology)
        obtain m f g where f: "singular_chain (Suc n) (subtopology X (S - U)) f"
                       and g: "singular_chain (Suc n) (subtopology X T) g"
                       and dfg: "(singular_subdivision (Suc n) ^^ m) d = f + g"
          using excised_chain_exists [OF assms d] .
        obtain h where
            h0:  "\p. h p 0 = (0 :: 'a chain)"
         and hdiff: "\p c1 c2. h p (c1-c2) = h p c1 - h p c2"
         and hSuc: "\p X c. singular_chain p X c \ singular_chain (Suc p) X (h p c)"
         and hchain: "\p X c. singular_chain p X c
                           \<Longrightarrow> chain_boundary (Suc p) (h p c) + h (p - Suc 0) (chain_boundary p c)
                             = (singular_subdivision p ^^ m) c - c"
          using chain_homotopic_iterated_singular_subdivision by blast
        have hadd: "\p c1 c2. h p (c1 + c2) = h p c1 + h p c2"
          by (metis add_diff_cancel diff_add_cancel hdiff)
        define c1 where "c1 \ f - h n c"
        define c2 where "c2 \ chain_boundary (Suc n) (h n e) - (chain_boundary (Suc n) g - e)"
        show ?thesis
          unfolding singular_relboundary_alt
        proof (intro exI conjI)
          show c1: "singular_chain (Suc n) (subtopology X (S - U)) c1"
            by (simp add: \<open>singular_chain n (subtopology X (S - U)) c\<close> c1_def f hSuc singular_chain_diff)
          have "chain_boundary (Suc n) (chain_boundary (Suc (Suc n)) (h (Suc n) d) + h n (c+e))
            = chain_boundary (Suc n) (f + g - d)"
              using hchain [OF d] by (simp add: dce dfg)
            then have "chain_boundary (Suc n) (h n (c + e))
                 = chain_boundary (Suc n) f + chain_boundary (Suc n) g - (c + e)"
              using chain_boundary_boundary_alt [of "Suc n" "subtopology X S"]
              by (simp add: chain_boundary_add chain_boundary_diff d hSuc dce)
            then have "chain_boundary (Suc n) (h n c) + chain_boundary (Suc n) (h n e)
                 = chain_boundary (Suc n) f + chain_boundary (Suc n) g - (c + e)"
              by (simp add: chain_boundary_add hadd)
            then have *: "chain_boundary (Suc n) (f - h n c) = c + (chain_boundary (Suc n) (h n e) - (chain_boundary (Suc n) g - e))"
              by (simp add: algebra_simps chain_boundary_diff)
            then show "chain_boundary (Suc n) c1 = c + c2"
            unfolding c1_def c2_def
              by (simp add: algebra_simps chain_boundary_diff)
            obtain "singular_chain n (subtopology X (S - U)) c2" "singular_chain n (subtopology X T) c2"
              using singular_chain_diff c c1 *
              unfolding c1_def c2_def
              by (metis add_diff_cancel_left' e g hSuc singular_chain_boundary_alt)
            then show "singular_chain n (subtopology (subtopology X (S - U)) (T - U)) c2"
              by (fastforce simp add: singular_chain_subtopology)
        qed
      qed
      then have "singular_relboundary n (subtopology X S) T (c - d) \
                 singular_relboundary n (subtopology X (S - U)) (T - U) (c - d)"
        using c d singular_relcycle_diff by metis
      with hh show "homologous_rel n (subtopology X (S - U)) (T - U) c d"
        apply (simp add: hom_induced_chain_map cont c d chain_map_ident [OF scc] chain_map_ident [OF scd])
        using homologous_rel_set_eq homologous_rel_def by metis
    qed
  next
    have h: "homologous_rel_set n (subtopology X S) T a
          \<in> (\<lambda>x. homologous_rel_set n (subtopology X S) T (chain_map n id x)) `
            singular_relcycle_set n (subtopology X (S - U)) (T - U)"
      if a: "singular_relcycle n (subtopology X S) T a" for a
    proof -
      obtain c' where c': "singular_relcycle n (subtopology X (S - U)) (T - U) c'"
                          "homologous_rel n (subtopology X S) T a c'"
        using a by (blast intro: excised_relcycle_exists [OF assms])
      then have scc': "singular_chain n (subtopology X S) c'"
        using homologous_rel_singular_chain that
        by (force simp: singular_relcycle)
      then show ?thesis
        using scc' chain_map_ident [of _ "subtopology X S"] c' homologous_rel_set_eq
        by fastforce
    qed
    have "(\x. homologous_rel_set n (subtopology X S) T (chain_map n id x)) `
          singular_relcycle_set n (subtopology X (S - U)) (T - U) =
          homologous_rel_set n (subtopology X S) T `
          singular_relcycle_set n (subtopology X S) T"
      by (force simp: cont h singular_relcycle_chain_map)
    then
    show "hom_induced n (subtopology X (S - U)) (T - U) (subtopology X S) T id `
          homologous_rel_set n (subtopology X (S - U)) (T - U) `
          singular_relcycle_set n (subtopology X (S - U)) (T - U)
        = homologous_rel_set n (subtopology X S) T ` singular_relcycle_set n (subtopology X S) T"
      by (simp add: image_comp o_def hom_induced_chain_map_gen cont TU
                       cong: image_cong_simp)
  qed
qed

subsection\<open>Additivity axiom\<close>

text\<open>Not in the original Eilenberg-Steenrod list but usually included nowadays,
following Milnor's "On Axiomatic Homology Theory".\

lemma iso_chain_group_sum:
  assumes disj: "pairwise disjnt \" and UU: "\\ = topspace X"
    and subs: "\C T. \compactin X C; path_connectedin X C; T \ \; ~ disjnt C T\ \ C \ T"
  shows "(\f. sum' f \) \ iso (sum_group \ (\S. chain_group p (subtopology X S))) (chain_group p X)"
proof -
  have pw: "pairwise (\i j. disjnt (singular_simplex_set p (subtopology X i))
                                   (singular_simplex_set p (subtopology X j))) \<U>"
  proof
    fix S T
    assume "S \ \" "T \ \" "S \ T"
    then show "disjnt (singular_simplex_set p (subtopology X S))
                      (singular_simplex_set p (subtopology X T))"
      using nonempty_standard_simplex [of p] disj
      by (fastforce simp: pairwise_def disjnt_def singular_simplex_subtopology image_subset_iff)
  qed
  have "\S\\. singular_simplex p (subtopology X S) f"
    if f: "singular_simplex p X f" for f
  proof -
    obtain x where x: "x \ topspace X" "x \ f ` standard_simplex p"
      using f nonempty_standard_simplex [of p] continuous_map_image_subset_topspace
      unfolding singular_simplex_def by fastforce
    then obtain S where "S \ \" "x \ S"
      using UU by auto
    have "f ` standard_simplex p \ S"
    proof (rule subs)
      have cont: "continuous_map (subtopology (powertop_real UNIV)
                                 (standard_simplex p)) X f"
        using f singular_simplex_def by auto
      show "compactin X (f ` standard_simplex p)"
        by (simp add: compactin_subtopology compactin_standard_simplex image_compactin [OF _ cont])
      show "path_connectedin X (f ` standard_simplex p)"
        by (simp add: path_connectedin_subtopology path_connectedin_standard_simplex path_connectedin_continuous_map_image [OF cont])
      have "standard_simplex p \ {}"
        by (simp add: nonempty_standard_simplex)
      then
      show "\ disjnt (f ` standard_simplex p) S"
        using x \<open>x \<in> S\<close> by (auto simp: disjnt_def)
    qed (auto simp: \<open>S \<in> \<U>\<close>)
    then show ?thesis
      by (meson \<open>S \<in> \<U>\<close> singular_simplex_subtopology that)
  qed
  then have "(\i\\. singular_simplex_set p (subtopology X i)) = singular_simplex_set p X"
    by (auto simp: singular_simplex_subtopology)
  then show ?thesis
    using iso_free_Abelian_group_sum [OF pw] by (simp add: chain_group_def)
qed

lemma relcycle_group_0_eq_chain_group: "relcycle_group 0 X {} = chain_group 0 X"
proof (rule monoid.equality)
  show "carrier (relcycle_group 0 X {}) = carrier (chain_group 0 X)"
    by (simp add: Collect_mono chain_boundary_def singular_cycle subset_antisym)
qed (simp_all add: relcycle_group_def chain_group_def)

proposition iso_cycle_group_sum:
  assumes disj: "pairwise disjnt \" and UU: "\\ = topspace X"
    and subs: "\C T. \compactin X C; path_connectedin X C; T \ \; \ disjnt C T\ \ C \ T"
  shows "(\f. sum' f \) \ iso (sum_group \ (\T. relcycle_group p (subtopology X T) {}))
                               (relcycle_group p X {})"
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.