equivalence of fibres over equal base points?

Stream: Is there code for X?

[Scott Morrison]

What is

def foo (α : J → Type _) {j j' : J} (h : j = j') : α j ≃ α j' where
  toFun a := congrArg α h ▸ a
  invFun a := congrArg α h.symm ▸ a
  left_inv a := by aesop
  right_inv a := by aesop

called?

[Scott Morrison]

(Presumably it is in the library somewhere!)

[Adam Topaz]

docs#Equiv.congr ?

[Arend Mellendijk]

Equiv.cast (congrArg α h)?
docs#Equiv.cast

[Scott Morrison]

Thanks! I might combine those suggestions and add

def Equiv.congr (α : J → Type _) {j j' : J} (h : j = j') : α j ≃ α j' :=
  Equiv.cast (congrArg α h)

[Eric Wieser]

That strikes me as not a great name, given how maybe other equivs have congr in their name, and the existence of docs#Equiv.equivCongr

[Anatole Dedecker]

Is docs#Equiv.cast really not enough here? It feels a bit overkill to add a special definition for this case

[Eric Wieser]

I think the argument goes that it's useful to be able to find h by unification

[Antoine Chambert-Loir]

Scott Morrison said:

What is

def foo (α : J → Type _) {j j' : J} (h : j = j') : α j ≃ α j' where
  toFun a := congrArg α h ▸ a
  invFun a := congrArg α h.symm ▸ a
  left_inv a := by aesop
  right_inv a := by aesop

called?

Can't resist writing it's called 'foo'.

[Johan Commelin]

I guess it could be called eqToEquiv, just like we have eqToIso, etc...

[Scott Morrison]

It is currently called Equiv.transport in #6379, where I use it in building the monoidal structure on graded objects. I was not able to find something that worked just using Equiv.cast, but if anyone would like to experiment, they're welcome to push commits. :-)

[Eric Wieser]

These sound somewhat similar to the problems I faced when putting the monoid structure on DirectSum; are the constructions analogous in some way?

[Scott Morrison]

What do you mean by "putting the monoid structure on DirectSum"?

[Eric Wieser]

I'm referring to these three lemmas and their use in docs#DirectSum.semiring

[Scott Morrison]

I don't think it is directly related. The thing Joël and I have done here is:

variable {V : Type u} [Category.{v} V] [Preadditive V] [MonoidalCategory V] [MonoidalPreadditive V]
  [HasFiniteBiproducts V] [HasZeroObject V]

/-- The tensor product of graded objects `X` and `Y` is, in each degree `i`,
the biproduct over `a + b = i` of `X a ⊗ Y b`. -/
def tensorObj (X Y : GradedObject ℕ V) (i : ℕ) : V :=
  biproduct (fun p : antidiagonal i => (X p.1.1) ⊗ (Y p.1.2))

/-- The tensor product of morphisms between graded objects is the diagonal map
consisting of tensor products of components. -/
def tensorHom {W X Y Z : GradedObject ℕ V} (f : W ⟶ X) (g : Y ⟶ Z) :
    tensorObj W Y ⟶ tensorObj X Z :=
  fun _ => biproduct.map fun p => f p.1.1 ⊗ g p.1.2

/-- The tensor unit in graded `V`-objects is the tensor unit in `V`, supported in grading 0. -/
def tensorUnit : GradedObject ℕ V
| 0 => 𝟙_ V
| _ + 1 => 0

-- Construction of unitors and associators, and many lemmas.

instance : MonoidalCategory (GradedObject ℕ V) where
  ...

[Scott Morrison]

If you set V = AddCommGroup, then Mon_ (GradedObject ℕ V) will be equivalent to ℕ-graded rings.

[Eric Wieser]

I assume you use antidiagonal i and not {p // p.1 + p.2 = i} because you need finiteness in some way?