Magnitude conjecture

QuotientSubmoduleEquidistribution.ConvexGeometry.Relabeling

Relabeling a closure system #

This is the closure-theoretic target of either a Morita equivalence or finite-dimensional vector-space duality. The categorical work only has to produce map_closure; all lattice and level-polynomial consequences are then formal.

source
def QuotientSubmoduleEquidistribution.SetClosure.transport {E : Type u} {F : Type v} (c : SetClosure E) (e : E ≃ F) :
SetClosure F

Transport a closure operator across an equivalence of its ground type.

Instances For
    source
    @[simp]
    theorem QuotientSubmoduleEquidistribution.SetClosure.transport_refl {E : Type u} (c : SetClosure E) :
    c.transport (Equiv.refl E) = c
    source
    structure QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv {E : Type u} {F : Type v} (c : SetClosure E) (d : SetClosure F) :
    Type (max u v)

    An equivalence of ground labels which conjugates two closure operators.

    • equiv : E ≃ F
    • map_closure (S : Set E) : ⇑self.equiv '' c S = d (⇑self.equiv '' S)
    Instances For
      source
      def QuotientSubmoduleEquidistribution.SetClosure.transportRelabeling {E : Type u} {F : Type v} (c : SetClosure E) (e : E ≃ F) :
      c.RelabelingEquiv (c.transport e)

      The canonical relabeling from a closure operator to its transport.

      Instances For
        source
        def QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv.mapClosed {E : Type u} {F : Type v} {c : SetClosure E} {d : SetClosure F} (h : c.RelabelingEquiv d) (C : ClosureOperator.Closeds c) :
        ClosureOperator.Closeds d

        A closed set remains closed after relabeling.

        Instances For
          source
          def QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv.invClosed {E : Type u} {F : Type v} {c : SetClosure E} {d : SetClosure F} (h : c.RelabelingEquiv d) (D : ClosureOperator.Closeds d) :
          ClosureOperator.Closeds c

          A closed set can be pulled back along the relabeling.

          Instances For
            source
            def QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv.closedsOrderIso {E : Type u} {F : Type v} {c : SetClosure E} {d : SetClosure F} (h : c.RelabelingEquiv d) :
            ClosureOperator.Closeds c ≃o ClosureOperator.Closeds d

            Conjugate closure systems have order-isomorphic lattices of closed sets.

            Instances For
              source
              @[simp]
              theorem QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv.coe_closedsOrderIso_apply {E : Type u} {F : Type v} {c : SetClosure E} {d : SetClosure F} (h : c.RelabelingEquiv d) (C : ClosureOperator.Closeds c) :
              ↑(h.closedsOrderIso C) = ⇑h.equiv '' ↑C
              source
              @[simp]
              theorem QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv.ncard_closedsOrderIso_apply {E : Type u} {F : Type v} {c : SetClosure E} {d : SetClosure F} (h : c.RelabelingEquiv d) (C : ClosureOperator.Closeds c) :
              (↑(h.closedsOrderIso C)).ncard = (↑C).ncard

              Relabeling preserves the cardinality of every closed set.

              source
              theorem QuotientSubmoduleEquidistribution.SetClosure.RelabelingEquiv.levelPolynomial_eq {E : Type u} {F : Type v} {c : SetClosure E} {d : SetClosure F} (h : c.RelabelingEquiv d) [Finite E] [Finite F] :
              c.levelPolynomial = d.levelPolynomial

              Relabeling preserves the level-generating polynomial.