Theorems · Definition · category theory

CategoryTheory.MorphismProperty.IsLocalAtTarget.recOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.MorphismProperty C} →
      {K : CategoryTheory.Precoverage C} →
        {motive : P.IsLocalAtTarget K → Sort u_1} →
          (t : P.IsLocalAtTarget K) →
            ([toRespects : P.Respects (CategoryTheory.MorphismProperty.isomorphisms C)] →
                (pullbackSnd :
                    ∀ {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X} {U : C} {g : U ⟶ X},
                      R ∈ K.coverings X →
                        R g →
                          P f →
                            ∀ [inst_1 : CategoryTheory.Limits.HasPullback f g],
                              P (CategoryTheory.Limits.pullback.snd f g)) →
                  (of_forall_pullbackSnd :
                      ∀ {X Y : C} {f : Y ⟶ X} {R : CategoryTheory.Presieve X},
                        R ∈ K.coverings X →
                          (∀ {U : C} {g : U ⟶ X} [inst_1 : CategoryTheory.Limits.HasPullback f g],
                              R g → P (CategoryTheory.Limits.pullback.snd f g)) →
                            P f) →
                    motive ⋯) →
              motive t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Local

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category