Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit

Fundamental groupoid of punit #

The fundamental groupoid of punit is naturally isomorphic to CategoryTheory.Discrete PUnit

source
instance Path.instSubsingletonPUnitUnit :
Subsingleton (Path PUnit.unit PUnit.unit)
Equations
source
instance FundamentalGroupoid.instSubsingletonHomPUnit {x y : FundamentalGroupoid PUnit.{u_1 + 1} } :
Subsingleton (x ⟶ y)
Equations
  • ⋯ = ⋯
source
def FundamentalGroupoid.punitEquivDiscretePUnit :
FundamentalGroupoid PUnit.{u + 1} ≌ CategoryTheory.Discrete PUnit.{v + 1}

Equivalence of groupoids between fundamental groupoid of punit and punit

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_counitIso :
    FundamentalGroupoid.punitEquivDiscretePUnit.counitIso = CategoryTheory.Iso.refl (((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{v + 1} )).obj { as := PUnit.unit }).comp (CategoryTheory.Functor.star (FundamentalGroupoid PUnit.{u + 1} )))
    source
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_inverse :
    FundamentalGroupoid.punitEquivDiscretePUnit.inverse = (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{v + 1} )).obj { as := PUnit.unit }
    source
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_unitIso :
    FundamentalGroupoid.punitEquivDiscretePUnit.unitIso = CategoryTheory.NatIso.ofComponents (fun (x : FundamentalGroupoid PUnit.{u + 1} ) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (FundamentalGroupoid PUnit.{u + 1} )).obj x)) @FundamentalGroupoid.punitEquivDiscretePUnit.proof_1
    source
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_functor :
    FundamentalGroupoid.punitEquivDiscretePUnit.functor = CategoryTheory.Functor.star (FundamentalGroupoid PUnit.{u + 1} )