Properties of morphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We provide the basic framework for talking about properties of morphisms. The following meta-properties are defined
respects_iso:Prespects isomorphisms ifP f → P (e ≫ f)andP f → P (f ≫ e), whereeis an isomorphism.stable_under_composition:Pis stable under composition ifP f → P g → P (f ≫ g).stable_under_base_change:Pis stable under base change if in all pullback squares, the left map satisfiesPif the right map satisfies it.stable_under_cobase_change:Pis stable under cobase change if in all pushout squares, the right map satisfiesPif the left map satisfies it.
A morphism_property C is a class of morphisms between objects in C.
Equations
- category_theory.morphism_property C = Π ⦃X Y : C⦄, (X ⟶ Y) → Prop
Instances for category_theory.morphism_property
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
- category_theory.morphism_property.has_subset = {subset := λ (P₁ P₂ : category_theory.morphism_property C), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P₁ f → P₂ f}
@[protected, instance]
Equations
- category_theory.morphism_property.has_inter = {inter := λ (P₁ P₂ : category_theory.morphism_property C) (X Y : C) (f : X ⟶ Y), P₁ f ∧ P₂ f}
@[simp]
def
category_theory.morphism_property.op
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
The morphism property in Cᵒᵖ associated to a morphism property in C
Instances for category_theory.morphism_property.op
@[simp]
def
category_theory.morphism_property.unop
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property Cᵒᵖ) :
The morphism property in C associated to a morphism property in Cᵒᵖ
theorem
category_theory.morphism_property.unop_op
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
theorem
category_theory.morphism_property.op_unop
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property Cᵒᵖ) :
def
category_theory.morphism_property.inverse_image
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
(P : category_theory.morphism_property D)
(F : C ⥤ D) :
The inverse image of a morphism_property D by a functor C ⥤ D
Equations
- P.inverse_image F = λ (X Y : C) (f : X ⟶ Y), P (F.map f)
def
category_theory.morphism_property.respects_iso
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
Prop
A morphism property respects_iso if it still holds when composed with an isomorphism
theorem
category_theory.morphism_property.respects_iso.op
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(h : P.respects_iso) :
theorem
category_theory.morphism_property.respects_iso.unop
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property Cᵒᵖ}
(h : P.respects_iso) :
def
category_theory.morphism_property.stable_under_composition
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
Prop
A morphism property is stable_under_composition if the composition of two such morphisms
still falls in the class.
theorem
category_theory.morphism_property.stable_under_composition.op
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(h : P.stable_under_composition) :
theorem
category_theory.morphism_property.stable_under_composition.unop
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property Cᵒᵖ}
(h : P.stable_under_composition) :
def
category_theory.morphism_property.stable_under_inverse
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
Prop
A morphism property is stable_under_inverse if the inverse of a morphism satisfying
the property still falls in the class.
theorem
category_theory.morphism_property.stable_under_inverse.op
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(h : P.stable_under_inverse) :
theorem
category_theory.morphism_property.stable_under_inverse.unop
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property Cᵒᵖ}
(h : P.stable_under_inverse) :
def
category_theory.morphism_property.stable_under_base_change
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
Prop
A morphism property is stable_under_base_change if the base change of such a morphism
still falls in the class.
Equations
- P.stable_under_base_change = ∀ ⦃X Y Y' S : C⦄ ⦃f : X ⟶ S⦄ ⦃g : Y ⟶ S⦄ ⦃f' : Y' ⟶ Y⦄ ⦃g' : Y' ⟶ X⦄, category_theory.is_pullback f' g' g f → P g → P g'
def
category_theory.morphism_property.stable_under_cobase_change
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
Prop
A morphism property is stable_under_cobase_change if the cobase change of such a morphism
still falls in the class.
Equations
- P.stable_under_cobase_change = ∀ ⦃A A' B B' : C⦄ ⦃f : A ⟶ A'⦄ ⦃g : A ⟶ B⦄ ⦃f' : B ⟶ B'⦄ ⦃g' : A' ⟶ B'⦄, category_theory.is_pushout g f f' g' → P f → P f'
theorem
category_theory.morphism_property.stable_under_composition.respects_iso
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_composition)
(hP' : ∀ {X Y : C} (e : X ≅ Y), P e.hom) :
theorem
category_theory.morphism_property.respects_iso.cancel_left_is_iso
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.respects_iso)
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.is_iso f] :
theorem
category_theory.morphism_property.respects_iso.cancel_right_is_iso
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.respects_iso)
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.is_iso g] :
theorem
category_theory.morphism_property.respects_iso.arrow_iso_iff
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.respects_iso)
{f g : category_theory.arrow C}
(e : f ≅ g) :
theorem
category_theory.morphism_property.respects_iso.arrow_mk_iso_iff
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.respects_iso)
{W X Y Z : C}
{f : W ⟶ X}
{g : Y ⟶ Z}
(e : category_theory.arrow.mk f ≅ category_theory.arrow.mk g) :
P f ↔ P g
theorem
category_theory.morphism_property.respects_iso.of_respects_arrow_iso
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C)
(hP : ∀ (f g : category_theory.arrow C), (f ≅ g) → P f.hom → P g.hom) :
theorem
category_theory.morphism_property.stable_under_base_change.mk
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
[category_theory.limits.has_pullbacks C]
(hP₁ : P.respects_iso)
(hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S), P g → P category_theory.limits.pullback.fst) :
theorem
category_theory.morphism_property.stable_under_base_change.respects_iso
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change) :
theorem
category_theory.morphism_property.stable_under_base_change.fst
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change)
{X Y S : C}
(f : X ⟶ S)
(g : Y ⟶ S)
[category_theory.limits.has_pullback f g]
(H : P g) :
theorem
category_theory.morphism_property.stable_under_base_change.snd
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change)
{X Y S : C}
(f : X ⟶ S)
(g : Y ⟶ S)
[category_theory.limits.has_pullback f g]
(H : P f) :
theorem
category_theory.morphism_property.stable_under_base_change.base_change_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change)
{S S' : C}
(f : S' ⟶ S)
(X : category_theory.over S)
(H : P X.hom) :
P ((category_theory.limits.base_change f).obj X).hom
theorem
category_theory.morphism_property.stable_under_base_change.base_change_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change)
{S S' : C}
(f : S' ⟶ S)
{X Y : category_theory.over S}
(g : X ⟶ Y)
(H : P g.left) :
P ((category_theory.limits.base_change f).map g).left
theorem
category_theory.morphism_property.stable_under_base_change.pullback_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change)
(hP' : P.stable_under_composition)
{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 = i₁ ≫ f')
(e₂ : g = i₂ ≫ g') :
P (category_theory.limits.pullback.map f g f' g' i₁ i₂ (𝟙 S) _ _)
theorem
category_theory.morphism_property.stable_under_cobase_change.mk
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
[category_theory.limits.has_pushouts C]
(hP₁ : P.respects_iso)
(hP₂ : ∀ (A B A' : C) (f : A ⟶ A') (g : A ⟶ B), P f → P category_theory.limits.pushout.inr) :
theorem
category_theory.morphism_property.stable_under_cobase_change.respects_iso
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_cobase_change) :
theorem
category_theory.morphism_property.stable_under_cobase_change.inl
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_cobase_change)
{A B A' : C}
(f : A ⟶ A')
(g : A ⟶ B)
[category_theory.limits.has_pushout f g]
(H : P g) :
theorem
category_theory.morphism_property.stable_under_cobase_change.inr
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_cobase_change)
{A B A' : C}
(f : A ⟶ A')
(g : A ⟶ B)
[category_theory.limits.has_pushout f g]
(H : P f) :
theorem
category_theory.morphism_property.stable_under_cobase_change.op
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_cobase_change) :
theorem
category_theory.morphism_property.stable_under_cobase_change.unop
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property Cᵒᵖ}
(hP : P.stable_under_cobase_change) :
theorem
category_theory.morphism_property.stable_under_base_change.op
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change) :
theorem
category_theory.morphism_property.stable_under_base_change.unop
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property Cᵒᵖ}
(hP : P.stable_under_base_change) :
def
category_theory.morphism_property.is_inverted_by
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
(P : category_theory.morphism_property C)
(F : C ⥤ D) :
Prop
If P : morphism_property C and F : C ⥤ D, then
P.is_inverted_by F means that all morphisms in P are mapped by F
to isomorphisms in D.
Equations
- P.is_inverted_by F = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P f → category_theory.is_iso (F.map f)
theorem
category_theory.morphism_property.is_inverted_by.of_comp
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₃ : Type u_3}
[category_theory.category C₁]
[category_theory.category C₂]
[category_theory.category C₃]
(W : category_theory.morphism_property C₁)
(F : C₁ ⥤ C₂)
(hF : W.is_inverted_by F)
(G : C₂ ⥤ C₃) :
W.is_inverted_by (F ⋙ G)
theorem
category_theory.morphism_property.is_inverted_by.op
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{W : category_theory.morphism_property C}
{L : C ⥤ D}
(h : W.is_inverted_by L) :
W.op.is_inverted_by L.op
theorem
category_theory.morphism_property.is_inverted_by.right_op
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{W : category_theory.morphism_property C}
{L : Cᵒᵖ ⥤ D}
(h : W.op.is_inverted_by L) :
theorem
category_theory.morphism_property.is_inverted_by.left_op
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{W : category_theory.morphism_property C}
{L : C ⥤ Dᵒᵖ}
(h : W.is_inverted_by L) :
W.op.is_inverted_by L.left_op
theorem
category_theory.morphism_property.is_inverted_by.unop
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{W : category_theory.morphism_property C}
{L : Cᵒᵖ ⥤ Dᵒᵖ}
(h : W.op.is_inverted_by L) :
W.is_inverted_by L.unop
@[simp]
def
category_theory.morphism_property.naturality_property
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{F₁ F₂ : C ⥤ D}
(app : Π (X : C), F₁.obj X ⟶ F₂.obj X) :
Given app : Π X, F₁.obj X ⟶ F₂.obj X where F₁ and F₂ are two functors,
this is the morphism_property C satisfied by the morphisms in C with respect
to whom app is natural.
theorem
category_theory.morphism_property.naturality_property.is_stable_under_composition
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{F₁ F₂ : C ⥤ D}
(app : Π (X : C), F₁.obj X ⟶ F₂.obj X) :
theorem
category_theory.morphism_property.naturality_property.is_stable_under_inverse
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{F₁ F₂ : C ⥤ D}
(app : Π (X : C), F₁.obj X ⟶ F₂.obj X) :
theorem
category_theory.morphism_property.respects_iso.inverse_image
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{P : category_theory.morphism_property D}
(h : P.respects_iso)
(F : C ⥤ D) :
(P.inverse_image F).respects_iso
theorem
category_theory.morphism_property.stable_under_composition.inverse_image
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
{P : category_theory.morphism_property D}
(h : P.stable_under_composition)
(F : C ⥤ D) :
The morphism_property C satisfied by isomorphisms in C.
Equations
- category_theory.morphism_property.isomorphisms C = λ (X Y : C) (f : X ⟶ Y), category_theory.is_iso f
The morphism_property C satisfied by monomorphisms in C.
Equations
- category_theory.morphism_property.monomorphisms C = λ (X Y : C) (f : X ⟶ Y), category_theory.mono f
The morphism_property C satisfied by epimorphisms in C.
Equations
- category_theory.morphism_property.epimorphisms C = λ (X Y : C) (f : X ⟶ Y), category_theory.epi f
@[simp]
theorem
category_theory.morphism_property.isomorphisms.iff
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.morphism_property.monomorphisms.iff
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.morphism_property.epimorphisms.iff
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y) :
theorem
category_theory.morphism_property.isomorphisms.infer_property
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.is_iso f] :
theorem
category_theory.morphism_property.monomorphisms.infer_property
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.mono f] :
theorem
category_theory.morphism_property.epimorphisms.infer_property
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[hf : category_theory.epi f] :
@[nolint]
def
category_theory.morphism_property.functors_inverting
{C : Type u}
[category_theory.category C]
(W : category_theory.morphism_property C)
(D : Type u_1)
[category_theory.category D] :
Type (max v u_2 u u_1)
The full subcategory of C ⥤ D consisting of functors inverting morphisms in W
Equations
- W.functors_inverting D = category_theory.full_subcategory (λ (F : C ⥤ D), W.is_inverted_by F)
Instances for category_theory.morphism_property.functors_inverting
@[protected, instance]
def
category_theory.morphism_property.functors_inverting.category
{C : Type u}
[category_theory.category C]
(W : category_theory.morphism_property C)
(D : Type u_1)
[category_theory.category D] :
def
category_theory.morphism_property.functors_inverting.mk
{C : Type u}
[category_theory.category C]
{W : category_theory.morphism_property C}
{D : Type u_1}
[category_theory.category D]
(F : C ⥤ D)
(hF : W.is_inverted_by F) :
A constructor for W.functors_inverting D
Equations
- category_theory.morphism_property.functors_inverting.mk F hF = {obj := F, property := hF}
theorem
category_theory.morphism_property.is_inverted_by.iff_of_iso
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
(W : category_theory.morphism_property C)
{F₁ F₂ : C ⥤ D}
(e : F₁ ≅ F₂) :
W.is_inverted_by F₁ ↔ W.is_inverted_by F₂
def
category_theory.morphism_property.diagonal
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
(P : category_theory.morphism_property C) :
For P : morphism_property C, P.diagonal is a morphism property that holds for f : X ⟶ Y
whenever P holds for X ⟶ Y xₓ Y.
Equations
- P.diagonal = λ (X Y : C) (f : X ⟶ Y), P (category_theory.limits.pullback.diagonal f)
theorem
category_theory.morphism_property.diagonal_iff
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
{X Y : C}
{f : X ⟶ Y} :
theorem
category_theory.morphism_property.respects_iso.diagonal
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
(hP : P.respects_iso) :
theorem
category_theory.morphism_property.stable_under_composition.diagonal
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_composition)
(hP' : P.respects_iso)
(hP'' : P.stable_under_base_change) :
theorem
category_theory.morphism_property.stable_under_base_change.diagonal
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_pullbacks C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change)
(hP' : P.respects_iso) :
def
category_theory.morphism_property.universally
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
P.universally holds for a morphism f : X ⟶ Y iff P holds for all X ×[Y] Y' ⟶ Y'.
Equations
- P.universally = λ (X Y : C) (f : X ⟶ Y), ∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), category_theory.is_pullback f' i₁ i₂ f → P f'
theorem
category_theory.morphism_property.universally_respects_iso
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
theorem
category_theory.morphism_property.universally_le
{C : Type u}
[category_theory.category C]
(P : category_theory.morphism_property C) :
P.universally ≤ P
theorem
category_theory.morphism_property.stable_under_base_change.universally_eq
{C : Type u}
[category_theory.category C]
{P : category_theory.morphism_property C}
(hP : P.stable_under_base_change) :
P.universally = P
@[protected]
def
category_theory.morphism_property.injective
(C : Type u)
[category_theory.category C]
[category_theory.concrete_category C] :
Injectiveness (in a concrete category) as a morphism_property
Equations
- category_theory.morphism_property.injective C = λ (X Y : C) (f : X ⟶ Y), function.injective ⇑f
@[protected]
def
category_theory.morphism_property.surjective
(C : Type u)
[category_theory.category C]
[category_theory.concrete_category C] :
Surjectiveness (in a concrete category) as a morphism_property
Equations
- category_theory.morphism_property.surjective C = λ (X Y : C) (f : X ⟶ Y), function.surjective ⇑f
@[protected]
def
category_theory.morphism_property.bijective
(C : Type u)
[category_theory.category C]
[category_theory.concrete_category C] :
Bijectiveness (in a concrete category) as a morphism_property
Equations
- category_theory.morphism_property.bijective C = λ (X Y : C) (f : X ⟶ Y), function.bijective ⇑f