Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit

Fundamental groupoid of punit #

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

source
📐 coverage
instance Path.instSubsingletonPUnitUnit :
Subsingleton (Path PUnit.unit PUnit.unit)
source
📐 coverage
instance FundamentalGroupoid.instSubsingletonHomPUnit {x y : FundamentalGroupoid PUnit.{u_1 + 1}} :
Subsingleton (x ⟶ y)
source
🔸 coverage
noncomputable def FundamentalGroupoid.punitEquivDiscretePUnit :
FundamentalGroupoid PUnit.{u + 1} ≌ CategoryTheory.Discrete PUnit.{v + 1}

Equivalence of groupoids between fundamental groupoid of punit and punit

Instances For
    source
    📐 coverage
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_functor :
    punitEquivDiscretePUnit.functor = CategoryTheory.Functor.star (FundamentalGroupoid PUnit.{u + 1})
    source
    📐 coverage
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_inverse :
    punitEquivDiscretePUnit.inverse = (CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{v + 1})).obj { as := PUnit.unit }
    source
    📐 coverage
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_counitIso :
    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
    📐 coverage
    @[simp]
    theorem FundamentalGroupoid.punitEquivDiscretePUnit_unitIso :
    punitEquivDiscretePUnit.unitIso = CategoryTheory.NatIso.ofComponents (fun (x : FundamentalGroupoid PUnit.{u + 1}) => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (FundamentalGroupoid PUnit.{u + 1})).obj x)) @punitEquivDiscretePUnit._proof_2