Theorems · Definition · category theory

CategoryTheory.MorphismProperty.IsLocalAtSource.recOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.MorphismProperty C} →
      {K : CategoryTheory.Precoverage C} →
        {motive : P.IsLocalAtSource K → Sort u_1} →
          (t : P.IsLocalAtSource K) →
            ([toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)] →
                (comp :
                    ∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
                      R ∈ K.coverings X →
                        ∀ {U : C} (g : U ⟶ X), R g → P f → P (CategoryTheory.CategoryStruct.comp g f)) →
                  (of_forall_comp :
                      ∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
                        R ∈ K.coverings X →
                          (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f)) → P f) →
                    motive ⋯) →
              motive t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.Category