Relation of morphism properties with limits #

The following predicates are introduces for morphism properties P:

IsStableUnderBaseChange: P is stable under base change if in all pullback squares, the left map satisfies P if the right map satisfies it.
IsStableUnderCobaseChange: P is stable under cobase change if in all pushout squares, the right map satisfies P if the left map satisfies it.

We define P.universally for the class of morphisms which satisfy P after any base change.

We also introduce properties IsStableUnderProductsOfShape, IsStableUnderLimitsOfShape, IsStableUnderFiniteProducts.

source

class CategoryTheory.MorphismProperty.IsStableUnderBaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) :

Prop

A morphism property is IsStableUnderBaseChange if the base change of such a morphism still falls in the class.

of_isPullback {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : CategoryTheory.IsPullback f' g' g f) (hg : P g) : P g'

Instances

source

class CategoryTheory.MorphismProperty.IsStableUnderCobaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) :

Prop

A morphism property is IsStableUnderCobaseChange if the cobase change of such a morphism still falls in the class.

of_isPushout {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : CategoryTheory.IsPushout g f f' g') (hf : P f) : P f'

Instances

source

theorem CategoryTheory.MorphismProperty.of_isPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : CategoryTheory.IsPullback f' g' g f) (hg : P g) :

P g'

source

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] (hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : CategoryTheory.Limits.HasPullback f g], P g → P (CategoryTheory.Limits.pullback.fst f g)) :

P.IsStableUnderBaseChange

Alternative constructor for IsStableUnderBaseChange.

source

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] :

(CategoryTheory.MorphismProperty.isomorphisms C).IsStableUnderBaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.monomorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] :

(CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderBaseChange

source

@[instance 900]

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] :

P.RespectsIso

source

theorem CategoryTheory.MorphismProperty.pullback_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P g) :

P (CategoryTheory.Limits.pullback.fst f g)

source

@[deprecated CategoryTheory.MorphismProperty.pullback_fst]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P g) :

P (CategoryTheory.Limits.pullback.fst f g)

Alias of CategoryTheory.MorphismProperty.pullback_fst.

source

theorem CategoryTheory.MorphismProperty.pullback_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P f) :

P (CategoryTheory.Limits.pullback.snd f g)

source

@[deprecated CategoryTheory.MorphismProperty.pullback_snd]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [CategoryTheory.Limits.HasPullback f g] (H : P f) :

P (CategoryTheory.Limits.pullback.snd f g)

Alias of CategoryTheory.MorphismProperty.pullback_snd.

source

theorem CategoryTheory.MorphismProperty.baseChange_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) (X : CategoryTheory.Over S) (H : P X.hom) :

P ((CategoryTheory.Over.pullback f).obj X).hom

source

@[deprecated CategoryTheory.MorphismProperty.baseChange_obj]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.baseChange_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) (X : CategoryTheory.Over S) (H : P X.hom) :

P ((CategoryTheory.Over.pullback f).obj X).hom

Alias of CategoryTheory.MorphismProperty.baseChange_obj.

source

theorem CategoryTheory.MorphismProperty.baseChange_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) {X Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P g.left) :

P ((CategoryTheory.Over.pullback f).map g).left

source

@[deprecated CategoryTheory.MorphismProperty.baseChange_map]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.baseChange_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] {S S' : C} (f : S' ⟶ S) {X Y : CategoryTheory.Over S} (g : X ⟶ Y) (H : P g.left) :

P ((CategoryTheory.Over.pullback f).map g).left

Alias of CategoryTheory.MorphismProperty.baseChange_map.

source

theorem CategoryTheory.MorphismProperty.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') :

P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

source

@[deprecated CategoryTheory.MorphismProperty.pullback_map]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] {S X X' Y Y' : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂) (e₁ : f = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : g = CategoryTheory.CategoryStruct.comp i₂ g') :

P (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

Alias of CategoryTheory.MorphismProperty.pullback_map.

source

theorem CategoryTheory.MorphismProperty.of_isPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A A' B B' : C} {f : A ⟶ A'} {g : A ⟶ B} {f' : B ⟶ B'} {g' : A' ⟶ B'} (sq : CategoryTheory.IsPushout g f f' g') (hf : P f) :

P f'

source

theorem CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] (hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B) [inst : CategoryTheory.Limits.HasPushout f g], P f → P (CategoryTheory.Limits.pushout.inr f g)) :

P.IsStableUnderCobaseChange

An alternative constructor for IsStableUnderCobaseChange.

source

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.epimorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] :

(CategoryTheory.MorphismProperty.epimorphisms C).IsStableUnderCobaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] :

P.RespectsIso

source

theorem CategoryTheory.MorphismProperty.pushout_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P g) :

P (CategoryTheory.Limits.pushout.inl f g)

source

@[deprecated CategoryTheory.MorphismProperty.pushout_inl]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inl {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P g) :

P (CategoryTheory.Limits.pushout.inl f g)

Alias of CategoryTheory.MorphismProperty.pushout_inl.

source

theorem CategoryTheory.MorphismProperty.pushout_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P f) :

P (CategoryTheory.Limits.pushout.inr f g)

source

@[deprecated CategoryTheory.MorphismProperty.pushout_inr]

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inr {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] {A B A' : C} (f : A ⟶ A') (g : A ⟶ B) [CategoryTheory.Limits.HasPushout f g] (H : P f) :

P (CategoryTheory.Limits.pushout.inr f g)

Alias of CategoryTheory.MorphismProperty.pushout_inr.

source

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] :

P.op.IsStableUnderBaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} [P.IsStableUnderCobaseChange] :

P.unop.IsStableUnderBaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.op {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] :

P.op.IsStableUnderCobaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.unop {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty Cᵒᵖ} [P.IsStableUnderBaseChange] :

P.unop.IsStableUnderCobaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [Q.IsStableUnderBaseChange] :

(P ⊓ Q).IsStableUnderBaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.inf {C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C} [P.IsStableUnderCobaseChange] [Q.IsStableUnderCobaseChange] :

(P ⊓ Q).IsStableUnderCobaseChange

source

def CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) [CategoryTheory.Category.{u_2, u_1} J] :

Prop

The property that a morphism property W is stable under limits indexed by a category J.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.lim_map {C : Type u} [CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] (hW : W.IsStableUnderLimitsOfShape J) {X Y : CategoryTheory.Functor J C} (f : X ⟶ Y) [CategoryTheory.Limits.HasLimitsOfShape J C] (hf : W.functorCategory J f) :

W (CategoryTheory.Limits.lim.map f)

source

@[reducible, inline]

abbrev CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) :

Prop

The property that a morphism property W is stable under products indexed by a type J.

Equations

W.IsStableUnderProductsOfShape J = W.IsStableUnderLimitsOfShape (CategoryTheory.Discrete J)

Instances For

source

theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1) [W.RespectsIso] [CategoryTheory.Limits.HasProductsOfShape J C] (hW : ∀ (X₁ X₂ : J → C) (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Pi.map f)) :

W.IsStableUnderProductsOfShape J

source

class CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) :

Prop

The condition that a property of morphisms is stable by finite products.

isStableUnderProductsOfShape (J : Type) [Finite J] : W.IsStableUnderProductsOfShape J

Instances

source

theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type) [Finite J] [W.IsStableUnderFiniteProducts] :

W.IsStableUnderProductsOfShape J

source

def CategoryTheory.MorphismProperty.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.MorphismProperty C) :

CategoryTheory.MorphismProperty C

For P : MorphismProperty C, P.diagonal is a morphism property that holds for f : X ⟶ Y whenever P holds for X ⟶ Y xₓ Y.

Equations

P.diagonal f = P (CategoryTheory.Limits.pullback.diagonal f)

Instances For

source

theorem CategoryTheory.MorphismProperty.diagonal_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y} :

P.diagonal f ↔ P (CategoryTheory.Limits.pullback.diagonal f)

source

instance CategoryTheory.MorphismProperty.RespectsIso.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] :

P.diagonal.RespectsIso

source

instance CategoryTheory.MorphismProperty.diagonal_isStableUnderComposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderComposition] [P.RespectsIso] [P.IsStableUnderBaseChange] :

P.diagonal.IsStableUnderComposition

source

instance CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.RespectsIso] :

P.diagonal.IsStableUnderBaseChange

source

theorem CategoryTheory.MorphismProperty.diagonal_isomorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] :

(CategoryTheory.MorphismProperty.isomorphisms C).diagonal = CategoryTheory.MorphismProperty.monomorphisms C

source

theorem CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {P : CategoryTheory.MorphismProperty C} [P.IsStableUnderBaseChange] [P.IsMultiplicative] {Q : CategoryTheory.MorphismProperty C} [Q.IsStableUnderBaseChange] :

P.HasOfPostcompProperty Q ↔ Q ≤ P.diagonal

If P is multiplicative and stable under base change, having the of-postcomp property wrt. Q is equivalent to Q implying P on the diagonal.

source

def CategoryTheory.MorphismProperty.universally {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) :

CategoryTheory.MorphismProperty C

P.universally holds for a morphism f : X ⟶ Y iff P holds for all X ×[Y] Y' ⟶ Y'.

Equations

P.universally f = ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), CategoryTheory.IsPullback f' i₁ i₂ f → P f'

Instances For

source

instance CategoryTheory.MorphismProperty.universally_respectsIso {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) :

P.universally.RespectsIso

source

instance CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) :

P.universally.IsStableUnderBaseChange

source

instance CategoryTheory.MorphismProperty.IsStableUnderComposition.universally {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] (P : CategoryTheory.MorphismProperty C) [hP : P.IsStableUnderComposition] :

P.universally.IsStableUnderComposition

source

theorem CategoryTheory.MorphismProperty.universally_le {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) :

P.universally ≤ P

source

theorem CategoryTheory.MorphismProperty.universally_inf {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.MorphismProperty C) :

(P ⊓ Q).universally = P.universally ⊓ Q.universally

source

theorem CategoryTheory.MorphismProperty.universally_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} :

P.universally = P ↔ P.IsStableUnderBaseChange

source

theorem CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [hP : P.IsStableUnderBaseChange] :

P.universally = P

source

theorem CategoryTheory.MorphismProperty.universally_mono {C : Type u} [CategoryTheory.Category.{v, u} C] :

Monotone CategoryTheory.MorphismProperty.universally

Documentation

Mathlib.CategoryTheory.MorphismProperty.Limits

Relation of morphism properties with limits #