Commit 2024-04-27 05:44 9e489ab7

View on Github →

chore: split CategoryTheory.MorphismProperty (#12393) The file CategoryTheory.MorphismProperty is split into five files Basic, Composition, Limits, Concrete, IsInvertedBy.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory.lean

Modified Mathlib/Algebra/Homology/HomotopyCofiber.lean

Modified Mathlib/Algebra/Homology/Localization.lean

Modified Mathlib/Algebra/Homology/ShortComplex/Exact.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/CategoryTheory/Localization/FiniteProducts.lean

Modified Mathlib/CategoryTheory/Localization/Pi.lean

Modified Mathlib/CategoryTheory/Localization/Prod.lean

Deleted Mathlib/CategoryTheory/MorphismProperty.lean

deleted theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_op

deleted theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_unop

deleted theorem CategoryTheory.MorphismProperty.FunctorsInverting.ext

deleted theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext

deleted def CategoryTheory.MorphismProperty.FunctorsInverting.mk

deleted def CategoryTheory.MorphismProperty.FunctorsInverting

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_subset_isomorphisms

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.leftOp

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.map_iff

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_subset

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.op

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.pi

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.prod

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.rightOp

deleted theorem CategoryTheory.MorphismProperty.IsInvertedBy.unop

deleted def CategoryTheory.MorphismProperty.IsInvertedBy

deleted theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_op

deleted theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_unop

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.lim_map

deleted def CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape

deleted theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.diagonal

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.epimorphisms

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.inverseImage

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.isomorphisms

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.monomorphisms

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.op

deleted theorem CategoryTheory.MorphismProperty.RespectsIso.unop

deleted def CategoryTheory.MorphismProperty.RespectsIso

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.fst

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.mk

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.op

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.respectsIso

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.snd

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.universally_eq

deleted theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.unop

deleted def CategoryTheory.MorphismProperty.StableUnderBaseChange

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.op

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.respectsIso

deleted theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.unop

deleted def CategoryTheory.MorphismProperty.StableUnderCobaseChange

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.diagonal

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.epimorphisms

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.inverseImage

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.isomorphisms

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.monomorphisms

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.op

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.universally

deleted theorem CategoryTheory.MorphismProperty.StableUnderComposition.unop

deleted def CategoryTheory.MorphismProperty.StableUnderComposition

deleted theorem CategoryTheory.MorphismProperty.StableUnderInverse.op

deleted theorem CategoryTheory.MorphismProperty.StableUnderInverse.unop

deleted def CategoryTheory.MorphismProperty.StableUnderInverse

deleted theorem CategoryTheory.MorphismProperty.bijective_eq_sup

deleted theorem CategoryTheory.MorphismProperty.bijective_respectsIso

deleted theorem CategoryTheory.MorphismProperty.bijective_stableUnderComposition

deleted theorem CategoryTheory.MorphismProperty.comp_mem

deleted def CategoryTheory.MorphismProperty.diagonal

deleted theorem CategoryTheory.MorphismProperty.diagonal_iff

deleted theorem CategoryTheory.MorphismProperty.epimorphisms.iff

deleted theorem CategoryTheory.MorphismProperty.epimorphisms.infer_property

deleted def CategoryTheory.MorphismProperty.epimorphisms

deleted theorem CategoryTheory.MorphismProperty.ext

deleted def CategoryTheory.MorphismProperty.functorCategory

deleted theorem CategoryTheory.MorphismProperty.id_mem

deleted theorem CategoryTheory.MorphismProperty.injective_respectsIso

deleted theorem CategoryTheory.MorphismProperty.injective_stableUnderComposition

deleted def CategoryTheory.MorphismProperty.inverseImage

deleted theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse

deleted theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor

deleted theorem CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence

deleted theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts

deleted def CategoryTheory.MorphismProperty.isoClosure

deleted theorem CategoryTheory.MorphismProperty.isoClosure_isoClosure

deleted theorem CategoryTheory.MorphismProperty.isoClosure_respectsIso

deleted theorem CategoryTheory.MorphismProperty.isoClosure_subset_iff

deleted theorem CategoryTheory.MorphismProperty.isomorphisms.iff

deleted theorem CategoryTheory.MorphismProperty.isomorphisms.infer_property

deleted def CategoryTheory.MorphismProperty.isomorphisms

deleted def CategoryTheory.MorphismProperty.map

deleted theorem CategoryTheory.MorphismProperty.map_eq_of_iso

deleted theorem CategoryTheory.MorphismProperty.map_id

deleted theorem CategoryTheory.MorphismProperty.map_id_eq_isoClosure

deleted theorem CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence

deleted theorem CategoryTheory.MorphismProperty.map_inverseImage_subset

deleted theorem CategoryTheory.MorphismProperty.map_isoClosure

deleted theorem CategoryTheory.MorphismProperty.map_map

deleted theorem CategoryTheory.MorphismProperty.map_mem_map

deleted theorem CategoryTheory.MorphismProperty.map_respectsIso

deleted theorem CategoryTheory.MorphismProperty.map_subset_iff

deleted theorem CategoryTheory.MorphismProperty.monomorphisms.iff

deleted theorem CategoryTheory.MorphismProperty.monomorphisms.infer_property

deleted def CategoryTheory.MorphismProperty.monomorphisms

deleted theorem CategoryTheory.MorphismProperty.monotone_isoClosure

deleted theorem CategoryTheory.MorphismProperty.monotone_map

deleted theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition

deleted theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse

deleted def CategoryTheory.MorphismProperty.naturalityProperty

deleted def CategoryTheory.MorphismProperty.op

deleted theorem CategoryTheory.MorphismProperty.op_unop

deleted def CategoryTheory.MorphismProperty.pi

deleted def CategoryTheory.MorphismProperty.prod

deleted theorem CategoryTheory.MorphismProperty.subset_iff_le

deleted theorem CategoryTheory.MorphismProperty.subset_isoClosure

deleted theorem CategoryTheory.MorphismProperty.surjective_respectsIso

deleted theorem CategoryTheory.MorphismProperty.surjective_stableUnderComposition

deleted theorem CategoryTheory.MorphismProperty.top_apply

deleted theorem CategoryTheory.MorphismProperty.top_eq

deleted def CategoryTheory.MorphismProperty.universally

deleted theorem CategoryTheory.MorphismProperty.universally_le

deleted theorem CategoryTheory.MorphismProperty.universally_mono

deleted theorem CategoryTheory.MorphismProperty.universally_respectsIso

deleted theorem CategoryTheory.MorphismProperty.universally_stableUnderBaseChange

deleted def CategoryTheory.MorphismProperty.unop

deleted theorem CategoryTheory.MorphismProperty.unop_op

deleted def CategoryTheory.MorphismProperty

deleted theorem CategoryTheory.NatTrans.isIso_app_iff_of_iso

Created Mathlib/CategoryTheory/MorphismProperty/Basic.lean

added theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_iso_iff

added theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff

added theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso

added theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso

added theorem CategoryTheory.MorphismProperty.RespectsIso.epimorphisms

added theorem CategoryTheory.MorphismProperty.RespectsIso.inverseImage

added theorem CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq

added theorem CategoryTheory.MorphismProperty.RespectsIso.isomorphisms

added theorem CategoryTheory.MorphismProperty.RespectsIso.monomorphisms

added theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso

added theorem CategoryTheory.MorphismProperty.RespectsIso.op

added theorem CategoryTheory.MorphismProperty.RespectsIso.unop

added def CategoryTheory.MorphismProperty.RespectsIso

added theorem CategoryTheory.MorphismProperty.epimorphisms.iff

added theorem CategoryTheory.MorphismProperty.epimorphisms.infer_property

added def CategoryTheory.MorphismProperty.epimorphisms

added theorem CategoryTheory.MorphismProperty.ext

added def CategoryTheory.MorphismProperty.functorCategory

added def CategoryTheory.MorphismProperty.inverseImage

added theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_functor_eq_map_inverse

added theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor

added theorem CategoryTheory.MorphismProperty.inverseImage_map_eq_of_isEquivalence

added def CategoryTheory.MorphismProperty.isoClosure

added theorem CategoryTheory.MorphismProperty.isoClosure_isoClosure

added theorem CategoryTheory.MorphismProperty.isoClosure_respectsIso

added theorem CategoryTheory.MorphismProperty.isoClosure_subset_iff

added theorem CategoryTheory.MorphismProperty.isomorphisms.iff

added theorem CategoryTheory.MorphismProperty.isomorphisms.infer_property

added def CategoryTheory.MorphismProperty.isomorphisms

added def CategoryTheory.MorphismProperty.map

added theorem CategoryTheory.MorphismProperty.map_eq_of_iso

added theorem CategoryTheory.MorphismProperty.map_id

added theorem CategoryTheory.MorphismProperty.map_id_eq_isoClosure

added theorem CategoryTheory.MorphismProperty.map_inverseImage_eq_of_isEquivalence

added theorem CategoryTheory.MorphismProperty.map_inverseImage_subset

added theorem CategoryTheory.MorphismProperty.map_isoClosure

added theorem CategoryTheory.MorphismProperty.map_map

added theorem CategoryTheory.MorphismProperty.map_mem_map

added theorem CategoryTheory.MorphismProperty.map_respectsIso

added theorem CategoryTheory.MorphismProperty.map_subset_iff

added theorem CategoryTheory.MorphismProperty.monomorphisms.iff

added theorem CategoryTheory.MorphismProperty.monomorphisms.infer_property

added def CategoryTheory.MorphismProperty.monomorphisms

added theorem CategoryTheory.MorphismProperty.monotone_isoClosure

added theorem CategoryTheory.MorphismProperty.monotone_map

added def CategoryTheory.MorphismProperty.op

added theorem CategoryTheory.MorphismProperty.op_unop

added def CategoryTheory.MorphismProperty.pi

added def CategoryTheory.MorphismProperty.prod

added theorem CategoryTheory.MorphismProperty.subset_iff_le

added theorem CategoryTheory.MorphismProperty.subset_isoClosure

added theorem CategoryTheory.MorphismProperty.top_apply

added theorem CategoryTheory.MorphismProperty.top_eq

added def CategoryTheory.MorphismProperty.unop

added theorem CategoryTheory.MorphismProperty.unop_op

added def CategoryTheory.MorphismProperty

added theorem CategoryTheory.NatTrans.isIso_app_iff_of_iso

Created Mathlib/CategoryTheory/MorphismProperty/Composition.lean

added theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_op

added theorem CategoryTheory.MorphismProperty.ContainsIdentities.of_unop

added theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_op

added theorem CategoryTheory.MorphismProperty.IsMultiplicative.of_unop

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.epimorphisms

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.inverseImage

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.isomorphisms

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.monomorphisms

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.op

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.respectsIso

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.unop

added def CategoryTheory.MorphismProperty.StableUnderComposition

added theorem CategoryTheory.MorphismProperty.StableUnderInverse.op

added theorem CategoryTheory.MorphismProperty.StableUnderInverse.unop

added def CategoryTheory.MorphismProperty.StableUnderInverse

added theorem CategoryTheory.MorphismProperty.comp_mem

added theorem CategoryTheory.MorphismProperty.id_mem

added theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition

added theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse

added def CategoryTheory.MorphismProperty.naturalityProperty

Created Mathlib/CategoryTheory/MorphismProperty/Concrete.lean

added theorem CategoryTheory.MorphismProperty.bijective_eq_sup

added theorem CategoryTheory.MorphismProperty.bijective_respectsIso

added theorem CategoryTheory.MorphismProperty.bijective_stableUnderComposition

added theorem CategoryTheory.MorphismProperty.injective_respectsIso

added theorem CategoryTheory.MorphismProperty.injective_stableUnderComposition

added theorem CategoryTheory.MorphismProperty.surjective_respectsIso

added theorem CategoryTheory.MorphismProperty.surjective_stableUnderComposition

Created Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean

added theorem CategoryTheory.MorphismProperty.FunctorsInverting.ext

added theorem CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext

added def CategoryTheory.MorphismProperty.FunctorsInverting.mk

added def CategoryTheory.MorphismProperty.FunctorsInverting

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_comp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_map_subset_isomorphisms

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.isoClosure_iff

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.leftOp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.map_iff

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_subset

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.op

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.pi

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.prod

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.rightOp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.unop

added def CategoryTheory.MorphismProperty.IsInvertedBy

Created Mathlib/CategoryTheory/MorphismProperty/Limits.lean

added theorem CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.lim_map

added def CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape

added theorem CategoryTheory.MorphismProperty.IsStableUnderProductsOfShape.mk

added theorem CategoryTheory.MorphismProperty.RespectsIso.diagonal

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_obj

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.diagonal

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.fst

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.mk

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.op

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.pullback_map

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.respectsIso

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.snd

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.universally_eq

added theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.unop

added def CategoryTheory.MorphismProperty.StableUnderBaseChange

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inl

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.inr

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.mk

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.op

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.respectsIso

added theorem CategoryTheory.MorphismProperty.StableUnderCobaseChange.unop

added def CategoryTheory.MorphismProperty.StableUnderCobaseChange

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.diagonal

added theorem CategoryTheory.MorphismProperty.StableUnderComposition.universally

added def CategoryTheory.MorphismProperty.diagonal

added theorem CategoryTheory.MorphismProperty.diagonal_iff

added theorem CategoryTheory.MorphismProperty.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts

added def CategoryTheory.MorphismProperty.universally

added theorem CategoryTheory.MorphismProperty.universally_le

added theorem CategoryTheory.MorphismProperty.universally_mono

added theorem CategoryTheory.MorphismProperty.universally_respectsIso

added theorem CategoryTheory.MorphismProperty.universally_stableUnderBaseChange

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean