status of `tactic/transfer.lean`

Stream: general

[Cyril Cohen]

Hi, is the general transfer tactic used in the codebase? Is there doc beyond the header of the tactic.lean file and a summary of its capabilities? Am I looking at the right file?

[Scott Morrison]

Not as far as I'm aware.

[Cyril Cohen]

Is there another transfer tactic that is in use in the code base?

[Alex J. Best]

I think it is used in data.nat.num.lemmas but that might be the only place iirc. there is also tactic#equiv_rw and tactic#transport which as I understand aim to do related things, but none of these tactics are used extensively in mathlib

[Eric Wieser]

One reason we almost never use transport is that results we could prove with it are usually true more generally when only an injection is available

[Kevin Buzzard]

or a surjection: for example "X isomorphic to compact Y is compact" follows from "continuous image of compact is compact", and "R isomorphic to S has at most one maximal ideal" follows from "R -> S a surjection and R has at most one maximal ideal implies S has at most one maximal ideal".

[Scott Morrison]

A brand new transport (not ready for PR yet) can now do things like:

def MyCompact (X : Type) [TopologicalSpace X] :=
  ∀ {ι : Type} {U : ι → Set X} (_ : ∀ i, IsOpen (U i)) (_ : Set.univ ⊆ ⋃ i, U i),
  ∃ t : Finset ι, Set.univ ⊆ ⋃ i ∈ t, U i

variable {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] in
example (f : X → Y) (hf : f.Surjective) (hf_cont : Continuous f) (hX : MyCompact X) : MyCompact Y := by
  transport hX along f

WIP with @Jake Levinson.

[Kevin Buzzard]

What?? This must be pulling the fact that preimage of open is open out of a hat somewhere. Your transport isn't just transporting along isomorphisms then? Because an isomorphism of topological spaces sends opens to opens by definition.

Here's my favourite of these injective/surjective questions. By transport below I mean this amazing extension of what I was thinking of, where you can transport along injections and surjections as well as isomorphisms.

Let's say a commutative ring is local if it has exactly one maximal ideal. I claim that a ring isomorphic to a local ring is local, and here's a funny proof. Say a ring is nontrivial if it has more than one element. If R -> S is an injection and R is nontrivial then S is nontrivial, by transport. Say a ring is prelocal if it has at most one maximal ideal. If R -> S is a surjection and R is prelocal then S is prelocal, by transport. Furthermore a nontrivial prelocal ring is local. Hence if R -> S is an isomorphism and R is local then S is local.

I am currently very confused about how you're transporting along non-isomorphisms so I'm wondering how far you're likely to be able to go and the above question is, I would imagine, quite a challenge.

[Anatole Dedecker]

Yes please tell us how it works!

[Scott Morrison]

Indeed, Kevin, you have correctly identified our cheating, but it is only as bad as

attribute [aesop safe apply] IsOpen.preimage

which I think is fairly justifiable even without this tactic wanting it.

[Scott Morrison]

Another fun example that currently works (again, requiring the same aesop rule for IsOpen.preimage, but no other cheating):

def MySeqCompact (X : Type) [TopologicalSpace X] :=
  ∀ (α : ℕ → X),
  ∃ (β : ℕ → ℕ) (x : X),
  ∀ (U : Set X) (_ : IsOpen U) (_ : x ∈ U),
  ∃ (N : ℕ),
  ∀ (n : ℕ) (_ : n ≥ N), α (β n) ∈ U

example (f : X → Y) (hf : f.Surjective) (hf_cont : Continuous f) (hX : MySeqCompact X) :  MySeqCompact Y := by
  transport hX along f

[Scott Morrison]

Jake and I were planning on working on this again tomorrow, and perhaps we will try local rings. :-)

[Jake Levinson]

To say a bit more about (the current state of) the tactic, it works through the goal syntactically - it checks if the goal is a forall / pi type, if it is an exists statement, and so on. For example if the goal is p and q and we’re given p’ and q’, the tactic will try to transport p’ to p and q’ to q and will fail if this is not the correct way to proceed. So the goal has to syntactically resemble the transport hypothesis.

The guesswork is limited, for instance to transport x : X to a goal Y it will try f x and see that it works. The default guess is to try aesop.

The tactic isn’t intended to be very intelligent, the main point is to break down the transport goal piece by piece and transport each (small) part separately. Compactness is a nice example because there are several nested quantifiers that can be handled automatically, but only one (as Kevin pointed out) nontrivial choice.

[Scott Morrison]

Jake's description leaves out one important part: we don't just transport by applying the bare function, but also by using solve_by_elim with lemmas tagged as functor to build new functions. Working out how to deal with ambiguity here (Filter.map via Filter.comap etc) is the big thing we haven't really decided how to deal with yet!