Commit 2023-03-24 20:19 a5694618

View on Github →

feat: port CategoryTheory.Localization.Construction (#2917)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Localization/Construction.lean

added structure CategoryTheory.Localization.Construction.LocQuiver

added def CategoryTheory.Localization.Construction.NatTransExtension.app

added theorem CategoryTheory.Localization.Construction.NatTransExtension.app_eq

added def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso

added def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor

added def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse

added def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso

added theorem CategoryTheory.Localization.Construction.fac

added def CategoryTheory.Localization.Construction.lift

added def CategoryTheory.Localization.Construction.liftToPathCategory

added theorem CategoryTheory.Localization.Construction.morphismProperty_is_top'

added theorem CategoryTheory.Localization.Construction.morphismProperty_is_top

added def CategoryTheory.Localization.Construction.natTransExtension

added theorem CategoryTheory.Localization.Construction.natTransExtension_hcomp

added theorem CategoryTheory.Localization.Construction.natTrans_hcomp_injective

added def CategoryTheory.Localization.Construction.objEquiv

added inductive CategoryTheory.Localization.Construction.relations

added theorem CategoryTheory.Localization.Construction.uniq

added def CategoryTheory.Localization.Construction.wIso

added def CategoryTheory.Localization.Construction.whiskeringLeftEquivalence

added def CategoryTheory.Localization.Construction.ιPaths

added def CategoryTheory.Localization.Construction.ψ₁

added def CategoryTheory.Localization.Construction.ψ₂

added def CategoryTheory.MorphismProperty.Localization

added def CategoryTheory.MorphismProperty.Q

added theorem CategoryTheory.MorphismProperty.Q_inverts

Modified Mathlib/CategoryTheory/MorphismProperty.lean

added theorem CategoryTheory.MorphismProperty.FunctorsInverting.ext

added theorem CategoryTheory.MorphismProperty.top_apply

added theorem CategoryTheory.MorphismProperty.top_eq

Modified Mathlib/CategoryTheory/Quotient.lean