Theorems · Definition · algebraic topology

ContinuousMap.Homotopy.prodToProdTopI

{X : TopCat} →
  {a₁ a₂ : ↑(TopCat.of (ULift.{u, 0} ↑unitInterval))} →
    {b₁ b₂ : ↑X} →
      (FundamentalGroupoid.fromTop a₁ ⟶ FundamentalGroupoid.fromTop a₂) →
        (FundamentalGroupoid.fromTop b₁ ⟶ FundamentalGroupoid.fromTop b₂) →
          ((FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{u, 0} ↑unitInterval)) X).obj
              ({ as := a₁ }, { as := b₁ }) ⟶
            (FundamentalGroupoidFunctor.prodToProdTop (TopCat.of (ULift.{u, 0} ↑unitInterval)) X).obj
              ({ as := a₂ }, { as := b₂ }))

An abbreviation for prodToProdTop, with some types already in place to help the typechecker. In particular, the first path should be on the ulifted unit interval.

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Cited by

4 results in Mathlib

Foundations

Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound