Product

📁 Source: Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

Statistics

Metric	Count
Definitions coneDiscreteComp, piIso, piToPiTop, piTopToPiCone, prodIso, prodToProdTop, proj, projLeft, projRight	9
Theorems coneDiscreteComp_obj_mapCone, instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone, piIso_hom, piIso_inv, piToPiTop_map, piToPiTop_obj_as, preservesProduct, prodIso_hom, prodIso_inv, prodToProdTop_map, prodToProdTop_obj, projLeft_map, projRight_map, proj_map	14
Total	23

FundamentalGroupoidFunctor

Definitions

Name	Category	Theorems
coneDiscreteComp 📖	CompOp	1 math math: coneDiscreteComp_obj_mapCone
piIso 📖	CompOp	2 math math: piIso_hom, piIso_inv
piToPiTop 📖	CompOp	3 math math: piIso_hom, piToPiTop_map, piToPiTop_obj_as
piTopToPiCone 📖	CompOp	1 math math: instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone
prodIso 📖	CompOp	2 math math: prodIso_hom, prodIso_inv
prodToProdTop 📖	CompOp	6 math math: ContinuousMap.Homotopy.apply_zero_path, ContinuousMap.Homotopy.evalAt_eq, prodToProdTop_obj, prodIso_hom, ContinuousMap.Homotopy.apply_one_path, prodToProdTop_map
proj 📖	CompOp	4 math math: instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone, piIso_inv, proj_map, coneDiscreteComp_obj_mapCone
projLeft 📖	CompOp	2 math math: projLeft_map, prodIso_inv
projRight 📖	CompOp	2 math math: prodIso_inv, projRight_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneDiscreteComp_obj_mapCone 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.Cone CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Functor.comp TopCat TopCat.instCategory CategoryTheory.Discrete.functor FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.Limits.Cone.category CategoryTheory.Equivalence.functor coneDiscreteComp CategoryTheory.Functor.mapCone TopCat.piFan TopCat.of Pi.topologicalSpace TopCat.carrier TopCat.str proj	—	—
instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.Fan CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Functor.obj TopCat TopCat.instCategory FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.Limits.Cone.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor TopCat.of Pi.topologicalSpace TopCat.carrier TopCat.str proj CategoryTheory.Grpd.piLimitFan piTopToPiCone	—	CategoryTheory.Limits.Cones.cone_iso_of_hom_iso CategoryTheory.Iso.isIso_inv
piIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Grpd.of CategoryTheory.groupoidPi CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.Grpd.str' TopCat.of Pi.topologicalSpace TopCat.carrier TopCat.str piIso piToPiTop	—	—
piIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Grpd.of CategoryTheory.groupoidPi CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.Grpd.str' TopCat.of Pi.topologicalSpace TopCat.carrier TopCat.str piIso CategoryTheory.Functor.pi' CategoryTheory.Groupoid.toCategory proj	—	—
piToPiTop_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.pi CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' TopCat.of Pi.topologicalSpace TopCat.carrier TopCat.str piToPiTop Path.Homotopic.pi FundamentalGroupoid.as	—	—
piToPiTop_obj_as 📖	mathematical	—	FundamentalGroupoid.as TopCat.carrier TopCat.of Pi.topologicalSpace TopCat.str CategoryTheory.Functor.obj CategoryTheory.pi CategoryTheory.Bundled.α CategoryTheory.Groupoid TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' piToPiTop	—	—
preservesProduct 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.functor FundamentalGroupoid.fundamentalGroupoidFunctor	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone instIsIsoFanGrpdObjTopCatFundamentalGroupoidFunctorPiTopToPiCone
prodIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Grpd.of CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.groupoidProd CategoryTheory.Grpd.str' TopCat.of TopCat.carrier instTopologicalSpaceProd TopCat.str prodIso prodToProdTop	—	—
prodIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Grpd CategoryTheory.Grpd.category CategoryTheory.Grpd.of CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.groupoidProd CategoryTheory.Grpd.str' TopCat.of TopCat.carrier instTopologicalSpaceProd TopCat.str prodIso CategoryTheory.Functor.prod' CategoryTheory.Groupoid.toCategory projLeft projRight	—	—
prodToProdTop_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.prod' CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' TopCat.of TopCat.carrier instTopologicalSpaceProd TopCat.str prodToProdTop Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Path.Homotopic.prod FundamentalGroupoid.as	—	—
prodToProdTop_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bundled.α CategoryTheory.Groupoid TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor CategoryTheory.prod' CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' TopCat.of TopCat.carrier instTopologicalSpaceProd TopCat.str prodToProdTop FundamentalGroupoid.as	—	—
projLeft_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor TopCat.of TopCat.carrier instTopologicalSpaceProd TopCat.str CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' projLeft Path.Homotopic.projLeft FundamentalGroupoid.as	—	—
projRight_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor TopCat.of TopCat.carrier instTopologicalSpaceProd TopCat.str CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' projRight Path.Homotopic.projRight FundamentalGroupoid.as	—	—
proj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Bundled.α CategoryTheory.Groupoid CategoryTheory.Functor.obj TopCat TopCat.instCategory CategoryTheory.Grpd CategoryTheory.Grpd.category FundamentalGroupoid.fundamentalGroupoidFunctor TopCat.of Pi.topologicalSpace TopCat.carrier TopCat.str CategoryTheory.Groupoid.toCategory CategoryTheory.Grpd.str' proj Path.Homotopic.proj FundamentalGroupoid.as	—	—

---

← Back to Index