# Zulip Chat Archive

## Stream: maths

### Topic: Working with subtypes.

#### Wrenna Robson (Dec 07 2020 at 22:34):

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 (Dec 07 2020 at 22:34):

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

#### Wrenna Robson (Dec 07 2020 at 22:35):

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

#### Yakov Pechersky (Dec 07 2020 at 22:39):

For any subtype, a subtype's value is `subtype.val`

or in your case `(ps : prime_spectrum R).val`

.

#### Alex J. Best (Dec 07 2020 at 22:40):

And to go the other way `⟨I, hI⟩`

is notation for a term of type `{I : ideal R // I.is_prime}`

#### Yakov Pechersky (Dec 07 2020 at 22:40):

And with the concomitant proof

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

#### Wrenna Robson (Dec 07 2020 at 22:40):

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

#### Yakov Pechersky (Dec 07 2020 at 22:41):

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 (Dec 07 2020 at 22:42):

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

#### Yakov Pechersky (Dec 07 2020 at 22:42):

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 (Dec 07 2020 at 22:43):

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 (Dec 07 2020 at 22:44):

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

#### Wrenna Robson (Dec 07 2020 at 22:44):

For which the angle-brackets are syntactic sugar?

#### Yakov Pechersky (Dec 07 2020 at 22:50):

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 (Dec 07 2020 at 22:50):

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 (Dec 07 2020 at 22:53):

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

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

#### Yakov Pechersky (Dec 07 2020 at 22:59):

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 (Dec 07 2020 at 23:02):

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 (Dec 07 2020 at 23:36):

Right! I forget about obtain.

Last updated: May 14 2021 at 20:13 UTC