Subsingleton (AddTorsor G P)

Stream: Is there code for X?

[Jesse Alama]

I'm working on formalizing some convex geometry and have reached a point where I need to prove that AddTorsor structures are unique. Specifically:

instance (G : Type*) [AddGroup G] (P : Type*) : Subsingleton (AddTorsor G P)

The problem is that after decomposing with cases and congr, I need to prove two equalities:

1. the vadd operations are equal
2. the vsub operations are equal

I'm stuck because I appear to be in circular dependency loop:

• to prove vsub equality, I'd use (p₁ -ᵥ p₂) +ᵥ p₂ = p₁, but each instance uses its own +ᵥ
• to prove vadd equality, I'd use the axiom (g +ᵥ p) -ᵥ p = g, but each instance uses its own -ᵥ

This comes up because I'm proving that translation in an affine subspace (more specifically, reducing an affine space to a vector subspace) is a homeomorphism, and the proof I've got uses subsingleton tactic, which requires the aforementioned instance.

Is there an existing instance I'm missing? I've gone hunting but haven't uncovered anything yet. If not, what's a good approach for proving typeclass uniqueness when operations are mutually dependent?

[Notification Bot]

This topic was moved here from #Is there code for X? > How to prove `Subsingleton (AddTorsor G P)` for ? by Jesse Alama.

[Aaron Liu]

I don't think these are unique?

[Aaron Liu]

what kind of uniqueness are you looking for?

[Aaron Liu]

maybe you want some sort of extensionality like "if the AddActions are the same then the AddTorsors are also the same"?

[Jesse Alama]

The theorem I'm reaching for is this:

theorem affineSubspace_translation_homeomorph (A : AffineSubspace ℝ E)
    [Nonempty A] [MetricSpace A]
    (p₀ : A) :
    ∃ (f : A ≃ₜ A.direction), ∀ p : A, f p = (p : E) -ᵥ (p₀ : E) := by sorry

I'm trying to translate an affine space to the origin and work with the result as a vector (sub)space rather than trying to do everything in the affine space. I got stuck in some type tetris and the (possibly unsound) principle above emerged.

[Aaron Liu]

Jesse Alama said:

The theorem I'm reaching for is this:

theorem affineSubspace_translation_homeomorph (A : AffineSubspace ℝ E)
    [Nonempty A] [MetricSpace A]
    (p₀ : A) :
    ∃ (f : A ≃ₜ A.direction), ∀ p : A, f p = (p : E) -ᵥ (p₀ : E) := by sorry

I'm trying to translate an affine space to the origin and work with the result as a vector (sub)space rather than trying to do everything in the affine space. I got stuck in some type tetris and the (possibly unsound) principle above emerged.

Why are you putting a metric space on A?

[Jesse Alama]

Ah, oops, the metric space doesn't need to be there, sorry.

[Aaron Liu]

this theorem looks very false, why do you think it should be true

[Aaron Liu]

oh no I got the quantifiers mixed up

[Aaron Liu]

this should be fine yeah

[Aaron Liu]

if you drop [MetricSpace A] then it should be fine

[Jesse Alama]

Yeah I think this should be sound. I've dropped the [MetricSpace A] but the issue remains.

[Aaron Liu]

docs#Homeomorph.vaddConst is what you're looking for

[Aaron Liu]

I found that by doing @loogle Homeomorph, AddTorsor

[loogle]

:search: Homeomorph.vaddConst, Homeomorph.vaddConst_symm_apply, and 4 more

[Jesse Alama]

Homeomorph.vaddConst and Homeomorph.vaddConst_symm_apply did the job -- thank you!! Sorry for the noise. I somehow convinced myself that that weird subsingleton was true.