Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-24 07:49 6cb52e67

View on Github →

feat(category_theory/limits): Results about (co)limits in Top (#9985)

  • Provided the explicit topologies for limits and colimits, and specialized this result onto some shapes.
  • Provided the isomorphism between the (co)limits and the constructions in topology/constructions.lean.
  • Provided conditions about whether prod.map and pullback_map are inducing, embedding, etc.

Estimated changes

added theorem Top.colimit_topology
added theorem Top.embedding_prod_map
added theorem Top.inducing_prod_map
added theorem Top.limit_topology
added def Top.pi_fan
added def Top.pi_iso_pi
added theorem Top.pi_iso_pi_inv_π
added def Top.pi_π
added def Top.prod_fst
added def Top.prod_snd
added theorem Top.prod_topology
added def Top.pullback_fst
added theorem Top.pullback_fst_range
added def Top.pullback_snd
added theorem Top.pullback_snd_range
added theorem Top.pullback_topology
added theorem Top.range_prod_map
added theorem Top.range_pullback_map
added def Top.sigma_cofan
added def Top.sigma_ι