axioms

Stream: condensed mathematics

[Johan Commelin]

We have

theorem liquid_tensor_experiment (S : Profinite.{0}) (V : pBanach.{0} p) :
  ∀ i > 0, Ext i (ℳ_{p'} S) V ≅ 0 :=

and

#print axioms liquid_tensor_experiment
-- propext
-- quot.sound
-- classical.choice

[Johan Commelin]

Confirms that we didn't add new axioms, and that there really is no sorry left.

[Peter Scholze]

So what are those funky axioms propext and quot.sound? (classical.choice I can guess)

[Patrick Massot]

docs#propext and docs#quot.sound are links to these axioms.

[Kevin Buzzard]

Propositional extensionality (Fermat's Last Theorem equals 2+2=4) (because they're both true)

[Patrick Massot]

These are completely irrelevant to mathematics.

[Kevin Buzzard]

and quotients satisfy the universal property of quotients.

[Patrick Massot]

They are only relevant for people interested only in constructive mathematics.

[Kevin Buzzard]

Propositional extensionality is used to prove the law of the excluded middle I think?

[Anatole Dedecker]

Doesn’t it use choice ?

[Anatole Dedecker]

Oh but maybe propext too

[Patrick Massot]

In Lean the proof of excluded middle uses all those three axioms

[Patrick Massot]

I mean the same three axioms as LTE.

[Peter Scholze]

OK, so I guess it's not surprising they are used in LTE ;-)

[Junyan Xu]

Patrick Massot said:

In Lean the proof of excluded middle uses all those three axioms

quot.sound is actually not needed for docs#classical.em, but no one has PR'd this (into core Lean) yet.