mapNatTrans — Mathlib

English

Given a natural transformation k: F₁ ⟶ F₂, induce a natural transformation map₂Functor F x₁ ⟶ map₂Functor F x₂ for ThinSkeleton.

Русский

У данной натуральной трансформации k: F₁ ⟶ F₂ индуцируется естественная трансформация map₂Functor F x₁ ⟶ map₂Functor F x₂ в тонком скелете.

LaTeX

$$map₂NatTrans (F) : {x₁ x₂ : ThinSkeleton C} → (x₁ ⟶ x₂) → (map₂Functor F x₁ ⟶ map₂Functor F x₂)$$

Lean4

/-- Given a natural transformation `F₁ ⟶ F₂`, induce a natural transformation `map F₁ ⟶ map F₂`. -/
def mapNatTrans {F₁ F₂ : C ⥤ D} (k : F₁ ⟶ F₂) : map F₁ ⟶ map F₂ where
  app
    X :=
    Quotient.recOnSubsingleton X fun x =>
      ⟨⟨⟨k.app x⟩⟩⟩
        /- Porting note: `map₂ObjMap`, `map₂Functor`, and `map₂NatTrans` were all extracted
        from the original `map₂` proof. Lean needed an extensive amount explicit type
        annotations to figure things out. This also translated into repeated deterministic
        timeouts. The extracted defs allow for explicit motives for the multiple
        descents to the quotients.

        It would be better to prove that
        `ThinSkeleton (C × D) ≌ ThinSkeleton C × ThinSkeleton D`
        which is more immediate from comparing the preorders. Then one could get
        `map₂` by currying.
        -/

Похожие утверждения