Theorems · Definition · category theory

CategoryTheory.Arrow.mapCechConerve

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
        [inst_2 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout g.left (fun x => g.right) fun x => g.hom] →
          (f ⟶ g) → (f.cechConerve ⟶ g.cechConerve)

The morphism between Čech conerves associated to a morphism of arrows.

Defined in

Mathlib.AlgebraicTopology.CechNerve

Cited by

3 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWidePushoutCategoryTheory.Limits.HasWidePushout