Theory Ring_Misc

section ‹Ring Miscellaneous›
theory Ring_Misc

imports 
  "HOL-Algebra.RingHom" 
  "HOL-Algebra.QuotRing" 
  "HOL-Algebra.Embedded_Algebras"
begin

text ‹Some lemmas that may be considered as useful, and that helps for the Hilbert's basis proof›

lemma (in ring)carrier_quot: ‹ideal I R ⟹ carrier (R Quot I) = {{y⊕x | y. y∈I} |x. x∈carrier R}›
proof(safe)
  fix x
  assume h:‹ideal I R› ‹x ∈ carrier (R Quot I)›
  then have ‹∃xa∈carrier R. x = (⋃x∈I. {x ⊕ xa})› 
    unfolding FactRing_def A_RCOSETS_def RCOSETS_def cgenideal_def r_coset_def 
    by(simp) 
  then obtain y where ‹x = (⋃x∈I. {x ⊕ y}) ∧ y ∈carrier R› by blast
  with h show ‹∃xa. x = {y ⊕ xa |y. y ∈ I} ∧ xa ∈ carrier R›
    by(blast) 
next
  fix x xa
  assume ‹ideal I R› ‹xa ∈ carrier R›
  then show ‹{y ⊕ xa |y. y ∈ I} ∈ carrier (R Quot I)›
    unfolding FactRing_def A_RCOSETS_def RCOSETS_def cgenideal_def r_coset_def 
    apply simp
    apply(rule bexI[where x=xa])
    by auto
qed


context
  fixes A B h
  assumes ring_A: ‹ring A›
  assumes ring_B: ‹ring B›
  assumes h1:‹h∈ring_iso A B›
begin
interpretation ringA: ring A
  using ring_A by auto
interpretation ringB: ring B
  using ring_B by auto

interpretation rhr:ring_hom_ring A B h
  apply(unfold_locales)
  using h1 unfolding ring_iso_def by auto

lemma inv_img_exist:‹∀xa∈carrier B. ∃y.  y ∈ carrier A ∧ h y = xa›
  using h1 bij_betw_iff_bijections[of h ‹carrier A› ‹carrier B›] unfolding ring_iso_def
  by(auto)

lemma img_ideal_is_ideal:assumes j1:‹ideal I A› 
  shows ‹ideal (h ` I) B›
proof(intro idealI)
  show ‹ring B›
    by(simp add: ringB.ring_axioms) 
  from j1 show ‹subgroup (h ` I) (add_monoid B)›
    by (metis (no_types, lifting) additive_subgroup_def ideal_def rhr.img_is_add_subgroup)
  fix a x
  assume hyp:‹a ∈ h ` I› ‹x ∈ carrier B› 
  with j1 show fst:‹x ⊗⇘B⇙ a ∈ h ` I›
    by (smt (verit, ccfv_threshold) inv_img_exist h1  ideal.I_l_closed ideal.Icarr image_iff ring_iso_memE(2))
  from j1 show ‹a ⊗⇘B⇙ x ∈ h ` I› 
    using inv_img_exist fst hyp(2) 
    by (smt (verit, best) hyp(1) ideal.I_r_closed ideal.Icarr image_iff rhr.hom_mult)
qed


lemma img_in_carrier_quot:‹∀x∈ carrier (A Quot I). h ` x ∈ carrier (B Quot (h`I))› if j:‹ideal I A› for I
proof(subst ringA.carrier_quot(1)[OF j],subst ringB.carrier_quot[of ‹h`I›], safe)
  show ‹ideal (h ` I) B› 
    using img_ideal_is_ideal that by blast
next
  fix x xa
  assume h:‹xa ∈ carrier A›
  then show ‹∃x. h ` {y ⊕⇘A⇙ xa |y. y ∈ I} = {y ⊕⇘B⇙ x |y. y ∈ h ` I} ∧ x ∈ carrier B›
    apply(intro exI[where x=‹h xa›])
    apply(safe)       
    using h1 j ideal.Icarr ring_iso_memE(3) that apply fastforce
    using h1 ideal.Icarr image_iff mem_Collect_eq ring_iso_memE(3) that apply fastforce
    by (meson h1 ring_iso_memE(1))
qed

lemma f8:‹xa∈carrier B ∧ xb∈I ⟹h(xb ⊕⇘A⇙ inv_into (carrier A) h xa) = h xb  ⊕⇘B⇙ xa› if j:‹ideal I A› for I xb xa
proof -
  assume "xa ∈ carrier B ∧ xb ∈ I"
  then show ?thesis
    using inv_img_exist f_inv_into_f[of xa h ‹carrier A›] ideal.Icarr[OF that, of xb] 
      inv_into_into[of xa h] 
    by(auto)
qed

lemma f9:‹∀xa∈carrier B. ∀xb∈carrier A. ∃y. h y = h xb ⊕⇘B⇙ xa›
  using f8 ringA.oneideal by blast

lemma img_over_set_is_iso: ‹ideal I A ⟹ ((`) h) ∈ ring_iso (A Quot I) (B Quot (h`I))› for I
proof(rule ring_iso_memI)
  fix x
  assume k:‹ideal I A› ‹x ∈ carrier (A Quot I)›
  then show ‹h ` x ∈ carrier (B Quot h ` I)›
    using h1 ringA.ring_axioms ringB.ring_axioms
    by(simp add:img_in_carrier_quot)
  fix y
  {
    fix xa xb xc
    assume g:‹xa ∈ x› ‹xb ∈ y› ‹xc ∈ I› ‹ideal I A›‹x ∈ a_rcosets⇘A⇙ I› ‹y ∈ a_rcosets⇘A⇙ I›
    have xa:‹xa ∈ carrier A› 
      using abelian_subgroup.a_rcosets_carrier abelian_subgroupI3 g(1) g(5) 
        ideal_def k(1) ring_def by blast
    have xb:‹xb ∈carrier A› 
      using abelian_subgroup.a_rcosets_carrier abelian_subgroupI3 g(2) g(6) 
        ideal_def k(1) ring_def by blast
    have xc:‹xc∈carrier A›
      using g(3) k(1) ringA.ideal_is_subalgebra ringA.subalgebra_in_carrier by fastforce
    have ‹∃x∈x. ∃xd∈y. ∃xe∈I. h (xc ⊕⇘A⇙ xa ⊗⇘A⇙ xb) = h xe ⊕⇘B⇙ h x ⊗⇘B⇙ h xd ›
      apply(rule bexI[where x=xa]) 
       apply(rule bexI[where x=xb]) 
        apply(rule bexI[where x=xc]) 
      using g rhr.hom_add[OF xc ] rhr.hom_mult[OF xa xb] 
      using ringA.m_closed xa xb by presburger+ 
  }note fst_prf=this 
  {fix xa xb xc
    assume g:‹xa ∈ x› ‹xb ∈ y› ‹xc ∈ I› ‹ideal I A›‹x ∈ a_rcosets⇘A⇙ I› ‹y ∈ a_rcosets⇘A⇙ I›
    have xa:‹xa ∈ carrier A› 
      using abelian_subgroup.a_rcosets_carrier abelian_subgroupI3 g(1) g(5) 
        ideal_def k(1) ring_def by blast
    have xb:‹xb ∈carrier A› 
      using abelian_subgroup.a_rcosets_carrier abelian_subgroupI3 g(2) g(6) 
        ideal_def k(1) ring_def by blast
    have xc:‹xc∈carrier A›
      using g(3) k(1) ringA.ideal_is_subalgebra ringA.subalgebra_in_carrier by fastforce
    have ‹∃ya∈x. ∃y∈y. ∃yb∈I. h xc ⊕⇘B⇙ h xa ⊗⇘B⇙ h xb = h (yb ⊕⇘A⇙ ya ⊗⇘A⇙ y)›
      apply(rule bexI[where x=xa]) 
       apply(rule bexI[where x=xb])
        apply(rule bexI[where x=xc]) 
      using g rhr.hom_add[OF xc ] rhr.hom_mult[OF xa xb] 
      using ringA.m_closed xa xb by presburger+ }note snd_prf=this
  assume k1:‹y ∈ carrier (A Quot I)›
  with k show ‹h ` (x ⊗⇘A Quot I⇙ y) = h ` x ⊗⇘B Quot h ` I⇙ h ` y›
    by(auto simp:FactRing_def image_iff rcoset_mult_def r_coset_def a_r_coset_def snd_prf fst_prf)
  from k k1 show ‹h ` (x ⊕⇘A Quot I⇙ y) = h ` x ⊕⇘B Quot h ` I⇙ h ` y›
    apply(simp add:FactRing_def rcoset_mult_def r_coset_def a_r_coset_def)
    using h1 ring_A ring_B unfolding ring_iso_def FactRing_def rcoset_mult_def r_coset_def a_r_coset_def
    by (metis (no_types, lifting) abelian_subgroup.a_rcosets_carrier abelian_subgroupI3
        ideal.axioms(1) mem_Collect_eq ring_def set_add_hom)
next 
  assume k:‹ideal I A›
  have important:‹xa ∈ carrier (B Quot h ` I) ⟹ ∃y∈carrier (A Quot I). h ` y = xa› for xa
  proof(rule bexI[where x=‹inv_into (carrier A) h ` xa›])
    assume g:‹xa ∈ carrier (B Quot h ` I)›
    then show ‹h ` inv_into (carrier A) h ` xa = xa›
      by (metis Sup_le_iff bij_betw_def img_ideal_is_ideal h1 image_inv_into_cancel k 
          ringB.canonical_proj_vimage_in_carrier ring_iso_memE(5) subset_refl)
    {fix x
      assume g1:‹x∈carrier B› ‹ xa = (⋃xa∈I. {h xa ⊕⇘B⇙ x})›
      {fix xaa
        assume g2:‹xaa ∈ I›
        with g1 have ‹∃xa∈I. (SOME y. y ∈ carrier A ∧ h y = h xaa ⊕⇘B⇙ x) = xa ⊕⇘A⇙ inv_into (carrier A) h x›
          by (smt (verit, del_insts) bij_betw_def bij_betw_iff_bijections h1 ideal.Icarr 
              inv_into_f_f k rhr.hom_add ringA.add.m_closed ring_iso_memE(5) some_equality)
      }note 2=this
      {fix xaa
        assume ‹xaa∈I›
        with g1 have ‹xaa ⊕⇘A⇙ inv_into (carrier A) h x = (SOME y. y ∈ carrier A ∧ h y = h xaa ⊕⇘B⇙ x)›
          using h1 ring_A ring_B unfolding ring_iso_def
          by (smt (verit, del_insts) bij_betw_def k inv_img_exist f8 h1 ideal.Icarr
              inv_into_f_f mem_Collect_eq ringA.add.m_closed someI_ex)
      }note 3=this
      from g1 have ‹∃xa∈carrier A. (λx. SOME y. y ∈ carrier A ∧ h y = x) ` (⋃xa∈I. {h xa ⊕⇘B⇙ x}) = (⋃x∈I. {x ⊕⇘A⇙ xa})›
        apply(intro bexI[where x=‹inv_into (carrier A) h x›]) 
        using inv_img_exist image_eqI inv_into_into[of x h ‹carrier A›] 
        by(auto simp: 2 3) 
    }note 1 =this
    from g show ‹inv_into (carrier A) h ` xa ∈ carrier (A Quot I)›
      unfolding FactRing_def inv_into_def A_RCOSETS_def RCOSETS_def r_coset_def by(auto simp:1)  
  qed
  have imp2:‹∀J⊆carrier A. ∀K⊆carrier A. h ` J = h ` K ⟶ J = K›
    unfolding image_def using h1  apply(safe) 
    using h1 ring_A ring_B unfolding ring_iso_def 
    by (smt (verit, ccfv_SIG) bij_betw_iff_bijections in_mono mem_Collect_eq) +
  with important have important3:‹xa ∈ carrier (B Quot h ` I) 
  ⟹ ∃!y∈carrier (A Quot I). h ` y = xa› for xa
    apply(safe) 
      apply blast
     apply (metis Sup_le_iff equalityE k ringA.canonical_proj_vimage_in_carrier)
    by (metis Sup_le_iff dual_order.refl k ringA.canonical_proj_vimage_in_carrier)
  have bij_inv:‹bij_betw (inv_into (carrier A) h) (carrier B) (carrier A)›
    by (simp add: bij_betw_inv_into h1 ring_iso_memE(5))
  with k show ‹h ` 𝟭⇘A Quot I⇙ = 𝟭⇘B Quot h ` I⇙› 
    apply(auto simp:image_def FactRing_def rcoset_mult_def r_coset_def a_r_coset_def) [1]
     apply (smt (verit, ccfv_threshold) h1 ideal.Icarr insert_iff ringA.one_closed ring_iso_memE(3) ring_iso_memE(4))
    by (metis (full_types) h1 ideal.Icarr ringA.one_closed ring_iso_memE(3) ring_iso_memE(4) singletonI)
  show ‹bij_betw ((`) h) (carrier (A Quot I)) (carrier (B Quot h ` I))›
  proof(intro  bij_betw_byWitness[where ?f' = "(`) (inv_into (carrier A) h)"])
    from k show ‹∀a∈carrier (A Quot I). inv_into (carrier A) h ` h ` a = a›
      apply(intro ballI)
      apply(subst inv_into_image_cancel) 
      using bij_betw_def h1 ring_A ring_B unfolding ring_iso_def apply blast
       apply (metis FactRing_def abelian_subgroup.a_rcosets_carrier 
          abelian_subgroupI3 ideal_def partial_object.select_convs(1) ring_def)
      by(simp)
    from k show ‹∀a'∈carrier (B Quot h ` I). h ` inv_into (carrier A) h ` a' = a'›
      using ring_A ring_B h1 unfolding ring_iso_def
      by (metis (no_types, lifting) Sup_le_iff bij_betw_def img_ideal_is_ideal image_inv_into_cancel
          mem_Collect_eq ringB.canonical_proj_vimage_in_carrier subset_refl)
    from k show ‹(`) h ` carrier (A Quot I) ⊆ carrier (B Quot h ` I)›
      using img_in_carrier_quot by blast
    from k show ‹(`) (inv_into (carrier A) h) ` carrier (B Quot h ` I) ⊆ carrier (A Quot I)›
      apply(subst (1) image_def)
      apply(safe)  
      by (metis ‹∀a∈carrier (A Quot I). inv_into (carrier A) h ` h ` a = a› important3)
  qed
qed   
end

lemma Quot_iso_cgen:‹a∈carrier A ∧ b:carrier B ∧ cring A ∧ cring B ∧ h ∈ ring_iso A B ∧  h(a) = b 
⟹ A Quot (cgenideal A a) ≃ B Quot (cgenideal B b)›
  unfolding is_ring_iso_def ring_iso_def 
proof(subst ex_in_conv[symmetric]) 
  assume h1:‹a∈carrier A ∧ b:carrier B ∧cring A ∧ cring B ∧ h ∈ {h ∈ ring_hom A B. bij_betw h (carrier A) (carrier B)} ∧ h a = b›
  have h1':‹h ∈ ring_iso A B›
    using h1 apply(fold ring_iso_def) by simp
  interpret ringA: cring A
    using h1 by auto
  interpret ringB: cring B
    using h1 by simp
  have f1:‹∀xa∈carrier B. ∃y.  y ∈ carrier A ∧ h y = xa›
    by (metis (no_types, lifting) bij_betw_iff_bijections h1 mem_Collect_eq)
  have f0:‹ideal (PIdl⇘A⇙ a) A ∧ ideal (PIdl⇘B⇙ b) B›
    using ringA.cgenideal_ideal[of a] ringB.cgenideal_ideal[of b] h1 by(simp)
  then have f2:‹(carrier (A Quot PIdl⇘A⇙ a)) = {{y⊕⇘A⇙x | y. y∈PIdl⇘A⇙ a} |x. x∈carrier A}
› ‹(carrier (B Quot PIdl⇘B⇙ b)) = {{y⊕⇘B⇙x | y. y∈PIdl⇘B⇙ b} |x. x∈carrier B}›
    using ringA.carrier_quot ringB.carrier_quot by simp+
  then have ‹h`(PIdl⇘A⇙ a) = (PIdl⇘B⇙ b)›
    unfolding image_def cgenideal_def 
  proof(safe) 
    fix x xa xb
    assume h2:‹ carrier (A Quot {x ⊗⇘A⇙ a |x. x ∈ carrier A}) = {{y ⊕⇘A⇙ x |y. y ∈ {x ⊗⇘A⇙ a |x. x ∈ carrier A}} |x. x ∈ carrier A}›
      ‹carrier (B Quot {x ⊗⇘B⇙ b |x. x ∈ carrier B}) = {{y ⊕⇘B⇙ x |y. y ∈ {x ⊗⇘B⇙ b |x. x ∈ carrier B}} |x. x ∈ carrier B}›
      ‹xb ∈ carrier A›
    then show ‹∃x. h (xb ⊗⇘A⇙ a) = x ⊗⇘B⇙ b ∧ x ∈ carrier B›
      using h1 ring_iso_def ring_iso_memE(1) ring_iso_memE(2) by fastforce
  next
    fix x xa
    assume h2:‹ carrier (A Quot {x ⊗⇘A⇙ a |x. x ∈ carrier A}) = {{y ⊕⇘A⇙ x |y. y ∈ {x ⊗⇘A⇙ a |x. x ∈ carrier A}} |x. x ∈ carrier A}›
      ‹carrier (B Quot {x ⊗⇘B⇙ b |x. x ∈ carrier B}) = {{y ⊕⇘B⇙ x |y. y ∈ {x ⊗⇘B⇙ b |x. x ∈ carrier B}} |x. x ∈ carrier B}›
      ‹xa ∈ carrier B›
    show ‹∃x∈{x ⊗⇘A⇙ a |x. x ∈ carrier A}. xa ⊗⇘B⇙ b = h x ›
      using f1 h1 h1' h2(3) ring_iso_memE(2) by fastforce
  qed
  then have ‹∀x∈(PIdl⇘B⇙ b). ∃!y∈(PIdl⇘A⇙ a). h y = x›
    by (smt (verit) bij_betw_iff_bijections f0 h1 ideal.Icarr image_def mem_Collect_eq)
  then have ‹x∈carrier (A Quot {x ⊗⇘A⇙ a |x. x ∈ carrier A}) ⟹ ∃y'∈carrier A. x = {y⊕⇘A⇙y' | y. y∈PIdl⇘A⇙ a}› for x
  proof -
    assume a1: "x ∈ carrier (A Quot {x ⊗⇘A⇙ a |x. x ∈ carrier A})"
    have f2: "∀Aa Ab. Ab ∉ carrier (A Quot Aa) ∨ ¬ ideal Aa A 
              ∨ (∃a. Ab = {aa ⊕⇘A⇙ a |aa. aa ∈ Aa} ∧ a ∈ carrier A)"
      using ringA.carrier_quot by auto
    have "x ∈ carrier (A Quot PIdl⇘A⇙ a)"
      using a1 by (simp add: cgenideal_def)
    then show ?thesis
      using f2 f0 by blast
  qed
  show ‹∃x. x ∈ {h ∈ ring_hom (A Quot PIdl⇘A⇙ a) (B Quot PIdl⇘B⇙ b).
              bij_betw h (carrier (A Quot PIdl⇘A⇙ a)) (carrier (B Quot PIdl⇘B⇙ b))}›
    apply(fold ring_iso_def)
    apply(intro exI[where x=‹λx. h`x›])
    using ‹h ` (PIdl⇘A⇙ a) = PIdl⇘B⇙ b› f0 h1' img_over_set_is_iso ringA.ring_axioms ringB.ring_axioms 
    by force
qed


end