Theorems · Theorem · category theory

CategoryTheory.Precoverage.IsStableUnderComposition.comp_mem_coverings

∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C}
  [self : J.IsStableUnderComposition] {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
    ∀ {σ : ι → Type (max u v)} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i),
      (∀ (i : ι), CategoryTheory.Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) →
        (CategoryTheory.Presieve.ofArrows (fun p => Y p.fst p.snd) fun x =>
            CategoryTheory.CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈
          J.coverings S

Defined in

Mathlib.CategoryTheory.Sites.Precoverage

Cited by

1 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Precoverage.IsStableUnderComposition