problem caused by `by`

Stream: general

[Suzuka Yu]

Greetings! I encountered a strange anomaly that might have something to do with by, here is a mwe:

mwe

import Mathlib

open Finsupp Representation Rep CategoryTheory NatTrans
  ConcreteCategory Limits groupCohomology

noncomputable section

variable (R G : Type) [CommRing R] [Group G]

namespace Representation

variable (V W : Type) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
variable {R G V} (ρ : Representation R G V)
variable {W X : Type} [AddCommGroup W] [Module R W] [AddCommGroup X] [Module R X]

@[simps] def ind₁' : Representation R G (G →₀ V) where
  toFun g := lmapDomain _ _ (fun x ↦ x * g⁻¹) ∘ₗ mapRange.linearMap (ρ g)
  map_one' := by ext; simp
  map_mul' _ _ := by ext; simp [mul_assoc]

private abbrev ind₁'_map (f : V →ₗ[R] W) : (G →₀ V) →ₗ[R] (G →₀ W) := mapRange.linearMap f

@[simps] def ind₁'_π : (G →₀ V) →ₗ[R] V where
  toFun f := f.sum (fun _ ↦ (1 : V →ₗ[R] V))
  map_add' _ _ :=  sum_add_index' (congrFun rfl) fun _ _ ↦ congrFun rfl
  map_smul' _ _ := by simp

lemma ind₁'_π_comm (g : G) : ind₁'_π ∘ₗ ind₁' ρ g = ρ g ∘ₗ ind₁'_π := by
  ext; simp

end Representation

namespace Rep

variable {R G} (M : Rep R G) (A : ModuleCat R)

def ind₁' : Rep R G ⥤ Rep R G where
  obj M := of M.ρ.ind₁'
  map f := {
    hom := ofHom (Representation.ind₁'_map (ModuleCat.Hom.hom f.hom))
    comm g := sorry
  }
  map_id _ := by
    ext : 2
    exact mapRange.linearMap_id
  map_comp _ _ := by
    ext : 2
    exact mapRange.linearMap_comp _ _

/--
The natural projection `ind₁'.obj M ⟶ M`, which takes `f : G →₀ M.V` to the sum of the
values of `f`.
-/

def aux (M : Rep R G) : ind₁'.obj M ⟶ (𝟭 (Rep R G)).obj M := ofHom {
  val := Representation.ind₁'_π
  property g := by
    rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
    apply ind₁'_π_comm
}

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  app := Rep.aux
  naturality _ _ _ := by
    expose_names
    refine Action.hom_ext _ _ ?_
    ext z
    show Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁']
    rw [Finsupp.sum_mapRange_index]
    · exact (map_finsuppSum x_2.hom.hom z fun _ ↦ _).symm
    · exact fun _ ↦ rfl

end Rep
end

This file compiles flawlessly.

But I want to insert the definition of aux into ind₁'_π, namely, I wish to write:

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  app M := ofHom {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      apply ind₁'_π_comm
  }
  naturality _ _ _ := by
    expose_names
    refine Action.hom_ext _ _ ?_
    ext z
    show Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁']
    rw [Finsupp.sum_mapRange_index]
    · exact (map_finsuppSum x_2.hom.hom z fun _ ↦ _).symm
    · exact fun _ ↦ rfl

This, however, won't work, and I don't understand why. Comment out the proof for naturality in ind₁'_π works:

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  app M := ofHom {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      apply ind₁'_π_comm
  }
  naturality _ _ _ := by
    sorry

If we place the cursor between the by and sorry in naturality, there will be a meta variable appears in the infoview: ind₁'.map x✝ ≫ ofHom ?m.116652 = ofHom ?m.116652 ≫ (𝟭 (Rep R G)).map x✝.

However if we change by sorry to just sorry, it works fine: ind₁'.map x✝ ≫ ofHom ⟨Representation.ind₁'_π, ⋯⟩ = ofHom ⟨Representation.ind₁'_π, ⋯⟩ ≫ (𝟭 (Rep R G)).map x✝.

I wonder whats happening here and how to accomplish the insertion?

[Kyle Miller]

Interesting. There's something about the elaboration order that leads to the failure. Having the separate definition guarantees the app field is elaborated first.

If you wrap the body of the app field with by exact, that perturbs the order enough that it goes through.

code

import Mathlib

open Finsupp Representation Rep CategoryTheory NatTrans
  ConcreteCategory Limits groupCohomology

noncomputable section

variable (R G : Type) [CommRing R] [Group G]

namespace Representation

variable (V W : Type) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
variable {R G V} (ρ : Representation R G V)
variable {W X : Type} [AddCommGroup W] [Module R W] [AddCommGroup X] [Module R X]

@[simps] def ind₁' : Representation R G (G →₀ V) where
  toFun g := lmapDomain _ _ (fun x ↦ x * g⁻¹) ∘ₗ mapRange.linearMap (ρ g)
  map_one' := by ext; simp
  map_mul' _ _ := by ext; simp [mul_assoc]

private abbrev ind₁'_map (f : V →ₗ[R] W) : (G →₀ V) →ₗ[R] (G →₀ W) := mapRange.linearMap f

@[simps] def ind₁'_π : (G →₀ V) →ₗ[R] V where
  toFun f := f.sum (fun _ ↦ (1 : V →ₗ[R] V))
  map_add' _ _ :=  sum_add_index' (congrFun rfl) fun _ _ ↦ congrFun rfl
  map_smul' _ _ := by simp

lemma ind₁'_π_comm (g : G) : ind₁'_π ∘ₗ ind₁' ρ g = ρ g ∘ₗ ind₁'_π := by
  ext; simp

end Representation

namespace Rep

variable {R G} (M : Rep R G) (A : ModuleCat R)

def ind₁' : Rep R G ⥤ Rep R G where
  obj M := of M.ρ.ind₁'
  map f := {
    hom := ofHom (Representation.ind₁'_map (ModuleCat.Hom.hom f.hom))
    comm g := sorry
  }
  map_id _ := by
    ext : 2
    exact mapRange.linearMap_id
  map_comp _ _ := by
    ext : 2
    exact mapRange.linearMap_comp _ _

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  -- Remove `by exact` and elaboration fails
  app M := by exact (ofHom {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      apply ind₁'_π_comm
  })
  naturality x x_1 x_2 := by
    refine Action.hom_ext _ _ ?_
    ext z
    change Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁']
    rw [Finsupp.sum_mapRange_index]
    · exact (map_finsuppSum x_2.hom.hom z fun _ ↦ _).symm
    · exact fun _ ↦ rfl

Do you think you could help minimize this? That means making an example that's mathlib-free and that removes unnecessary detail, but still exhibits the error. It doesn't need to be minimal. If you have a minimization, that would help get to the bottom of this. Possibly there's a Lean elaboration bug.

[Kyle Miller]

Here's another more robust workaround, which is to tell ofHom what category it's elaborating for:

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  app M := ofHom (C := Rep R G) {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      apply ind₁'_π_comm
  }
  naturality x x_1 x_2 := by
    refine Action.hom_ext _ _ ?_
    ext z
    change Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁']
    rw [Finsupp.sum_mapRange_index]
    · exact (map_finsuppSum x_2.hom.hom z fun _ ↦ _).symm
    · exact fun _ ↦ rfl

[Suzuka Yu]

Kyle Miller 发言道：

Here's another more robust workaround, which is to tell ofHom what category it's elaborating for:

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  app M := ofHom (C := Rep R G) {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      apply ind₁'_π_comm
  }
  naturality x x_1 x_2 := by
    refine Action.hom_ext _ _ ?_
    ext z
    change Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁']
    rw [Finsupp.sum_mapRange_index]
    · exact (map_finsuppSum x_2.hom.hom z fun _ ↦ _).symm
    · exact fun _ ↦ rfl

Great! Thanks for your help!

[Suzuka Yu]

Kyle Miller 发言道：

Interesting. There's something about the elaboration order that leads to the failure. Having the separate definition guarantees the app field is elaborated first.

If you wrap the body of the app field with by exact, that perturbs the order enough that it goes through.

code

import Mathlib

open Finsupp Representation Rep CategoryTheory NatTrans
  ConcreteCategory Limits groupCohomology

noncomputable section

variable (R G : Type) [CommRing R] [Group G]

namespace Representation

variable (V W : Type) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
variable {R G V} (ρ : Representation R G V)
variable {W X : Type} [AddCommGroup W] [Module R W] [AddCommGroup X] [Module R X]

@[simps] def ind₁' : Representation R G (G →₀ V) where
  toFun g := lmapDomain _ _ (fun x ↦ x * g⁻¹) ∘ₗ mapRange.linearMap (ρ g)
  map_one' := by ext; simp
  map_mul' _ _ := by ext; simp [mul_assoc]

private abbrev ind₁'_map (f : V →ₗ[R] W) : (G →₀ V) →ₗ[R] (G →₀ W) := mapRange.linearMap f

@[simps] def ind₁'_π : (G →₀ V) →ₗ[R] V where
  toFun f := f.sum (fun _ ↦ (1 : V →ₗ[R] V))
  map_add' _ _ :=  sum_add_index' (congrFun rfl) fun _ _ ↦ congrFun rfl
  map_smul' _ _ := by simp

lemma ind₁'_π_comm (g : G) : ind₁'_π ∘ₗ ind₁' ρ g = ρ g ∘ₗ ind₁'_π := by
  ext; simp

end Representation

namespace Rep

variable {R G} (M : Rep R G) (A : ModuleCat R)

def ind₁' : Rep R G ⥤ Rep R G where
  obj M := of M.ρ.ind₁'
  map f := {
    hom := ofHom (Representation.ind₁'_map (ModuleCat.Hom.hom f.hom))
    comm g := sorry
  }
  map_id _ := by
    ext : 2
    exact mapRange.linearMap_id
  map_comp _ _ := by
    ext : 2
    exact mapRange.linearMap_comp _ _

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  -- Remove `by exact` and elaboration fails
  app M := by exact (ofHom {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      apply ind₁'_π_comm
  })
  naturality x x_1 x_2 := by
    refine Action.hom_ext _ _ ?_
    ext z
    change Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁']
    rw [Finsupp.sum_mapRange_index]
    · exact (map_finsuppSum x_2.hom.hom z fun _ ↦ _).symm
    · exact fun _ ↦ rfl

Do you think you could help minimize this? That means making an example that's mathlib-free and that removes unnecessary detail, but still exhibits the error. It doesn't need to be minimal. If you have a minimization, that would help get to the bottom of this. Possibly there's a Lean elaboration bug.

Sure! This is a smaller and cleaner example that can still demonstrate the issue:

import Mathlib.Combinatorics.Quiver.ReflQuiver
import Mathlib.RepresentationTheory.Rep

open Finsupp CategoryTheory

noncomputable section

variable {R G : Type} [CommRing R] [Group G]

namespace Representation

variable {V : Type} [AddCommGroup V] [Module R V] (ρ : Representation R G V)

def ind₁' : Representation R G (G →₀ V) where
  toFun g := lmapDomain _ _ (fun x ↦ x * g⁻¹) ∘ₗ mapRange.linearMap (ρ g)
  map_one' := sorry
  map_mul' := sorry

@[simps] def ind₁'_π : (G →₀ V) →ₗ[R] V where
  toFun f := f.sum (fun _ ↦ (1 : V →ₗ[R] V))
  map_add' := sorry
  map_smul' := sorry

end Representation

namespace Rep

def ind₁' : Rep R G ⥤ Rep R G where
  obj M := of (Representation.ind₁' M.ρ)
  map f := ⟨ConcreteCategory.ofHom (mapRange.linearMap f.hom.hom), sorry⟩
  map_id _ := sorry
  map_comp _ _ := sorry

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  -- Remove `by exact` and elaboration fails
  app M := by exact (ConcreteCategory.ofHom {
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      sorry
  })
  naturality x x_1 x_2 := by
    ext z
    change Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁', sum_mapRange_index]
    exact (map_finsuppSum x_2.hom.hom z _).symm

elaboration seems like a rabbit hole for me :joy:, hope there are some useful information in the example

[Kyle Miller]

I think what's going on is that it's not able to figure out that the inner structure instance is a Subtype by the time it's first being elaborated, so it gets postponed. Then, the second by gets run before the first by, and because of the way the sorts of metavariables for postponement work, the second by doesn't even get any partial information about the app field.

Here's yet another workaround:

def ind₁'_π : ind₁' ⟶ 𝟭 (Rep R G) where
  app M := ConcreteCategory.ofHom ({
    val := Representation.ind₁'_π
    property g := by
      rw [←LinearMap.coe_comp, ←LinearMap.coe_comp, ←DFunLike.ext'_iff]
      sorry
  } : Subtype _)
  naturality x x_1 x_2 := by
    ext z
    change Representation.ind₁'_π ((ind₁'.map x_2).hom.hom z) =
      x_2.hom.hom ((Representation.ind₁'_π) z)
    simp [ind₁', sum_mapRange_index]
    exact (map_finsuppSum x_2.hom.hom z _).symm

If you change Subtype _ to just _ then you get the original error, so it's not the type ascription syntax itself that's changing anything.

[Kyle Miller]

Without having debugged very hard, it seems like the proximal issue is that none of the instance arguments to ofHom are being synthesized before the structure instance notation starts elaboration, so there's missing information, and so it decides that it's best to just postpone.

Possibly, when structure instance notation is about to postpone, it could try a pass of synthesizing pending problems first to see if it's necessary. That might fix this example, but who knows what then might break :fear: