Fixing ProofNet data set with valid Mathlib4

Stream: mathlib4

[Brando Miranda]

I think I found a invalid name in a ML data set for this statement:

import Mathlib
open Filter Set TopologicalSpace
open scoped Topology


theorem exercise_22_2b {X : Type*} [TopologicalSpace X]
  {A : Set X} (r : X → A) (hr : Continuous r) (h : ∀ x : A, r x = x) :
  QuotientMap r:= sorry

What is the recommended fix for the type? Thanks in advance!

My corrected dataset will live here: https://huggingface.co/datasets/UDACA/proofnet-v2-lean4/viewer/default/validation?row=46

[Aaron Liu]

Could this be docs#Topology.IsQuotientMap

[Kevin Buzzard]

In maths this is called a retraction https://en.m.wikipedia.org/wiki/Retraction_(topology) . A quotient map is something else.

[Patrick Massot]

Aaron is right, the statement is meant to be IsQuotientMap.

[Patrick Massot]

Kevin, this is indeed a retraction, but it’s true that a retraction is a quotient map.

[Patrick Massot]

Here is a proof:

import Mathlib.Topology.Order
open Filter Set Topology TopologicalSpace
open scoped Topology


theorem exercise_22_2b {X : Type*} [TopologicalSpace X]
    {A : Set X} (r : X → A) (hr : Continuous r) (h : ∀ x : A, r x = x) :
    IsQuotientMap r:= by
  refine ⟨Function.RightInverse.surjective h,  le_antisymm ?_ <| continuous_iff_coinduced_le.mp hr⟩
  let ι := ((↑) : A → X)
  have : coinduced r (coinduced ι (induced ι ‹_›)) ≤ coinduced r ‹_› :=
    coinduced_mono (coinduced_le_iff_le_induced.mpr fun _ a => a)
  rwa [coinduced_compose, show r ∘ ι = id by aesop ] at this

it may be that we don’t have this in Mathlib.

[Patrick Massot]

And we should really rename these coinduced and induced

[Patrick Massot]

for consistency with everything else. I agree that we say “induced topology” in the real world. But I’ve never heard anyone saying “coinduced topology”.

[Patrick Massot]

That fact that this “co” is reversed from our usual “map/comap” pair is really bad.

[Kevin Buzzard]

Anatole pointed out to me when I asked about this recently that the coinduced topology is just indiscrete(edit: discrete) away from the image so it only really makes sense to consider it for surjections where we can just call it the quotient topology

[Patrick Massot]

I still think it should be called map.

[Eric Wieser]

Brando Miranda said:

I think I found a invalid name in a ML data set for this statement:

This seems unlikely; rather, I think you used a different version of Lean to the one that the dataset was built with. Either the instructions for the dataset are at fault for not specifying the mathlib version, or you are at fault for not following said instructions!

[Aaron Liu]

Kevin Buzzard said:

Anatole pointed out to me when I asked about this recently that the coinduced topology is just indiscrete away from the image so it only really makes sense to consider it for surjections where we can just call it the quotient topology

Shouldn't that be discrete instead? All the points are apart, not together, since the function is not there to hold them together.

[Kevin Buzzard]

Yeah maybe, I didn't stop to think :-) Yeah, preimage of anything outside image is open because it's empty, so it's discrete.