LeanPool.WhiteheadTheorem.HomotopyGroup.InducedMaps

Imported Lean Pool material for LeanPool.WhiteheadTheorem.HomotopyGroup.InducedMaps.

@[reducible, inline]

abbrev PointedTopCat : Type (u_1 + 1)

PointedTopCat

Equations

• PointedTopCat = CategoryTheory.Under (TopCat.of PUnit.{?u.1 + 1})

@[reducible, inline]

abbrev PointedTopCat.of {X : Type u} [TopologicalSpace X] (point : X) : PointedTopCat

Make a pointed topological space from X and a piont in X.

Equations

• PointedTopCat.of point = CategoryTheory.Under.mk (TopCat.ofHom (ContinuousMap.const PUnit.{?u.1 + 1} point))

@[reducible, inline]

abbrev PointedTopCat.ofHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (point : X) : of point ⟶ of (f point)

Typecheck a ContinuousMap as a morphism in PointedTopCat, by choosing a point in X.

Equations

• PointedTopCat.ofHom f point = CategoryTheory.Under.homMk (TopCat.ofHom f) ⋯

@[reducible, inline]

abbrev PointedTopCat.Hom.rwTargetPt {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (point : X) (gf : g = f) : of point ⟶ of (f point)

Change the target point of a morphism of PointedTopCat from g point to f point, given g = f. Useful to fix definitional equality.

Equations

• PointedTopCat.Hom.rwTargetPt point gf = CategoryTheory.Under.homMk (TopCat.ofHom g) ⋯

theorem PointedTopCat.Hom.toFun_rwTargetPt {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (point : X) (gf : g = f) : (TopCat.Hom.hom (CategoryTheory.Under.Hom.right (rwTargetPt point gf))).toFun = ⇑g

theorem PointedTopCat.Hom.rwTargetPt_eq {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (point : X) (gf : g = f) : rwTargetPt point gf = ofHom f point

@[reducible, inline]

abbrev PointedTopCat.ofHom' {X Y : TopCat} (f : X ⟶ Y) (point : ↑X) : of point ⟶ of ((CategoryTheory.ConcreteCategory.hom f) point)

Typecheck a morphism in TopCat as a morphism in PointedTopCat, by choosing a point in X.

Equations

• PointedTopCat.ofHom' f point = CategoryTheory.Under.homMk f ⋯

@[reducible, inline]

abbrev PointedTopCat.Hom'.rwTargetPt {X Y : TopCat} {f g : X ⟶ Y} (point : ↑X) (gf : g = f) : of point ⟶ of ((CategoryTheory.ConcreteCategory.hom f) point)

Change the target point of a morphism of PointedTopCat from g point to f point, given g = f. Useful to fix definitional equality.

Equations

• PointedTopCat.Hom'.rwTargetPt point gf = CategoryTheory.Under.homMk g ⋯

theorem PointedTopCat.Hom'.toFun_rwTargetPt {X Y : TopCat} {f g : X ⟶ Y} (point : ↑X) (gf : g = f) : (TopCat.Hom.hom (CategoryTheory.Under.Hom.right (rwTargetPt point gf))).toFun = ⇑(CategoryTheory.ConcreteCategory.hom g)

theorem PointedTopCat.Hom'.rwTargetPt_eq {X Y : TopCat} {f g : X ⟶ Y} (point : ↑X) (gf : g = f) : rwTargetPt point gf = ofHom' f point

@[reducible, inline]

abbrev PointedTopCat.as (X : PointedTopCat) : TopCat

Regard a pointed topological space as simply a topological space.

Equations

• X.as = CategoryTheory.Under.right X

@[reducible, inline]

abbrev PointedTopCat.point (X : PointedTopCat) : ↑X.as

The distinguished piont of a pointed topological space

Equations

• X.point = (TopCat.Hom.hom (CategoryTheory.Under.hom X)) PUnit.unit

theorem PointedTopCat.w {X Y : PointedTopCat} (f : X ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Under.Hom.right f)) X.point = Y.point

A morphism between pointed topological spaces maps the base point to the base point.

theorem TopCat.isIso_of_isHomeomorph {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (hf : IsHomeomorph ⇑f) : CategoryTheory.IsIso (ofHom f)

theorem PointedTopCat.isIso_of_isHomeomorph {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (point : X) (hf : IsHomeomorph ⇑f) : CategoryTheory.IsIso (ofHom f point)

theorem PointedTopCat.ofHom_comp {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(X, Y)) (g : C(Y, Z)) (point : X) : ofHom (g.comp f) point = CategoryTheory.CategoryStruct.comp (ofHom f point) (ofHom g (f point))

theorem PointedTopCat.ofHom'_comp {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (point : ↑X) : ofHom' (CategoryTheory.CategoryStruct.comp f g) point = CategoryTheory.CategoryStruct.comp (ofHom' f point) (ofHom' g ((CategoryTheory.ConcreteCategory.hom f) point))

theorem Pointed.isIso_iff_bijective {A B : Type u} {a₀ : A} {b₀ : B} (f : of a₀ ⟶ of b₀) : CategoryTheory.IsIso f ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)

@[reducible, inline]

abbrev Pointed.Hom.rwTargetPt {X Y : Type u} (point : X) {f g : X → Y} (gf : g = f) : of point ⟶ of (f point)

Change the target point of a Pointed.Hom from g point to f point, given g = f. Useful to fix definitional equality.

Equations

• Pointed.Hom.rwTargetPt point gf = { toFun := g, map_point := ⋯ }

theorem Pointed.Hom.toFun_rwTargetPt {X Y : Type u} (point : X) {f g : X → Y} (gf : g = f) : (rwTargetPt point gf).toFun = g

theorem Pointed.Hom.rwTargetPt_eq {X Y : Type u} (point : X) {f g : X → Y} (gf : g = f) : rwTargetPt point gf = { toFun := f, map_point := ⋯ }

def GenLoop.inducedMap' (n : ℕ) {X Y : PointedTopCat} (f : X ⟶ Y) : ↑(GenLoop (Fin n) (↑X.as) X.point) → ↑(GenLoop (Fin n) (↑Y.as) Y.point)

The map of GenLoops induced by a morphism f : X ⟶ Y of pointed topological spaces

Equations

• GenLoop.inducedMap' n f α = ⟨(TopCat.Hom.hom (CategoryTheory.Under.Hom.right f)).comp ↑α, ⋯⟩

@[reducible, inline]

abbrev GenLoop.inducedMap {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) (x : X) (f : C(X, Y)) : ↑(GenLoop (Fin n) X x) → ↑(GenLoop (Fin n) Y (f x))

The map of GenLoops induced by a continuous map f : C(X, Y)

Equations

• GenLoop.inducedMap n x f = GenLoop.inducedMap' n (PointedTopCat.ofHom f x)

def HomotopyGroup.inducedMap' (n : ℕ) {X Y : PointedTopCat} (f : X ⟶ Y) : Pi n (↑X.as) X.point → Pi n (↑Y.as) Y.point

The map between homotopy groups (as sets) induced by a morphism f : X ⟶ Y of pointed topological spaces

Equations

• HomotopyGroup.inducedMap' n f = Quotient.map (GenLoop.inducedMap' n f) ⋯

theorem HomotopyGroup.inducedMap'_default (n : ℕ) {X Y : PointedTopCat} (f : X ⟶ Y) : inducedMap' n f default = default

@[reducible, inline]

abbrev HomotopyGroup.inducedMap {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) (x : X) (f : C(X, Y)) : Pi n X x → Pi n Y (f x)

The map between homotopy groups (as sets) induced by a continuous map f : C(X, Y)

Equations

• HomotopyGroup.inducedMap n x f = HomotopyGroup.inducedMap' n (PointedTopCat.ofHom f x)

@[reducible, inline]

abbrev HomotopyGroup.inducedMap.rwTargetPt {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) {f g : C(X, Y)} (x : X) (gf : g = f) : Pi n X x → Pi n Y (f x)

Change an induced map's target point from g x to f x, given g = f. Useful to fix definitional equality.

Equations

• HomotopyGroup.inducedMap.rwTargetPt n x gf = HomotopyGroup.inducedMap' n (PointedTopCat.Hom.rwTargetPt x gf)

theorem HomotopyGroup.inducedMap.rwTargetPt_eq {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) {f g : C(X, Y)} (x : X) (gf : g = f) : rwTargetPt n x gf = inducedMap n x f

noncomputable def HomotopyGroup.functorToType (n : ℕ) : CategoryTheory.Functor PointedTopCat (Type u)

π_n is a functor sending a based topological space (X, x₀) to its n-th homotopy group (as a type, ignoring its group structure) based at x₀.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HomotopyGroup.functorToPointed (n : ℕ) : CategoryTheory.Functor PointedTopCat Pointed

π_n is a functor sending a based topological space (X, x₀) to its n-th homotopy group (as a pointed type whose base point is the contant map, ignoring its group structure) based at x₀.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev HomotopyGroup.inducedPointedHom {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) (x₀ : X) (f : C(X, Y)) : Pointed.of default ⟶ Pointed.of default

The morphism $f_{*} : π_n(X, x₀) → π_n(Y, f(x₀))$ in the category Pointed, induced by the continuous map f : C(X, Y)

Equations

• HomotopyGroup.inducedPointedHom n x₀ f = (HomotopyGroup.functorToPointed n).map (PointedTopCat.ofHom f x₀)

@[reducible, inline]

noncomputable abbrev HomotopyGroup.inducedPointedHom' (n : ℕ) {X Y : TopCat} (x₀ : ↑X) (f : X ⟶ Y) : Pointed.of default ⟶ Pointed.of default

The morphism $f_{*} : π_n(X, x₀) → π_n(Y, f(x₀))$ in the category Pointed, induced by the morphism f : X ⟶ Y in TopCat

Equations

• HomotopyGroup.inducedPointedHom' n x₀ f = (HomotopyGroup.functorToPointed n).map (PointedTopCat.ofHom' f x₀)

theorem HomotopyGroup.inducedPointedHom'_eq_inducedPointedHom (n : ℕ) {X Y : TopCat} (x₀ : ↑X) (f : X ⟶ Y) : inducedPointedHom' n x₀ f = inducedPointedHom n x₀ (TopCat.Hom.hom f)

@[reducible, inline]

noncomputable abbrev HomotopyGroup.inducedPointedHom.isoTarget {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) {f g : C(X, Y)} (x₀ : X) (gf : g = f) : Pointed.of default ≅ Pointed.of default

isoTarget

Equations

• HomotopyGroup.inducedPointedHom.isoTarget n x₀ gf = gf ▸ CategoryTheory.Iso.refl (Pointed.of default)

@[reducible, inline]

noncomputable abbrev HomotopyGroup.inducedPointedHom.rwTargetPt {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) {f g : C(X, Y)} (x₀ : X) (gf : g = f) : Pointed.of default ⟶ Pointed.of default

Change an induced pointed morphism's target point from g x₀ to f x₀, given g = f. Useful to fix definitional equality.

Equations

• HomotopyGroup.inducedPointedHom.rwTargetPt n x₀ gf = (HomotopyGroup.functorToPointed n).map (PointedTopCat.Hom.rwTargetPt x₀ gf)

theorem HomotopyGroup.inducedPointedHom.toFun_rwTargetPt {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) {f g : C(X, Y)} (x₀ : X) (gf : g = f) : (rwTargetPt n x₀ gf).toFun = inducedMap.rwTargetPt n x₀ gf

theorem HomotopyGroup.inducedPointedHom.rwTargetPt_eq {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) {f g : C(X, Y)} (x₀ : X) (gf : g = f) : rwTargetPt n x₀ gf = inducedPointedHom n x₀ f

@[reducible, inline]

noncomputable abbrev HomotopyGroup.inducedPointedHom'.isoTarget (n : ℕ) {X Y : TopCat} (x₀ : ↑X) {f g : X ⟶ Y} (gf : g = f) : Pointed.of default ≅ Pointed.of default

isoTarget

Equations

• HomotopyGroup.inducedPointedHom'.isoTarget n x₀ gf = gf ▸ CategoryTheory.Iso.refl (Pointed.of default)

@[reducible, inline]

noncomputable abbrev HomotopyGroup.inducedPointedHom'.rwTargetPt (n : ℕ) {X Y : TopCat} (x₀ : ↑X) {f g : X ⟶ Y} (gf : g = f) : Pointed.of default ⟶ Pointed.of default

Change an induced pointed morphism's target point from g x₀ to f x₀, given g = f. Useful to fix definitional equality.

Equations

• HomotopyGroup.inducedPointedHom'.rwTargetPt n x₀ gf = (HomotopyGroup.functorToPointed n).map (PointedTopCat.Hom'.rwTargetPt x₀ gf)

theorem HomotopyGroup.inducedPointedHom'.toFun_rwTargetPt (n : ℕ) {X Y : TopCat} (x₀ : ↑X) {f g : X ⟶ Y} (gf : g = f) : (rwTargetPt n x₀ gf).toFun = inducedMap.rwTargetPt n x₀ ⋯

theorem HomotopyGroup.inducedPointedHom'.rwTargetPt_eq (n : ℕ) {X Y : TopCat} (x₀ : ↑X) {f g : X ⟶ Y} (gf : g = f) : rwTargetPt n x₀ gf = inducedPointedHom' n x₀ f

theorem HomotopyGroup.isIso_inducedPointedHom_of_isHomeomorph {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (n : ℕ) (x₀ : X) (f : C(X, Y)) (hf : IsHomeomorph ⇑f) : CategoryTheory.IsIso (inducedPointedHom n x₀ f)

instance HomotopyGroup.isIso_inducedPointedHom_id {X : Type u} [TopologicalSpace X] (n : ℕ) (x₀ : X) : CategoryTheory.IsIso (inducedPointedHom n x₀ (ContinuousMap.id X))

theorem HomotopyGroup.inducedPointedHom_comp {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (n : ℕ) (x₀ : X) (f : C(X, Y)) (g : C(Y, Z)) : inducedPointedHom n x₀ (g.comp f) = CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₀ f) (inducedPointedHom n (f x₀) g)

theorem HomotopyGroup.inducedPointedHom_comp_isoTarget_eq_comp {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (n : ℕ) (x₀ : X) {h : C(X, Z)} {f : C(X, Y)} {g : C(Y, Z)} (hgf : h = g.comp f) : CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₀ h) (inducedPointedHom.isoTarget n x₀ hgf).hom = CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₀ f) (inducedPointedHom n (f x₀) g)

theorem HomotopyGroup.inducedPointedHom_eq_comp_of_eq_comp {X Y Z : Type u} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (n : ℕ) (x₀ : X) {h : C(X, Z)} {f : C(X, Y)} {g : C(Y, Z)} (hgf : h = g.comp f) : inducedPointedHom.rwTargetPt n x₀ hgf = CategoryTheory.CategoryStruct.comp (inducedPointedHom n x₀ f) (inducedPointedHom n (f x₀) g)

theorem HomotopyGroup.inducedPointedHom'_comp (n : ℕ) {X Y Z : TopCat} (x₀ : ↑X) (f : X ⟶ Y) (g : Y ⟶ Z) : inducedPointedHom' n x₀ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (inducedPointedHom' n x₀ f) (inducedPointedHom' n ((CategoryTheory.ConcreteCategory.hom f) x₀) g)

theorem HomotopyGroup.inducedPointedHom'_comp_isoTarget_eq_comp (n : ℕ) {X Y Z : TopCat} (x₀ : ↑X) {h : X ⟶ Z} {f : X ⟶ Y} {g : Y ⟶ Z} (hfg : h = CategoryTheory.CategoryStruct.comp f g) : CategoryTheory.CategoryStruct.comp (inducedPointedHom' n x₀ h) (inducedPointedHom'.isoTarget n x₀ hfg).hom = CategoryTheory.CategoryStruct.comp (inducedPointedHom' n x₀ f) (inducedPointedHom' n ((CategoryTheory.ConcreteCategory.hom f) x₀) g)

theorem HomotopyGroup.inducedPointedHom'_eq_comp_of_eq_comp (n : ℕ) {X Y Z : TopCat} (x₀ : ↑X) {h : X ⟶ Z} {f : X ⟶ Y} {g : Y ⟶ Z} (hfg : h = CategoryTheory.CategoryStruct.comp f g) : inducedPointedHom'.rwTargetPt n x₀ hfg = CategoryTheory.CategoryStruct.comp (inducedPointedHom' n x₀ f) (inducedPointedHom' n ((CategoryTheory.ConcreteCategory.hom f) x₀) g)