Search code examples
isabelle

Ring structure induced by a bijection

Given a ring, together with a bijection to another set (n.b. set not type), it ought to be "trivial" to define the (unique) induced ring structure on the "other set" that makes the bijection an isomorphism. But my proof that tries to use this takes 101 lines (plus definitions and lemmas). Is there another approach using e.g. "lifting" that makes the whole thing fall out more easily?

Here's an example that could be filled in to do what I want:

theory InducedRing
  imports "HOL-Algebra.QuotRing"
begin

lemma
  assumes "ring โ„›" "bij_betw ฯ† (carrier โ„›) S"
  obtains ๐’ฎ where "ring ๐’ฎ" and "carrier ๐’ฎ = S" and "ฯ† โˆˆ ring_hom โ„› ๐’ฎ"
  sorry

end

Feel free to rewrite this to an equivalent or stronger statement (e.g., reverse the direction of \<phi> or even assume a pair of inverse bijections, make the hypotheses part of a locale definition, assert uniqueness of \<S>, change the names according to your own taste....)

The goal is to make the proof feel short and natural. I'm hoping there's a theorem somewhere in HOL-Algebra or another library that will make this easy, but sledgehammer was not able to find it for me -- at least, not with this version of the statement.

Solution

  • I do not think you will get around proofing the ring axioms, except if someone has already proven a similar lemma. I have no experience with HOL-Algebra, so maybe there is something nicer.

    Luckily automation seems to handle them fairly well (except one, where auto needs a bit of help). I obtained the proofs by hitting the goal with auto and sledgehammering what was left to search for relevant lemmas to add to auto.

    lemma
  assumes "ring โ„›" "bij_betw ฯ† (carrier โ„›) S"
  obtains ๐’ฎ where "ring ๐’ฎ" and "carrier ๐’ฎ = S" and "ฯ† โˆˆ ring_hom โ„› ๐’ฎ"
proof-
  interpret โ„›: ring โ„› 
    using assms(1) .

  (* Define the ring *)
  let ?Z = "ฯ† (zero โ„›)"
  let ?O = "ฯ† (one โ„›)"
  let ?mult = "ฮปx y . ฯ† (inv_into (carrier โ„›) ฯ† x โŠ—โ‡˜โ„›โ‡™ inv_into (carrier โ„›) ฯ† y)" 
  let ?add = "ฮปx y . ฯ† (inv_into (carrier โ„›) ฯ† x โŠ•โ‡˜โ„›โ‡™ inv_into (carrier โ„›) ฯ† y)" 
  let ?๐’ฎ = "โฆ‡ carrier = S, mult = ?mult , one = ?O, zero = ?Z, add = ?add, 
    โ€ฆ = (undefined :: 'd) โฆˆ :: ('c, 'd) ring_scheme"
  
  show thesis
  proof(rule that[of ?๐’ฎ])
    (* The only part where auto needed some help *)
    have helper: "โˆƒyโˆˆS. ฯ† (inv_into (carrier โ„›) ฯ† x โŠ•โ‡˜โ„›โ‡™ inv_into (carrier โ„›) ฯ† y) = ฯ† ๐Ÿฌโ‡˜โ„›โ‡™" 
      if "x โˆˆ S" for x 
      using assms that by (intro bexI[where x="ฯ† (โŠ–โ‡˜โ„›โ‡™ (inv_into (carrier โ„›) ฯ† x))"])
        (auto intro: bij_betw_apply 
          simp add: ring.ring_simprules bij_betw_imp_inj_on bij_betw_imp_surj_on inv_into_into)
      
    show "ring ?๐’ฎ"
      using assms by unfold_locales 
        (auto intro: bij_betw_apply simp add: ring.ring_simprules bij_betw_inv_into_right 
          bij_betw_imp_inj_on bij_betw_imp_surj_on inv_into_into Units_def helper)
  next
    show "carrier ?๐’ฎ = S"
      by simp
  next
    from assms(2) show "ฯ† โˆˆ ring_hom โ„› ?๐’ฎ"
      by (intro ring_hom_memI) (auto intro: bij_betw_apply simp add: bij_betw_inv_into_left)
  qed
qed

    In my proof (and yours as well) I explicitly give the definitions of the induced ring, which makes the obtains in the goal statement a bit pointless in my opinion. Similarly, the S can be computed from carrier โ„›. So why not have the concrete definitions available on the toplevel, similar to for example this:

    abbreviation "bij_ring โ„› ฯ† โ‰ก โฆ‡carrier = ฯ† ` carrier โ„›, 
    mult = ฮปx y . ฯ† (inv_into (carrier โ„›) ฯ† x โŠ—โ‡˜โ„›โ‡™ inv_into (carrier โ„›) ฯ† y), one = ฯ† (one โ„›), 
    zero = ฯ† (zero โ„›), add = ฮปx y . ฯ† (inv_into (carrier โ„›) ฯ† x โŠ•โ‡˜โ„›โ‡™ inv_into (carrier โ„›) ฯ† y), 
    โ€ฆ = (undefined :: 'd) โฆˆ :: ('c, 'd) ring_scheme"

lemma
  assumes "ring โ„›" "bij_betw ฯ† (carrier โ„›) (ฯ† ` (carrier โ„›))"
  shows "ring (bij_ring โ„› ฯ†)" and "ฯ† โˆˆ ring_hom โ„› (bij_ring โ„› ฯ†)"
proof-
  interpret โ„›: ring โ„› 
    using assms(1) . 
  (* Sadly it still needs help *)
  from assms have helper: "โˆƒxโˆˆcarrier โ„›. ฯ† (y โŠ•โ‡˜โ„›โ‡™ x) = ฯ† ๐Ÿฌโ‡˜โ„›โ‡™" 
    if "y โˆˆ carrier โ„›" for y 
    using that by (metis โ„›.add.r_inv_ex)

  from assms show "ring (bij_ring โ„› ฯ†)"
    by unfold_locales (auto simp add: bij_betw_inv_into_left
        โ„›.add.m_assoc bij_betw_imp_inj_on ring.ring_simprules Units_def helper)
  from assms(2) show "ฯ† โˆˆ ring_hom โ„› (bij_ring โ„› ฯ†)"
    by (intro ring_hom_memI) (auto intro: bij_betw_apply simp add: bij_betw_inv_into_left)
qed

    This also seems to simplify the proofs a bit. Sadly there is some duplication in the goal statement, but I cannot see a way to improve this now.