Commit 2023-03-24 17:17 cf80a760

View on Github →

feat: port CategoryTheory.MorphismProperty (#2909)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/MorphismProperty.lean

added def CategoryTheory.MorphismProperty.FunctorsInverting.mk

added def CategoryTheory.MorphismProperty.FunctorsInverting

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.iff_of_iso

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.leftOp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.of_comp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.op

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.rightOp

added theorem CategoryTheory.MorphismProperty.IsInvertedBy.unop

added def CategoryTheory.MorphismProperty.IsInvertedBy

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.diagonal

added theorem CategoryTheory.MorphismProperty.RespectsIso.epimorphisms

added theorem CategoryTheory.MorphismProperty.RespectsIso.inverseImage

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.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.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.universally

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.bijective_eq_sup

added theorem CategoryTheory.MorphismProperty.bijective_respectsIso

added theorem CategoryTheory.MorphismProperty.bijective_stableUnderComposition

added def CategoryTheory.MorphismProperty.diagonal

added theorem CategoryTheory.MorphismProperty.diagonal_iff

added theorem CategoryTheory.MorphismProperty.epimorphisms.iff

added theorem CategoryTheory.MorphismProperty.epimorphisms.infer_property

added def CategoryTheory.MorphismProperty.epimorphisms

added theorem CategoryTheory.MorphismProperty.injective_respectsIso

added theorem CategoryTheory.MorphismProperty.injective_stableUnderComposition

added def CategoryTheory.MorphismProperty.inverseImage

added theorem CategoryTheory.MorphismProperty.isomorphisms.iff

added theorem CategoryTheory.MorphismProperty.isomorphisms.infer_property

added def CategoryTheory.MorphismProperty.isomorphisms

added theorem CategoryTheory.MorphismProperty.monomorphisms.iff

added theorem CategoryTheory.MorphismProperty.monomorphisms.infer_property

added def CategoryTheory.MorphismProperty.monomorphisms

added theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderComposition

added theorem CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse

added def CategoryTheory.MorphismProperty.naturalityProperty

added def CategoryTheory.MorphismProperty.op

added theorem CategoryTheory.MorphismProperty.op_unop

added theorem CategoryTheory.MorphismProperty.surjective_respectsIso

added theorem CategoryTheory.MorphismProperty.surjective_stableUnderComposition

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

added def CategoryTheory.MorphismProperty.unop

added theorem CategoryTheory.MorphismProperty.unop_op

added def CategoryTheory.MorphismProperty