Magnitude conjecture

QuotientSubmoduleEquidistribution.CategoryTheory.Rejective

Rejective full subcategories and equivalence transport #

Rejectivity itself is purely categorical. No zero object, additive structure, kernels, cokernels, or module structure enters its definition or its invariance under equivalence.

source
structure QuotientSubmoduleEquidistribution.CategoricalRejective.RightRejectiveData {C : Type uC} [CategoryTheory.Category.{vC, uC} C] (P : CategoryTheory.ObjectProperty C) :
Type (max uC vC)

A full subcategory is right rejective when its inclusion has a right adjoint with componentwise monic counit.

  • coreflector : CategoryTheory.Functor C P.FullSubcategory
  • adjunction : P.ι ⊣ self.coreflector
  • counit_mono (X : C) : CategoryTheory.Mono (self.adjunction.counit.app X)
Instances For
    source
    def QuotientSubmoduleEquidistribution.CategoricalRejective.IsRightRejective {C : Type uC} [CategoryTheory.Category.{vC, uC} C] (P : CategoryTheory.ObjectProperty C) :
    Prop

    Propositional form of categorical right rejectivity.

    Instances For
      source
      structure QuotientSubmoduleEquidistribution.CategoricalRejective.LeftRejectiveData {C : Type uC} [CategoryTheory.Category.{vC, uC} C] (P : CategoryTheory.ObjectProperty C) :
      Type (max uC vC)

      A full subcategory is left rejective when its inclusion has a left adjoint with componentwise epic unit.

      • reflector : CategoryTheory.Functor C P.FullSubcategory
      • adjunction : self.reflector ⊣ P.ι
      • unit_epi (X : C) : CategoryTheory.Epi (self.adjunction.unit.app X)
      Instances For
        source
        def QuotientSubmoduleEquidistribution.CategoricalRejective.IsLeftRejective {C : Type uC} [CategoryTheory.Category.{vC, uC} C] (P : CategoryTheory.ObjectProperty C) :
        Prop

        Propositional form of categorical left rejectivity.

        Instances For
          source
          def QuotientSubmoduleEquidistribution.CategoricalRejective.imageProperty {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) :
          CategoryTheory.ObjectProperty D

          The replete image predicate on the target of an equivalence, expressed as pullback along its chosen inverse.

          Instances For
            source
            instance QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.instIsClosedUnderIsomorphismsImageProperty {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
            (imageProperty E P).IsClosedUnderIsomorphisms
            source
            def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.inverseLift {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) :
            CategoryTheory.Functor (imageProperty E P).FullSubcategory P.FullSubcategory

            Restriction of the inverse equivalence functor to the pulled-back object property.

            Instances For
              source
              def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.forwardLift {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
              CategoryTheory.Functor P.FullSubcategory (imageProperty E P).FullSubcategory

              Restriction of the forward equivalence functor. Repleteness of P supplies membership after applying the unit isomorphism.

              Instances For
                source
                def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.restrictedUnitIso {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                CategoryTheory.Functor.id P.FullSubcategory ≅ (forwardLift E P).comp (inverseLift E P)

                The unit of the ambient equivalence restricted to the full subcategories.

                Instances For
                  source
                  def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.restrictedCounitIso {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                  (inverseLift E P).comp (forwardLift E P) ≅ CategoryTheory.Functor.id (imageProperty E P).FullSubcategory

                  The counit of the ambient equivalence restricted to the full subcategories.

                  Instances For
                    source
                    def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.restricted {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                    P.FullSubcategory ≌ (imageProperty E P).FullSubcategory

                    The equivalence induced on a replete full subcategory.

                    Instances For
                      source
                      def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.inverseLiftCompInclusionCompFunctorIso {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                      (restricted E P).inverse.comp (P.ι.comp E.functor) ≅ (imageProperty E P).ι

                      The composite of the transported source inclusion with the ambient equivalence is canonically the target inclusion.

                      Instances For
                        source
                        def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportedCoreflector {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : RightRejectiveData P) :
                        CategoryTheory.Functor D (imageProperty E P).FullSubcategory

                        The transported right adjoint.

                        Instances For
                          source
                          def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportedRightAdjunction {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : RightRejectiveData P) :
                          (imageProperty E P).ι ⊣ transportedCoreflector E P data

                          The composite adjunction, with its left adjoint normalized back to the literal inclusion of the transported full subcategory.

                          Instances For
                            source
                            def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportedReflector {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : LeftRejectiveData P) :
                            CategoryTheory.Functor D (imageProperty E P).FullSubcategory

                            The transported left adjoint.

                            Instances For
                              source
                              def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportedLeftAdjunction {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : LeftRejectiveData P) :
                              transportedReflector E P data ⊣ (imageProperty E P).ι

                              The composite left-rejective adjunction, with its right adjoint normalized to the target inclusion.

                              Instances For
                                source
                                theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportedRightAdjunction_counit_mono {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : RightRejectiveData P) (X : D) :
                                CategoryTheory.Mono ((transportedRightAdjunction E P data).counit.app X)

                                The transported counit is monic. The proof separates the two composed adjunctions and the final normalization isomorphism, so typeclass search only sees composites of mapped monomorphisms and isomorphisms.

                                source
                                theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportedLeftAdjunction_unit_epi {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : LeftRejectiveData P) (X : D) :
                                CategoryTheory.Epi ((transportedLeftAdjunction E P data).unit.app X)

                                The transported unit is epic, by the dual componentwise argument.

                                source
                                def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportRightRejectiveData {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : RightRejectiveData P) :
                                RightRejectiveData (imageProperty E P)

                                Right rejective data transports along a categorical equivalence.

                                Instances For
                                  source
                                  def QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.transportLeftRejectiveData {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (data : LeftRejectiveData P) :
                                  LeftRejectiveData (imageProperty E P)

                                  Left rejective data transports along a categorical equivalence.

                                  Instances For
                                    source
                                    theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.isRightRejective_image {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (h : IsRightRejective P) :
                                    IsRightRejective (imageProperty E P)

                                    Right rejectivity transports in the forward direction.

                                    source
                                    theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.isLeftRejective_image {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] (h : IsLeftRejective P) :
                                    IsLeftRejective (imageProperty E P)

                                    Left rejectivity transports in the forward direction.

                                    source
                                    theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.imageProperty_symm_imageProperty_eq {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                                    imageProperty E.symm (imageProperty E P) = P

                                    Pulling the image predicate back through the inverse equivalence recovers the original predicate. Repleteness is the only input.

                                    source
                                    theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.isRightRejective_iff_image {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                                    IsRightRejective P ↔ IsRightRejective (imageProperty E P)

                                    Right rejectivity is invariant under categorical equivalence.

                                    source
                                    theorem QuotientSubmoduleEquidistribution.CategoricalRejective.Equivalence.isLeftRejective_iff_image {C : Type uC} [CategoryTheory.Category.{vC, uC} C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] (E : C ≌ D) (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] :
                                    IsLeftRejective P ↔ IsLeftRejective (imageProperty E P)

                                    Left rejectivity is invariant under categorical equivalence.