support_add

Stream: new members

[Damiano Testa]

Dear All,

I am trying to get Lean to check that the support of the sum of two polynomials is contained in the union of the supports. I found the command finsupp.support_add, claiming to do exactly this. Unfortunately, with the #mwe below, I get an error. I imagine that Lean has coerced something in the wrong type, but I have been unable to figure out what...

Can someone help me, please?

Thank you!

import tactic
import data.polynomial.degree.basic

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p+q).support ⊆ p.support ∪ q.support :=
begin
  exact finsupp.support_add,
end

Error (with finsupp underlined in red in the code):

invalid type ascription, term has type
  (?m_4 + ?m_5).support ⊆ ?m_4.support ∪ ?m_5.support
but is expected to have type
  (p + q).support ⊆ p.support ∪ q.support
state:
R : Type u_1,
_inst_1 : field R,
p q : polynomial R
⊢ (p + q).support ⊆ p.support ∪ q.support

[Kevin Buzzard]

convert finsupp.support_add, does it

[Damiano Testa]

@Kevin Buzzard Thank you so much!! I wasted so much time trying to figure out what types Lean was inferring!!

[Damiano Testa]

What is convert?

[Damiano Testa]

#check convert says unknown identifier...

[Kevin Buzzard]

exact @finsupp.support_add _ _ _ p q, gives the following error:

invalid type ascription, term has type
  (p + q).support ⊆
    @finsupp.support ℕ R
        (@add_monoid.to_has_zero R
           (@add_group.to_add_monoid R
              (@add_comm_group.to_add_group R
                 (@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
        p ∪
      @finsupp.support ℕ R
        (@add_monoid.to_has_zero R
           (@add_group.to_add_monoid R
              (@add_comm_group.to_add_group R
                 (@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
        q
but is expected to have type
  @finsupp.support ℕ R
      (@mul_zero_class.to_has_zero R
         (@monoid_with_zero.to_mul_zero_class R
            (@semiring.to_monoid_with_zero R
               (@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
      (p + q) ⊆
    @finsupp.support ℕ R
        (@mul_zero_class.to_has_zero R
           (@monoid_with_zero.to_mul_zero_class R
              (@semiring.to_monoid_with_zero R
                 (@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
        p ∪
      @finsupp.support ℕ R
        (@mul_zero_class.to_has_zero R
           (@monoid_with_zero.to_mul_zero_class R
              (@semiring.to_monoid_with_zero R
                 (@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
        q

and we can see if we can debug this.

[Kevin Buzzard]

convert is a tactic, so #check doesn't work. You can hover over it to see the docstring.

[Bryan Gin-ge Chen]

See also tactic#convert

[Damiano Testa]

They do look different, but I do not know why...

[Kevin Buzzard]

Me neither -- this is what type class inference is doing under the hood.

[Damiano Testa]

Ok, anyway, I am glad that I learned how to see what Lean is doing and I will now learn convert!

[Kevin Buzzard]

def X := @finsupp.support ℕ R
        (@add_monoid.to_has_zero R
           (@add_group.to_add_monoid R
              (@add_comm_group.to_add_group R
                 (@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))

def Y := @finsupp.support ℕ R
        (@mul_zero_class.to_has_zero R
           (@monoid_with_zero.to_mul_zero_class R
              (@semiring.to_monoid_with_zero R
                 (@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))

example : @X = @Y := rfl

So those outputs were more similar than we thought.

[Damiano Testa]

I interpret this as Lean having found 2 separate ways of loosing information to obtain a semi-quasi-almost-monoid and then being confused about why they are the same... is this more or less correct?

[Kevin Buzzard]

Well, exact is failing so there are some things which really are not equal by definition. We have to dig deeper:

import tactic
import data.polynomial.degree.basic

variables {R : Type*} [field R] {p q : polynomial R}

set_option pp.all true -- NEW

lemma supps  : (p+q).support ⊆ p.support ∪ q.support :=
begin
  exact @finsupp.support_add _ _ _ p q,
end

[Damiano Testa]

Btw, also assuming semiring things do not work with exact: that might have less overhead of conversion...

[Damiano Testa]

(I'm feeding my cats, so I can only type with my phone for a couple minutes!)

[Kevin Buzzard]

import tactic
import data.polynomial.degree.basic

variables {R : Type*} [semiring R] {p q : polynomial R}

set_option pp.all true

lemma supps  : (p+q).support ⊆ p.support ∪ q.support :=
begin
  exact @finsupp.support_add _ _ _ p q,
end


def X :=  @has_subset.subset.{0} (finset.{0} nat) (@finset.has_subset.{0} nat)
    (@finsupp.support.{0 u_1} nat R
       (@add_monoid.to_has_zero.{u_1} R
          (@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
       (@has_add.add.{u_1}
          (@finsupp.{0 u_1} nat R
             (@add_monoid.to_has_zero.{u_1} R
                (@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1))))
          (@finsupp.has_add.{0 u_1} nat R
             (@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
          p
          q))
    (@has_union.union.{0} (finset.{0} nat)
       (@finset.has_union.{0} nat (λ (a b : nat), classical.prop_decidable (@eq.{1} nat a b)))
       (@finsupp.support.{0 u_1} nat R
          (@add_monoid.to_has_zero.{u_1} R
             (@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
          p)
       (@finsupp.support.{0 u_1} nat R
          (@add_monoid.to_has_zero.{u_1} R
             (@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
          q))

def Y :=  @has_subset.subset.{0} (finset.{0} nat) (@finset.has_subset.{0} nat)
    (@finsupp.support.{0 u_1} nat R
       (@mul_zero_class.to_has_zero.{u_1} R
          (@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1)))
       (@has_add.add.{u_1} (@polynomial.{u_1} R _inst_1)
          (@distrib.to_has_add.{u_1} (@polynomial.{u_1} R _inst_1)
             (@semiring.to_distrib.{u_1} (@polynomial.{u_1} R _inst_1) (@polynomial.semiring.{u_1} R _inst_1)))
          p
          q))
    (@has_union.union.{0} (finset.{0} nat) (@finset.has_union.{0} nat (λ (a b : nat), nat.decidable_eq a b))
       (@finsupp.support.{0 u_1} nat R
          (@mul_zero_class.to_has_zero.{u_1} R
             (@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1)))
          p)
       (@finsupp.support.{0 u_1} nat R
          (@mul_zero_class.to_has_zero.{u_1} R
             (@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1)))
          q))

example : @X = @Y := rfl -- fails

[Kyle Miller]

In case it's helpful, I've expanded out convert as tactics:

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p + q).support ⊆ p.support ∪ q.support :=
begin
  have h := @finsupp.support_add _ _ _ p q,
  apply eq.mpr _ h,
  congr,
end

[Kyle Miller]

Now it's congr that's doing the heavy lifting, somehow.

[Kevin Buzzard]

example : @X R _inst_1 p q = @Y R _inst_1 p q :=
begin
  unfold X,
  unfold Y,
  -- refl, -- fails
  congr' -- works
end

Right, so you've got to the same stage as me but without the ugly staring at types. Nice!

[Kyle Miller]

I've gotten down to finset.has_union not equaling finset.has_union by refl:

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p + q).support ⊆ p.support ∪ q.support :=
begin
  have h := @finsupp.support_add _ _ _ p q,
  apply eq.mpr _ h,
  congr_core',
  -- finset ℕ = finset ℕ
  refl,
  -- finset.has_subset = finset.has_subset
  refl,
  -- (p + q).support = (p + q).support
  refl,
  -- p.support ∪ q.support = p.support ∪ q.support
  -- refl doesn't work!
  congr_core',
  -- finset ℕ = finset ℕ
  refl,
  swap,
  -- p.support = p.support
  refl,
  swap,
  -- q.support = q.support
  refl,
  -- finset.has_union = finset.has_union
  -- refl doesn't work!

end

[Kevin Buzzard]

Here's another way:

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p + q).support ⊆ p.support ∪ q.support :=
begin
  have h := @finsupp.support_add _ _ _ p q,
  apply eq.mpr _ h,
  congr' 2,
  refl, -- fails
end

Note congr' 3 solves the goal.

[Kyle Miller]

It looks like it's the decidability proof for finset's union:

⊢ @eq.{1} (has_union.{0} (finset.{0} nat)) (@finset.has_union.{0} nat (λ (a b : nat), nat.decidable_eq a b))
    (@finset.has_union.{0} nat (λ (a b : nat), classical.prop_decidable (@eq.{1} nat a b)))

[Damiano Testa]

Can I say that finsets are evil? They always cause problems for me...

[Kenny Lau]

just put open_locale classical at the beginning

[Kenny Lau]

edit: still doesn't work

[Kevin Buzzard]

So @Damiano Testa the solution is that nat.decidable_eq a b is not equal by definition to classical.prop_decidable (@eq.{1} nat a b).

[Damiano Testa]

Ok, I am not sure that I understand, but at least I am getting a sense of what is happening...

[Kevin Buzzard]

variables (a b : ℕ)

example : nat.decidable_eq a b = classical.prop_decidable (@eq.{1} nat a b) := rfl -- fails

example : subsingleton (decidable (a = b)) := by apply_instance -- works

This is why exact fails but convert works.

[Damiano Testa]

@Kevin Buzzard are your two examples equivalent mathematically? I do not really understand what they say...

[Kevin Buzzard]

It turns out that the two terms were not exactly the same. Lean's type class inference system fills in a lot of missing information for you -- that's its job. When you have (a b : nat) and write a + b this literally means has_add.add a b. Lean now has to figure out exactly the addition you mean, and it asks the type class inference system for an addition on the naturals, and the type class inference system returns one.

When you were trying to use the finsupp lemma to prove a result about polynomials, Lean twice had to ask the type class inference system for a proof that it is possible to decide whether two naturals are equal -- first when you stated the theorem, and secondly when you used the term that you hoped would prove it. However it got two different answers.

[Damiano Testa]

Ok, this is clearer, thanks!

[Kevin Buzzard]

By the way, the reason it's asking for this is that for finitely supported functions, the way they are implemented, the support is part of the data, and for Lean to figure out exactly which naturals are in the support it needs an algorithm to work out if two naturals are equal. It found two algorithms.

[Damiano Testa]

I had thought that the issue was with identifying the supports of the sum and the individual supports as being sets in the same ambient space... If I understand correctly, the issue was at a deeper level

[Kevin Buzzard]

The first one is nat.decidable_eq:

instance : decidable_eq ℕ
| zero     zero     := is_true rfl
| (succ x) zero     := is_false (λ h, nat.no_confusion h)
| zero     (succ y) := is_false (λ h, nat.no_confusion h)
| (succ x) (succ y) :=
    match decidable_eq x y with
    | is_true xeqy := is_true (xeqy ▸ eq.refl (succ x))
    | is_false xney := is_false (λ h, nat.no_confusion h (λ xeqy, absurd xeqy xney))
    end

This is the algorithm which uses induction: zero = zero, and succ m = succ n iff m = n.

[Kevin Buzzard]

But classical.prop_decidable just says "oh come on, x=y is a true-false statement, and mathematicians believe in the law of the excluded middle, which means that an algorithm exists for figuring out whether this is true or false, and let's use that algorithm."

[Kevin Buzzard]

These are definitely two different algorithms, not least because one of them isn't really an algorithm, it's just switching on a switch which says "forget the algorithm stuff, we are mathematicians and do not care about decidable equality"

[Kevin Buzzard]

However, Lean also knows that both these algorithms are correct, and hence must produce the same answer. Hence the algorithms must be equal, if we define equal algorithms in a highly mathematical way as "must produce the same answer".

[Damiano Testa]

This is making more sense. This is now off a tangent and is completely irrelevant for the purpose of my original question: why did Lean once use nat.decidable and once classical.prop_decidable?

[Kevin Buzzard]

For example, there is only one "sort" function, which takes a finite list of natural numbers and returns the same list but sorted. Two functions are equal if and only if they output the same output given the same input, right?

[Kevin Buzzard]

But computer scientists would argue that there were many sorting algorithms, because they care about the implementation and not just the output.

[Damiano Testa]

Kevin Buzzard said:

For example, there is only one "sort" function, which takes a finite list of natural numbers and returns the same list but sorted. Two functions are equal if and only if they output the same output given the same input, right?

It is similar to using or not using the bound given by GRH to compute class groups...

[Kevin Buzzard]

convert is clever. It looks for subsingleton instances, and if it finds them then it uses them. So convert can find a proof that a = b if it knows that a : T and b : T and subsingleton T.

[Kevin Buzzard]

well the problem with the GRH algorithm is that we haven't yet proved that it works :-)

[Kevin Buzzard]

The reason Lean found both is because they are both in the system, and Lean used different methods to look for them and found them both.

[Damiano Testa]

Kevin Buzzard said:

well the problem with the GRH algorithm is that we haven't yet proved that it works :-)

Right, but should GRH be true, the two algorithms are the same!

Anyway, I understand the difference, thanks!

[Damiano Testa]

This has been very informative: thanks!

[Kevin Buzzard]

One could fiddle with instance priorities to try and make this not happen, but this is beyond my pay grade. I have no idea why Lean finds them both.

[Damiano Testa]

Kevin Buzzard said:

One could fiddle with instance priorities to try and make this not happen, but this is beyond my pay grade. I have no idea why Lean finds them both.

Sure and, for me, already just knowing that I could use convert was a pretty good answer!

[Kevin Buzzard]

convert is a great tactic when something which should work, doesn't. It's also a cool way of reasoning -- I use it a lot. You kind of know what the last line of the proof is, approximately, early on, and convert lets you apply it it immediately.

[Damiano Testa]

I'll try it often, then!

[Adam Topaz]

I also think convert is great, but one thing to keep in mind: sometimes it spits out incomprehensible nonsense. When this has happened to me, it was always my fault, and just meant that I needed to do a bit more work before using it.

[Kevin Buzzard]

@Damiano Testa I looked into this a bit more. The file data.finsupp.basic in mathlib has the following warning at the beginning:

A general piece of advice is to not use `α →₀ β` directly, as the type class setup might not be a
good fit. Defining a copy and selecting the instances that are best suited for the application works
better.

## Implementation notes

This file is a `noncomputable theory` and uses classical logic throughout.

## Notation

This file defines `α →₀ β` as notation for `finsupp α β`.

So what's happening is that when you use finsupp.support_add it uses classical logic to deal with the decidable equality issues, but when you use polynomial it uses constructive logic.

I can't find polynomial.support_add in mathlib -- you should make a PR adding it, and proving it using convert.

[Damiano Testa]

Kevin Buzzard said:

I can't find polynomial.support_add in mathlib -- you should make a PR adding it, and proving it using convert.

I will try it!

[Johan Commelin]

Kevin Buzzard said:

So what's happening is that when you use finsupp.support_add it uses classical logic to deal with the decidable equality issues, but when you use polynomial it uses constructive logic.

Whut? polynomial is quite classical I would think.

[Johan Commelin]

@Damiano Testa There are lemmas called support_add. But maybe about multivariate polynomials.

[Johan Commelin]

They might serve as inspiration.

[Kevin Buzzard]

@Johan Commelin

import tactic
import data.polynomial.degree.basic

set_option pp.all true

lemma supps {R : Type*} [semiring R] {p q : polynomial R} :
  (p+q).support ⊆ p.support ∪ q.support :=
begin
  have h := @finsupp.support_add _ _ _ p q,
  -- h uses classical.prop_decidable
  -- polynomials (the goal) use nat.decidable
  sorry
end

[Johan Commelin]

Ouch, I see.

[Chris Wong]

convert is clever. It looks for subsingleton instances, and if it finds them then it uses them. So convert can find a proof that a = b if it knows that a : T and b : T and subsingleton T.

Should this be mentioned in the docs somewhere? That's the first time I've heard that.

[Scott Morrison]

Yes, it should be! Interested in making a documentation-only PR, that adds a sentence to the doc-string for convert?

[Mario Carneiro]

It's actually a feature of congr, which is inherited by congr' and convert

[Chris Wong]

https://github.com/leanprover-community/mathlib/pull/4060 :smile:

[Kevin Buzzard]

Thanks!

[Damiano Testa]

I am glad that @Chris Wong took care of this, since, even after looking at the suggestion, I am still unsure about what all this means!

Thanks!

[Kevin Buzzard]

@Damiano Testa The job of tactics like convert and congr is to try and prove that two terms are equal.

[Kevin Buzzard]

This is also the job of exact

[Kevin Buzzard]

exact is quick because it works with definitional equality which is exactly what lean is good at

[Kevin Buzzard]

But convert is more powerful because it has a second trick up its sleeve

[Kevin Buzzard]

If it has a : X and b : X and it can't prove that they are definitionally equal, it asks the type class inference system if perchance it knows a proof that X is a subsingleton

[Kevin Buzzard]

It's a brilliant idea

[Kevin Buzzard]

Subsingleton is a class so the type class system is very happy to manage this job

[Damiano Testa]

What is a subsingleton? I am reading #print subsingleton, but I cannot say that I understand the output.

@[class]
inductive subsingleton : Sort u → Prop
constructors:
subsingleton.intro : ∀ {α : Sort u}, (∀ (a b : α), a = b) → subsingleton α

[Kevin Buzzard]

Which means that occasionally convert gets lucky, finds an instance of subsingleton X, unwraps it to get a proof of "for all a and b : X, a=b" (the definition of subsingleton) and then applies this and moves on

[Kevin Buzzard]

Just #check subsingleton and jump to definition

[Kevin Buzzard]

Or read the docs

[Kevin Buzzard]

Use #print just to get technical information such as whether a certain lemma is tagged with [simp]. You almost always don't want #print.

[Damiano Testa]

Ok, so subsingleton is a singleton where you do not assume that it has one element, right? it is a type with at most one term, correct?

[Kevin Buzzard]

Right

[Damiano Testa]

Ok, indeed looking at the definition was much easier to understand than print!

[Kevin Buzzard]

So lean knows that a bunch of things are subsingletons

[Damiano Testa]

(I did not realize that #print and jumping to the definition were different)

[Kevin Buzzard]

Like presumably fin 0 and fin 1 (do you know how to check?)

[Kevin Buzzard]

#print gives you a description which doesn't use any variables and which doesn't display the docstring

[Damiano Testa]

#check (fin 0) : subsingleton did not work...

[Kevin Buzzard]

That's not the type of fin 0

[Kevin Buzzard]

fin 0 has type Type because it's what I'd call a set

[Kevin Buzzard]

So I asked "can you see if the type class system knows that fin 0 is a subsingleton"

[Damiano Testa]

Ok, so I do not know how to check whether fin 0 is a subsingleton

[Kevin Buzzard]

And the thing we have to do is to turn this into a question of the form "make a term of a type"

[Kevin Buzzard]

So the first question is "what is the type"

[Kevin Buzzard]

And the second question is what to use to make the term

[Kevin Buzzard]

You can try #check @subsingleton

[Kevin Buzzard]

That's the sort of output I'd find useful for making the type

[Kevin Buzzard]

Also look at the docstring for subsingleton

[Damiano Testa]

Lean says: subsingleton : Sort u_1 → Prop, so I understand that subsingleton takes a term of type u_1 and produces a proposition, likely saying whether or not what I feed to subsingleton is a subsingleton!

[Kevin Buzzard]

So what is the type that we want to construct a term of?

[Kevin Buzzard]

The translation into Lean of the statement of the theorem that fin 0 is a subsingleton?

[Damiano Testa]

we would like subsingleton (fin 0) is the type whose terms will be proofs of what we want, right?

[Kevin Buzzard]

Right

[Damiano Testa]

(and all those proofs will be the same!)

[Kevin Buzzard]

You can #check what you just posted

[Damiano Testa]

I get
subsingleton (fin 0) : Prop, which I confirms that this is a proposition!

[Kevin Buzzard]

And observe that it has type Prop which means it's a theorem statement

[Damiano Testa]

ok, good!

[Kevin Buzzard]

So now the question is how to prove it

[Damiano Testa]

so now I would like to know that there are terms in this type

[Kevin Buzzard]

You can put example : subsingleton $ fin 0 := begin

[Kevin Buzzard]

Does the $ work there instead of the bracket? I'm on mobile

[Damiano Testa]

library_search says

lemma ss : subsingleton (fin 0) :=
begin
  exact subsingleton_fin_zero,
end

[Kevin Buzzard]

Oh you cheated!

[Kevin Buzzard]

That's not the answer to the question

[Kevin Buzzard]

You just proved the theorem yourself

[Kevin Buzzard]

You don't want convert saying "ok they're equal as long as you can prove that the following things are subsingletons"

[Damiano Testa]

Kevin Buzzard said:

You can put example : subsingleton $ fin 0 := begin

This compiles, I added end after and Lean interprets it as looking for a term of the correct type

[Kevin Buzzard]

We need to use a tactic which doesn't involve knowing the name of the term beforehand

[Kevin Buzzard]

And that tactic is called apply_instance

[Kevin Buzzard]

And I don't know if it will solve the goal -- let me know!

[Damiano Testa]

example : subsingleton $ fin 0 := begin
 apply_instance,
end

solves the goal indeed!

[Kevin Buzzard]

Great. So here's how that magic worked

[Kevin Buzzard]

Because lean does not do magic

[Kevin Buzzard]

You found the name of the term already

[Kevin Buzzard]

Maybe you used library_search (which might be very slow)

[Damiano Testa]

Kevin Buzzard said:

Maybe you used library_search (which might be very slow)

Yes, I do not like using it

[Kevin Buzzard]

But now let's #print subsingleton_fin_zero

[Kevin Buzzard]

To see what's going on under the hood. Can you post the output? I'm on mobile

[Damiano Testa]

@[instance]
protected def subsingleton_fin_zero : subsingleton (fin 0) :=
fin_zero_equiv.subsingleton

[Kevin Buzzard]

So that definition is tagged with instance

[Kevin Buzzard]

And all the type class inference system does is that it's a fast program written in C or C++ or something which looks through everything tagged with instance and sees if anything helps

[Kevin Buzzard]

That's why the tactic is called apply_instance.

[Damiano Testa]

Ah, so apply_instance is similar to library_search, except that it only searches for statements tagged instance?

[Kevin Buzzard]

All of those @[derive decibable_equality, ext, simp]` things you see lying around in mathlib are just literally doing nothing more than tagging words onto the names of theorems and definitions

[Kevin Buzzard]

And then other things like tactics can use the tags

[Kevin Buzzard]

Right, apply_instance is similar but it's only looking at instances. But there's also another thing

[Kevin Buzzard]

This tactic is running behind the scenes all of the time because the elaborator is calling it every time you write 2+2

[Kevin Buzzard]

The elaborator sees this and says to the type class inference system "do you happen to know an addition on the naturals"

[Kevin Buzzard]

(or integers or reals or p-adics)

[Damiano Testa]

This probably explains why sometimes, when I type 1 : something, Lean then asks me for a has_one instance, right?

[Kevin Buzzard]

And the type class inference system says "sure, they're a semiring, let me just look up the addition for you"

[Kevin Buzzard]

Because there are functions defined in lean saying things like "if you are a semiring then you have an addition" and a carefully chosen collection are tagged with instance

[Kevin Buzzard]

Choosing the right ones to tag is a complicated research topic

[Damiano Testa]

Ok

[Kevin Buzzard]

In Lean 4 the algorithm will be replaced by a completely different one so we will have to learn how to use it from scratch

[Damiano Testa]

so, all terms in Prop are subsingletons, right? (this is just to make sure that I understand the definitions)

[Kevin Buzzard]

But if you just want to do mathematics then we basically have worked out what works best in lean 3

[Kevin Buzzard]

Right

[Damiano Testa]

Ok

[Kevin Buzzard]

So that means lean will be able to make a term of type subsingleton P if P : Prop`

[Johan Commelin]

But some things are subsingleton even though they don't have type Prop. Like prime_spectrum K.

[Damiano Testa]

yes, ok, I only meant it as an example, not an exhaustive one!

[Kevin Buzzard]

Or fin 0, which has type Type

[Kevin Buzzard]

It's all the propositions and all the sets with at most one element

[Damiano Testa]

for instance, I guess that you could formulate the valuative criterion of separatedness using subsingletons

[Kevin Buzzard]

You can model a false proposition as a set with no elements and a true one as a set with one element

[Kevin Buzzard]

What do you mean about the valuative criterion?

[Kevin Buzzard]

Oh you mean subsingleton schemes

[Damiano Testa]

yes

[Kevin Buzzard]

Do you need Noetherian hypotheses here?

[Kevin Buzzard]

I can't remember the non noeth story

[Kevin Buzzard]

I think Hartshorne does it

[Damiano Testa]

in the proof, you reduce to something being noetherian, but the statement may not require it

[Kevin Buzzard]

Is the statement about valuation rings?

[Kevin Buzzard]

Wait they have two points

[Damiano Testa]

yes, so i think that you can formulate the valuative criterion without noetherian hypotheses, but then they crop up somewhere...

[Kevin Buzzard]

General valuation rings can have more than two primes. Subsingleton is less than two

[Damiano Testa]

Ok, I had in mind the statement of the valuative criterion for "reasonable" schemes: I think that if X is of finite type, then you only need to check dvrs in the valuative criteria

[Kevin Buzzard]

Yes and this doesn't change the fact that fin 2 is not a subsingleton :-)

[Kevin Buzzard]

The criterion uses doubletons

[Damiano Testa]

Ok, I see what you are saying! I was thinking that once you fix the generic morphism, then there is at most one way of filling it in...

[Damiano Testa]

so, one of the elements of the doubleton is fixed and the other one is... a subsingleton! Ahahaha

[Damiano Testa]

(at least, this is how i view the valuative criteria: you are given the generic map and all you want to do is know if

1. you can extend it;
2. if so, can you extend it uniquely.
   )

[Johan Commelin]

@Damiano Testa Yup, that makes sense

[Kevin Buzzard]

Oh I see! Yes you should have formalised what you meant. Yes, separated is at most one, there's some adjective which is at least one and then proper is singleton

[Damiano Testa]

Great! I realize that explaining subsingleton via the valuative criteria is maybe not the most direct route...

[Kevin Buzzard]

There's a way of formalising the definition of compact to mean some statement involving filters has at least one answer, and a way of formalising Hausdorff so that it says the same statement has at most one answer

[Kevin Buzzard]

Basically certain filters have at least one limit in a compact space and at most one limit in a Hausdorff space

[Kevin Buzzard]

That's why compact Hausdorff is such a powerful criterion

[Damiano Testa]

I think that what you described is very close to my intuition for proper