Quotient involving real^3 · Beginner Questions

I want to take a quotient of R^3 minus the origin to define the real projective 2-space RP^2. I did this once using real×real×real, but now I find that I'd like to use things like Analysis.Cross3, which seems to require vectors.

I simply replaced the types everywhere (and I've "sorry"ed some proofs to make things shorter):

theory "Chapter1-2-alt-quo"
  imports Complex_Main "HOL-Analysis.Cross3"
begin

type_synonym v3 = "real^3"
definition map_vec where
"map_vec f g v = vec_lambda (map_fun g f (vec_nth v))"
functor map_vec
  unfolding map_vec_def
   apply fastforce
  using eq_id_iff by fastforce

definition projrel :: "v3 ⇒ v3 ⇒ bool"
  where "projrel = (λx y. (x ≠ 0 ∧ y ≠ 0) ∧  (∃ (c::real) . c ≠ 0 ∧ (x =  c *⇩R y)))"

lemma exists_projrel_refl: "∃x. projrel x x"
proof -
  have "vector[1, 0, 0] =  1 *⇩R vector[1, 0, 0]"  by simp
  then show ?thesis using projrel_def scaleR_one zero_neq_one  by metis
qed

lemma nonzero_inverse: "((c::real) ≠ 0) ⟹ ((1/c) ≠ 0)" by simp

lemma divide_through: "((c::real) ≠ 0) ⟹ (a = c*q) ⟹ ((1/c)*a = q)" by simp

lemma symp_projrel: "symp projrel"
proof -
  show ?thesis  unfolding symp_def
  proof (clarify)
    fix x y
    assume a: "projrel x y"
    obtain c where a1:"(x ≠ 0 ∧ y ≠ 0) ∧   c ≠ 0 ∧
         (x = c *⇩R y)" using a projrel_def by meson
    have inv: "(1/c) * c = 1" using a1 by auto
    from a1 have "(1/c) *⇩R x = (1/c) *⇩R (c *⇩R y)" by auto
    also have "... = 1 *⇩R y"  using inv by simp
    also have "... =  y" by simp
    finally have "(1/c) *⇩R  x = y" by auto
    then  show "projrel y x"  by (metis a1 projrel_def scaleR_zero_left)
  qed
qed

lemma transp_projrel: "transp projrel"
  sorry

lemma part_equivp_projrel: "part_equivp projrel"
  by (rule part_equivpI [OF exists_projrel_refl symp_projrel transp_projrel])

quotient_type rp2 = v3 / partial: "projrel"
  morphisms Rep_Proj Abs_Proj
  using part_equivp_projrel .

lemma Domainp_cr_proj [transfer_domain_rule]: "Domainp pcr_rp2 = (λx .( (x ≠ 0) ∧ projrel x x))"
  using  by sledgehammer

(*  by (simp add: projrel_def rp2.domain_eq) *)

end

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "Numeral_Type.bit1" found.

As a novice, I have no idea what Numeral_Type.bit1 is, or why it would arise here. But more important, whatever is going on seems to have messed things up enough that rp2.domain_eq, which was automatically defined when I used real×real×real,is no longer available, so the commented-out proof at the end no longer works.

Is my situation hopeless? Does Isabelle not want me to make quotients of real vector spaces?

Manuel Eberl (Oct 07 2025 at 18:46):

Just FYI, I do have a version of the cross product development that I intend to put in the distribution instead of the current one. Mine is strictly more general; it works for any three-dimensional real vector space with distinguished x, y, z axis.

John Hughes (Oct 07 2025 at 23:41):

I eagerly await that. I'd still like to be able to do the quotient on real^3, but given the lack of answers to earlier questions, that may have to await another life where I have the time and energy to learn about dead variables and bounded natural functors, etc.

Manuel Eberl (Oct 08 2025 at 19:18):

Oh and by the way, I think you can ignore the message about the "parametrized correspondence relation". I don't think you need that.

John Hughes (Oct 09 2025 at 15:48):

lemma Domainp_cr_proj [transfer_domain_rule]: "Domainp cr_rp2 = (λx .( (x ≠ 0) ∧ projrel x x))"
  using projrel_def rp2.domain by presburger

we actually get a quotient that's usable. (The difference is between pcr_rp2 and cr_rp2 for those who don't feel like playing "Where's Waldo" with the code.)

Stream: Beginner Questions

Topic: Quotient involving real^3

John Hughes (Oct 03 2025 at 17:17):

Manuel Eberl (Oct 07 2025 at 18:46):

John Hughes (Oct 07 2025 at 23:41):

Manuel Eberl (Oct 08 2025 at 19:18):

John Hughes (Oct 09 2025 at 15:48):