Working with subtypes.

Stream: maths

[Wrenna Robson]

Suppose I have terms I : ideal R, hI : I.is_prime, (with R a comm_ring), and the type prime_spectrum R = {I : ideal R // I.is_prime}.

How does one go "well I clearly have a term of type prime_spectrum R, it's "I", suitably reinterpreted".

[Wrenna Robson]

I thought there would just be a function but I can't see it.

[Wrenna Robson]

Maybe this should have been in "Is there code for X?"

[Yakov Pechersky]

For any subtype, a subtype's value is subtype.val or in your case (ps : prime_spectrum R).val.

[Alex J. Best]

And to go the other way ⟨I, hI⟩ is notation for a term of type {I : ideal R // I.is_prime}

[Yakov Pechersky]

And with the concomitant proof

lemma is_prime_ps (ps : prime_spectrum R) : ps.val.is_prime := ps.property

[Wrenna Robson]

Alex, that's perfect I think. Thank you.

[Yakov Pechersky]

That notation works, but only if it can be inferred that that is the exact type you need. Otherwise, you might have complaints. Sorry, I misread your initial message in the opposite direction.

[Wrenna Robson]

That's alright! It works for me in context.

[Yakov Pechersky]

You might have something like

def prime_spectrum.of_is_prime {I : ideal R} (hI : I.is_prime) : prime_spectrum R := ⟨I, hI⟩

[Yakov Pechersky]

that way you don't even have to think about supplying the I as long as you have the associated I.is_prime hypothesis in hand.

[Yakov Pechersky]

The "function" you asked about is docs#subtype.mk

[Wrenna Robson]

For which the angle-brackets are syntactic sugar?

[Yakov Pechersky]

As far as I understand, the brackets construct or destruct, based on the context. They construct or destruct inductive types. In this case, subtype p for some p : \a \to Prop is a structure with two required records, so you provide those in the ⟨I, hI⟩ construction.

[Yakov Pechersky]

And in the case of a destruction, you could "unwrap" a subtype p like so:

def ideal_from_prime_spectrum : prime_spectrum R -> ideal R
| ⟨I, hI⟩ := I

[Yakov Pechersky]

Of course, you can use these brackets to make something like

(⟨rfl, rfl⟩ : and (1 = 1) (2 = 2))

[Yakov Pechersky]

I find these brackets useful in places where I need to prove something about a complex statement, lets say

import tactic.default

example : ∃! (x : ℕ), ∀ y, x ≤ y ∧ x + x = x :=
begin
  refine ⟨0, _, _⟩,
  { intro y,
    exact ⟨nat.zero_le y, rfl⟩ },
  { intros z hz,
    obtain ⟨zle, zeq⟩ := hz 0,
    exact le_antisymm zle (nat.zero_le z) },
end

[Yakov Pechersky]

The first refine is an example of a similar tactic step like use 0 would be, where we are piece-meal constructing the full exists_unique term. The first exact shows how one can construct an and term using the brackets. The obtain line shows how we can destruct a similar and term.

[Wrenna Robson]

Right! I forget about obtain.