John Hughes (Jul 21 2025 at 17:56): John Hughes (Jul 21 2025 at 17:56):Having tried to define the projective plane as the quotient of $R^3 - {(0,0,0)}$ by the relation that $(x, y, z)$ is the same as $(cx, cy, cz)$ for any nonzero real number $c$, I realized that I wasn't sure whether Abs (0,0,0) was in fact an element of the resulting quotient type. To try to resolve that question, I built a much simpler and smaller case, one where I think the quotient type should have exactly one element. In this example, the element E of the original type serves the role of $(0,0,0)$ in the RP2 example, namely, it's something I don't want to consider in the quotient. And making elements A and B equivalent is a proxy for the "scalar multiple" relation. As you might guess from the names, the original type definition had constructors A,B,C,D,E, but I eventually simplified down to this (which was copy-pasted and then adjusted from the definition of rat in Isabelle):
theory Scratch5
imports Complex_Main
begin
datatype b = A | B | E
definition prel :: "b ⇒ b ⇒ bool"
where "prel = (λx y. (x ≠ E ∧ y ≠ E)∧ ((x = y) ∨
((x = A) ∧ (y = B)) ∨
((x = B) ∧ (y = A))
))"
lemma arel: shows "prel A A" using prel_def using b.distinct by presburger
lemma exists_prel_refl: "∃x. prel x x" using arel by auto
lemma symp_prel: "symp prel" by (metis prel_def sympI)
lemma transp_prel: "transp prel" by (metis prel_def transpI)
lemma part_equivp_prel: "part_equivp prel"
by (simp add: exists_prel_refl part_equivpI symp_prel transp_prel)
quotient_type q = "b" / partial: "prel"
morphisms Rep_p Abs_p
using part_equivp_prel .
lemma Domainp_cr_proj [transfer_domain_rule]: "Domainp pcr_q = (λx .( (x ≠ E)) ∧ prel x x)"
by (simp add: prel_def q.domain_eq)
thm q.domain_eq
thm Abs_p_def
theorem
shows "card (UNIV::q set) = 1" by sledgehammer
Sledgehammer can't prove that theorem. It also cannot prove that the cardinality is 2 or 3. This leaves me ignorant of what the whole quotient_type thing is doing.
Concrete questions:
p = q in RP2; that means that prel (Rep_p p) (Rep_p q) is true, and then I'd like to go on and say that if Rep_p p = (x, y, z) and Rep_p q = (a, b, c), then (x, y, z) must be a nonzero scalar multiple of (a, b, c), and that neither of them is (0,0,0). I thought that was the kind of thing I'd get by using a partial equivalence relation, but maybe I was mistaken. Can anyone enlighten me? Mathias Fleury (Jul 21 2025 at 18:21):It is a bit too much for sledgehammer in one step:
theorem
shows "card (UNIV::q set) = 1"
proof -
have ‹Abs_p A ∈ (UNIV::q set)›
by simp
moreover have ‹x ∈ (UNIV::q set) ⟹ prel (Rep_p x) A› for x
apply (cases x)
apply (auto simp: prel_def)
apply (metis (lifting) Quotient3_q Quotient3_rep_reflp prel_def)
by (metis Quotient3_q Quotient3_rep_reflp b.exhaust prel_def)
ultimately have ‹(UNIV::q set) = {Abs_p A}›
using Quotient_rel_abs2[OF Quotient_q] by fastforce
then show ?thesis
using card_1_singleton_iff by auto
qed
Thank you. With luck, I can imitate this in my larger example. I'm very relieved to find that the cardinality is, indeed, 1. :)
Last updated: Aug 13 2025 at 08:30 UTC