Theorems · Definition · category theory

CategoryTheory.Precoverage.ZeroHypercover.pushforward

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      [J.IsStableUnderComposition] →
        [J.HasIsos] →
          {X Y : C} →
            (f : X ⟶ Y) → CategoryTheory.Presieve.singleton f ∈ J.coverings Y → J.ZeroHypercover X → J.ZeroHypercover Y

Compose a 0-hypercover with a morphism on the right.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Precoverage.IsStableUnderCompositionCategoryTheory.Precoverage.HasIsos