Variables forgetting their type?

Stream: new members

[Klaus Gy]

import Mathlib.CategoryTheory.Subobject.Basic

universe u v

open CategoryTheory Category Limits Subobject

variable {C : Type u} [Category.{v} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)

noncomputable section

def foo : Subobject Z ⟶ Subobject Y := (Subobject.pullback g).obj
def bar : Subobject Y ⟶ Subobject X := (Subobject.pullback f).obj
def baz : Subobject X ⟶ Subobject Z := foo ≫ bar

end

Here I get the error

Application type mismatch: In the application
  ?m.3247 ≫ bar
the argument
  bar
has type
  (?m.3253 ⟶ ?m.3254) → (Subobject ?m.3254 ⟶ Subobject ?m.3253) : Type (max ?u.3248 ?u.3249)
but is expected to have type
  ?m.2045 ⟶ Subobject Z : Type (max u v)Lean 4

but why does the typechecker 'forgets' the type of bar? When I hover over bar, I see

bar.{u, v} {C : Type u} [Category.{v, u} C] [HasPullbacks C] {X Y : C} (f : X ⟶ Y) : Subobject Y ⟶ Subobject X

as expected, why does this change to

  (?m.3253 ⟶ ?m.3254) → (Subobject ?m.3254 ⟶ Subobject ?m.3253) : Type (max ?u.3248 ?u.3249)?

I noticed that it is generally very hard to coerce functions types (→) to morphism types (⟶).

[Kyle Miller]

It's following the usual rules to fill in the implicit arguments with metavariables.

If you want to refer to the constant bar itself without filling in implicit arguments, you can do @bar. That's probably not correct here, but that's how.

[Klaus Gy]

I see, thanks!

[Kyle Miller]

The variable command doesn't create variables that retain the same meaning from definition to definition. Each definition starts from scratch. The variables aren't parameters that are fixed across definitions.

[Kyle Miller]

This means that, for example, foo and bar are equal

[Kyle Miller]

example : @foo = @bar := rfl

[Kyle Miller]

You could do this:

def bar {X Y : C} (f : X ⟶ Y) : Subobject Y ⟶ Subobject X := (Subobject.pullback f).obj

def baz : Subobject Z ⟶ Subobject X := bar g ≫ bar f

[Klaus Gy]

yea sorry, i tried to simplify my example but then i made a mistake. originally i had something like this

theorem pullback_comp' :
    (Subobject.pullback (f ≫ g)).obj = (Subobject.pullback g).obj ≫ (Subobject.pullback f).obj := sorry

which doesn't typecheck and also this doesn't typecheck:

theorem pullback_comp' :
    ((Subobject.pullback (f ≫ g)).obj : Subobject Z ⟶ Subobject X) =
    ((Subobject.pullback g).obj : Subobject Z ⟶ Subobject Y) ≫
    ((Subobject.pullback f).obj : Subobject Y ⟶ Subobject X) := sorry

but then this does work:

theorem pullback_comp' :
    (Subobject.pullback (f ≫ g)).obj =
    ((Subobject.pullback g).obj ≫ (Subobject.pullback f).obj :
    Subobject Z ⟶ Subobject X) := sorry

I still don't fully understand why the second version doesn't work but at least i have a working version now.

[Klaus Gy]

interestingly this works fine as well:

def test : Nat :=
  let foo : Subobject Z ⟶ Subobject Y := (Subobject.pullback g).obj
  let bar : Subobject Y ⟶ Subobject X := (Subobject.pullback f).obj
  let baz := foo ≫ bar
  1

i sometimes feel that let NAME : TYPE := TERM does actual coercion while (TERM : TYPE) is treated differently, but i dont understand the difference...

[Kyle Miller]

It looks like the issue is that obj doesn't give a morphism, but a function.

Adding in a type hint makes it go through:

theorem pullback_comp' :
    (show Subobject Z ⟶ Subobject X from (Subobject.pullback (f ≫ g)).obj) =
    ((Subobject.pullback g).obj : Subobject Z ⟶ Subobject Y) ≫
    ((Subobject.pullback f).obj : Subobject Y ⟶ Subobject X) := sorry

(That's not recommended, but it works to illustrate the problem.)

This suggests you need a function that gives a Subobject morphism.

The deal with (t : Ty) is that it makes sure the type of t is Ty, inserting a coercion if it needs to. The coercion part is a secondary feature, and it's not being invoked here. The type of (Subojbect.pullback _).obj unifies with the morphism type, so nothing needs to be done. (Note that the type ascriptions on the RHS can be removed.)

[Kyle Miller]

This works too:

theorem pullback_comp' :
    (Subobject.pullback (f ≫ g)).obj =
    ((Subobject.pullback g).obj ≫ (Subobject.pullback f).obj : Subobject Z ⟶ Subobject X) := sorry

The type ascription tells >> enough information to know what category it's for.

[Kyle Miller]

Klaus Gy said:

interestingly this works fine as well:

That's not surprising, since all the lets share the same local context. Let definitions are fundamentally different from global constants. (Though maybe what's interesting is that creating these variables solves the elaboration issue, rather than being related to your original question about 'forgetting' types.)

Your feeling about "actual coercion" is that when you define a local let definition, then that locks in what you want the type of the variable to be, definitionally. The type of (Subobject.pullback g).obj is definitionally equal to the morphism type, but it's inferred type is just a plain function type.

[Klaus Gy]

The deal with (t : Ty) is that it makes sure the type of t is Ty, inserting a coercion if it needs to. The coercion part is a secondary feature, and it's not being invoked here. The type of (Subojbect.pullback _).obj unifies with the morphism type, so nothing needs to be done. (Note that the type ascriptions on the RHS can be removed.)

Thanks a lot! I'm slowly starting to understand :)

[Klaus Gy]

yea i noticed that also sometimes inside a proof if supplying (t : Ty) is not working out, it helps to introduce a temp variable of type Ty and immediately returning it

[Robin Arnez]

Yeah that's basically what show X from Y is doing (literally expands to have : X := Y; this). That way the type X is part of the term

[Klaus Gy]

thank you, thats a good trick!