Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.IsLocalAtTarget

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.Precoverage C → Prop

A property of morphisms P in C is local at the target with respect to the precoverage K if it respects isomorphisms, and: P holds for f : X ⟶ Y if and only if it holds for the restrictions of f to Uᵢ for a 0-hypercover {Uᵢ} of Y in the precoverage K.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

14 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category