Documentation

TauCeti.AlgebraicTopology.CechNerve

Homotopies between maps of Čech nerves, and maps into a Čech nerve #

Let F G : f ⟶ g be two morphisms of arrows with the same component F.right = G.right on the targets. The induced maps of Čech nerves Arrow.mapCechNerve F and Arrow.mapCechNerve G are simplicially homotopic. In degree n the i-th component of the homotopy f.cechNerve _⦋n⦌ ⟶ g.cechNerve _⦋n + 1⦌ repeats the i-th factor of the wide pullback and applies F.left to the factors in positions ≤ i and G.left to the others.

Applied to the Čech nerve of a family of objects over a terminal object, this says that the map induced on Čech nerves by a refinement of covers does not depend on the chosen refinement map, up to homotopy. This is the input for TauCeti.CategoryTheory.cechComplexMapHomotopy, which shows that the maps induced on Čech complexes by two refinement maps are homotopic.

The simplices of cechNerveTerminalFrom U, the Čech nerve of U ⟶ ⊤_ C with ⦋n⦌ ↦ Uⁿ⁺¹, are determined by their vertices, and every family of vertices is the family of vertices of a simplex (CategoryTheory.cechNerveTerminalFrom.hom_ext and CategoryTheory.cechNerveTerminalFrom.lift).

For an object T, the morphisms from T into the Čech nerve of f form an augmented simplicial set over the morphisms T ⟶ f.right which lift along f.hom. It has an extra degeneracy, which inserts a chosen lift of the base as a new first factor; this is Mathlib's extra degeneracy of the Čech nerve of a split epimorphism, Arrow.AugmentedCechNerve.extraDegeneracy, with the section chosen separately over each morphism. For the map from the disjoint union of a family of open sets and T a topological simplex, it shows that the rows of the Čech--singular double complex resolve the singular chains subordinate to the family.

Main definitions #

References #

source
noncomputable def CategoryTheory.Arrow.mapCechNerveHomotopy {C : Type u} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F G : f ⟶ g) (h : Hom.right F = Hom.right G) :
SimplicialObject.Homotopy (mapCechNerve F) (mapCechNerve G)

Morphisms of arrows with the same target component induce homotopic maps of Čech nerves. If F.right = G.right, then Arrow.mapCechNerve F and Arrow.mapCechNerve G are simplicially homotopic.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Arrow.mapCechNerveHomotopy_h_π {C : Type u} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F G : f ⟶ g) (h : Hom.right F = Hom.right G) {n : ℕ} (i : Fin (n + 1)) (j : Fin (n + 2)) :
    CategoryStruct.comp ((mapCechNerveHomotopy F G h).h i) (Limits.WidePullback.π (fun (x : Fin ((Opposite.unop (Opposite.op { len := n + 1 })).len + 1)) => g.hom) j) = CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)) => f.hom) (i.predAbove j)) (if j ≤ i.castSucc then Hom.left F else Hom.left G)

    The j-th factor of the i-th component of mapCechNerveHomotopy F G h is the i.predAbove j-th factor of the source followed by F.left if j ≤ i and by G.left otherwise.

    source
    @[simp]
    theorem CategoryTheory.Arrow.mapCechNerveHomotopy_h_π_assoc {C : Type u} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F G : f ⟶ g) (h : Hom.right F = Hom.right G) {n : ℕ} (i : Fin (n + 1)) (j : Fin (n + 2)) {Z : C} (h✝ : g.left ⟶ Z) :
    CategoryStruct.comp ((mapCechNerveHomotopy F G h).h i) (CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin (n + 1 + 1)) => g.hom) j) h✝) = CategoryStruct.comp (Limits.WidePullback.π (fun (x : Fin (n + 1)) => f.hom) (i.predAbove j)) (CategoryStruct.comp (if j ≤ i.castSucc then Hom.left F else Hom.left G) h✝)

    The j-th factor of the i-th component of mapCechNerveHomotopy F G h is the i.predAbove j-th factor of the source followed by F.left if j ≤ i and by G.left otherwise.

    source
    @[simp]
    theorem CategoryTheory.Arrow.mapCechNerveHomotopy_h_base {C : Type u} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F G : f ⟶ g) (h : Hom.right F = Hom.right G) {n : ℕ} (i : Fin (n + 1)) :
    CategoryStruct.comp ((mapCechNerveHomotopy F G h).h i) (Limits.WidePullback.base fun (x : Fin ((Opposite.unop (Opposite.op { len := n + 1 })).len + 1)) => g.hom) = CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin ((Opposite.unop (Opposite.op { len := n })).len + 1)) => f.hom) (Hom.right F)

    Every component of mapCechNerveHomotopy F G h lies over F.right = G.right.

    source
    @[simp]
    theorem CategoryTheory.Arrow.mapCechNerveHomotopy_h_base_assoc {C : Type u} [Category.{v, u} C] {f g : Arrow C} [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] [∀ (n : ℕ), Limits.HasWidePullback g.right (fun (x : Fin (n + 1)) => g.left) fun (x : Fin (n + 1)) => g.hom] (F G : f ⟶ g) (h : Hom.right F = Hom.right G) {n : ℕ} (i : Fin (n + 1)) {Z : C} (h✝ : g.right ⟶ Z) :
    CategoryStruct.comp ((mapCechNerveHomotopy F G h).h i) (CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1 + 1)) => g.hom) h✝) = CategoryStruct.comp (Limits.WidePullback.base fun (x : Fin (n + 1)) => f.hom) (CategoryStruct.comp (Hom.right F) h✝)

    Every component of mapCechNerveHomotopy F G h lies over F.right = G.right.

    source
    noncomputable def CategoryTheory.Arrow.augmentedCechNerveMapsFrom {C : Type u} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (T : C) :
    SimplicialObject.Augmented (Type v)

    The morphisms from T into the Čech nerve of f, augmented over the morphisms T ⟶ f.right which lift along f.hom. The augmentation composes with the projection WidePullback.base.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Arrow.augmentedCechNerveMapsFrom_left_map {C : Type u} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (T : C) {n m : SimplexCategoryᵒᵖ} (θ : n ⟶ m) (σ : T ⟶ f.cechNerve.obj n) :
      (ConcreteCategory.hom ((f.augmentedCechNerveMapsFrom T).left.map θ)) σ = CategoryStruct.comp σ (f.cechNerve.map θ)

      The simplicial operators act on maps into the Čech nerve by postcomposition.

      source
      @[simp]
      theorem CategoryTheory.Arrow.augmentedCechNerveMapsFrom_hom_app_coe {C : Type u} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (T : C) (n : SimplexCategoryᵒᵖ) (σ : T ⟶ f.cechNerve.obj n) :
      ↑((ConcreteCategory.hom ((f.augmentedCechNerveMapsFrom T).hom.app n)) σ) = CategoryStruct.comp σ (Limits.WidePullback.base fun (x : Fin ((Opposite.unop n).len + 1)) => f.hom)

      The augmentation sends a map into the Čech nerve to its composite with the base.

      The source and target of ConcreteCategory.hom are given explicitly, as left.obj n and right, so that the left-hand side is in simp normal form: elaborated directly they would be (𝟭 _).obj left and (const.obj right).obj n, which simp rewrites first.

      source
      noncomputable def CategoryTheory.Arrow.AugmentedCechNerveMapsFrom.extraDegeneracy {C : Type u} [Category.{v, u} C] (f : Arrow C) [∀ (n : ℕ), Limits.HasWidePullback f.right (fun (x : Fin (n + 1)) => f.left) fun (x : Fin (n + 1)) => f.hom] (T : C) :
      (f.augmentedCechNerveMapsFrom T).ExtraDegeneracy

      Maps into a Čech nerve over liftable maps have an extra degeneracy.

      Instances For
        source
        @[simp]
        theorem CategoryTheory.cechNerveTerminalFrom.map_const_π {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] (U : C) {m : ℕ} (i : Fin ({ len := m }.len + 1)) :
        CategoryStruct.comp ((cechNerveTerminalFrom U).map ({ len := 0 }.const { len := m } i).op) (Limits.Pi.π (fun (x : Fin ({ len := 0 }.len + 1)) => U) 0) = Limits.Pi.π (fun (x : Fin ({ len := m }.len + 1)) => U) i

        The i-th vertex of a simplex of cechNerveTerminalFrom U is its i-th factor.

        source
        theorem CategoryTheory.cechNerveTerminalFrom.hom_ext {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] (U : C) {Z : C} {m : ℕ} {a b : Z ⟶ (cechNerveTerminalFrom U).obj (Opposite.op { len := m })} (h : ∀ (i : Fin ({ len := m }.len + 1)), CategoryStruct.comp a ((cechNerveTerminalFrom U).map ({ len := 0 }.const { len := m } i).op) = CategoryStruct.comp b ((cechNerveTerminalFrom U).map ({ len := 0 }.const { len := m } i).op)) :
        a = b

        Two morphisms into (cechNerveTerminalFrom U) _⦋m⦌ agree if they have the same vertices.

        source
        noncomputable def CategoryTheory.cechNerveTerminalFrom.lift {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] (U : C) {Z : C} {m : ℕ} (a : Fin (m + 1) → (Z ⟶ (cechNerveTerminalFrom U).obj (Opposite.op { len := 0 }))) :
        Z ⟶ (cechNerveTerminalFrom U).obj (Opposite.op { len := m })

        The morphism into (cechNerveTerminalFrom U) _⦋m⦌ with prescribed vertices a i.

        Instances For
          source
          @[simp]
          theorem CategoryTheory.cechNerveTerminalFrom.lift_map_const {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] (U : C) {Z : C} {m : ℕ} (a : Fin (m + 1) → (Z ⟶ (cechNerveTerminalFrom U).obj (Opposite.op { len := 0 }))) (i : Fin (m + 1)) :
          CategoryStruct.comp (lift U a) ((cechNerveTerminalFrom U).map ({ len := 0 }.const { len := m } i).op) = a i

          The i-th vertex of lift U a is a i.

          source
          @[simp]
          theorem CategoryTheory.cechNerveTerminalFrom.lift_map_const_assoc {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] (U : C) {Z : C} {m : ℕ} (a : Fin (m + 1) → (Z ⟶ (cechNerveTerminalFrom U).obj (Opposite.op { len := 0 }))) (i : Fin (m + 1)) {Z✝ : C} (h : (cechNerveTerminalFrom U).obj (Opposite.op { len := 0 }) ⟶ Z✝) :
          CategoryStruct.comp (lift U a) (CategoryStruct.comp ((cechNerveTerminalFrom U).map ({ len := 0 }.const { len := m } i).op) h) = CategoryStruct.comp (a i) h

          The i-th vertex of lift U a is a i.