Documentation

Mathlib.Data.Setoid.Partition

Equivalence relations: partitions #

This file comprises properties of equivalence relations viewed as partitions. There are two implementations of partitions here:

Of course both implementations are related to Quotient and Setoid.

Setoid.isPartition.partition and Finpartition.isPartition_parts furnish a link between Setoid.IsPartition and Finpartition.

TODO #

Could the design of Finpartition inform the one of Setoid.IsPartition? Maybe bundling it and changing it from Set (Set α) to Set α where [Lattice α] [OrderBot α] would make it more usable.

Tags #

setoid, equivalence, iseqv, relation, equivalence relation, partition, equivalence class

theorem Setoid.eq_of_mem_eqv_class {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b : Set α, b c a b) {x : α} {b : Set α} {b' : Set α} (hc : b c) (hb : x b) (hc' : b' c) (hb' : x b') :
b = b'

If x ∈ α is in 2 elements of a set of sets partitioning α, those 2 sets are equal.

def Setoid.mkClasses {α : Type u_1} (c : Set (Set α)) (H : ∀ (a : α), ∃! b : Set α, b c a b) :

Makes an equivalence relation from a set of sets partitioning α.

Equations
Instances For
    def Setoid.classes {α : Type u_1} (r : Setoid α) :
    Set (Set α)

    Makes the equivalence classes of an equivalence relation.

    Equations
    • r.classes = {s : Set α | ∃ (y : α), s = {x : α | r.Rel x y}}
    Instances For
      theorem Setoid.mem_classes {α : Type u_1} (r : Setoid α) (y : α) :
      {x : α | r.Rel x y} r.classes
      theorem Setoid.classes_ker_subset_fiber_set {α : Type u_1} {β : Type u_2} (f : αβ) :
      (Setoid.ker f).classes Set.range fun (y : β) => {x : α | f x = y}
      theorem Setoid.finite_classes_ker {α : Type u_2} {β : Type u_3} [Finite β] (f : αβ) :
      (Setoid.ker f).classes.Finite
      theorem Setoid.card_classes_ker_le {α : Type u_2} {β : Type u_3} [Fintype β] (f : αβ) [Fintype (Setoid.ker f).classes] :
      theorem Setoid.eq_iff_classes_eq {α : Type u_1} {r₁ : Setoid α} {r₂ : Setoid α} :
      r₁ = r₂ ∀ (x : α), {y : α | r₁.Rel x y} = {y : α | r₂.Rel x y}

      Two equivalence relations are equal iff all their equivalence classes are equal.

      theorem Setoid.rel_iff_exists_classes {α : Type u_1} (r : Setoid α) {x : α} {y : α} :
      r.Rel x y cr.classes, x c y c
      theorem Setoid.classes_inj {α : Type u_1} {r₁ : Setoid α} {r₂ : Setoid α} :
      r₁ = r₂ r₁.classes = r₂.classes

      Two equivalence relations are equal iff their equivalence classes are equal.

      theorem Setoid.empty_not_mem_classes {α : Type u_1} {r : Setoid α} :
      r.classes

      The empty set is not an equivalence class.

      theorem Setoid.classes_eqv_classes {α : Type u_1} {r : Setoid α} (a : α) :
      ∃! b : Set α, b r.classes a b

      Equivalence classes partition the type.

      theorem Setoid.eq_of_mem_classes {α : Type u_1} {r : Setoid α} {x : α} {b : Set α} (hc : b r.classes) (hb : x b) {b' : Set α} (hc' : b' r.classes) (hb' : x b') :
      b = b'

      If x ∈ α is in 2 equivalence classes, the equivalence classes are equal.

      theorem Setoid.eq_eqv_class_of_mem {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b : Set α, b c a b) {s : Set α} {y : α} (hs : s c) (hy : y s) :
      s = {x : α | (Setoid.mkClasses c H).Rel x y}

      The elements of a set of sets partitioning α are the equivalence classes of the equivalence relation defined by the set of sets.

      theorem Setoid.eqv_class_mem {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b : Set α, b c a b) {y : α} :
      {x : α | (Setoid.mkClasses c H).Rel x y} c

      The equivalence classes of the equivalence relation defined by a set of sets partitioning α are elements of the set of sets.

      theorem Setoid.eqv_class_mem' {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b : Set α, b c a b) {x : α} :
      {y : α | (Setoid.mkClasses c H).Rel x y} c
      theorem Setoid.eqv_classes_disjoint {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b : Set α, b c a b) :
      c.PairwiseDisjoint id

      Distinct elements of a set of sets partitioning α are disjoint.

      theorem Setoid.eqv_classes_of_disjoint_union {α : Type u_1} {c : Set (Set α)} (hu : ⋃₀ c = Set.univ) (H : c.PairwiseDisjoint id) (a : α) :
      ∃! b : Set α, b c a b

      A set of disjoint sets covering α partition α (classical).

      def Setoid.setoidOfDisjointUnion {α : Type u_1} {c : Set (Set α)} (hu : ⋃₀ c = Set.univ) (H : c.PairwiseDisjoint id) :

      Makes an equivalence relation from a set of disjoints sets covering α.

      Equations
      Instances For
        theorem Setoid.mkClasses_classes {α : Type u_1} (r : Setoid α) :
        Setoid.mkClasses r.classes = r

        The equivalence relation made from the equivalence classes of an equivalence relation r equals r.

        @[simp]
        theorem Setoid.sUnion_classes {α : Type u_1} (r : Setoid α) :
        ⋃₀ r.classes = Set.univ
        noncomputable def Setoid.quotientEquivClasses {α : Type u_1} (r : Setoid α) :
        Quotient r r.classes

        The equivalence between the quotient by an equivalence relation and its type of equivalence classes.

        Equations
        • r.quotientEquivClasses = let f := fun (a : α) => {x : α | Setoid.r x a}, ; let_fun f_respects_relation := ; Equiv.ofBijective (Quot.lift f f_respects_relation)
        Instances For
          @[simp]
          theorem Setoid.quotientEquivClasses_mk_eq {α : Type u_1} (r : Setoid α) (a : α) :
          (r.quotientEquivClasses a) = {x : α | r.Rel x a}
          def Setoid.IsPartition {α : Type u_1} (c : Set (Set α)) :

          A collection c : Set (Set α) of sets is a partition of α into pairwise disjoint sets if ∅ ∉ c and each element a : α belongs to a unique set b ∈ c.

          Equations
          Instances For
            theorem Setoid.nonempty_of_mem_partition {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) {s : Set α} (h : s c) :
            s.Nonempty

            A partition of α does not contain the empty set.

            theorem Setoid.isPartition_classes {α : Type u_1} (r : Setoid α) :
            theorem Setoid.IsPartition.pairwiseDisjoint {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) :
            c.PairwiseDisjoint id
            theorem Set.PairwiseDisjoint.isPartition_of_exists_of_ne_empty {α : Type u_2} {s : Set (Set α)} (h₁ : s.PairwiseDisjoint id) (h₂ : ∀ (a : α), xs, a x) (h₃ : s) :
            theorem Setoid.IsPartition.sUnion_eq_univ {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) :
            ⋃₀ c = Set.univ
            theorem Setoid.exists_of_mem_partition {α : Type u_1} {c : Set (Set α)} (hc : Setoid.IsPartition c) {s : Set α} (hs : s c) :
            ∃ (y : α), s = {x : α | (Setoid.mkClasses c ).Rel x y}

            All elements of a partition of α are the equivalence class of some y ∈ α.

            theorem Setoid.classes_mkClasses {α : Type u_1} (c : Set (Set α)) (hc : Setoid.IsPartition c) :
            (Setoid.mkClasses c ).classes = c

            The equivalence classes of the equivalence relation defined by a partition of α equal the original partition.

            instance Setoid.Partition.le {α : Type u_1} :
            LE (Subtype Setoid.IsPartition)

            Defining on partitions as the defined on their induced equivalence relations.

            Equations
            instance Setoid.Partition.partialOrder {α : Type u_1} :
            PartialOrder (Subtype Setoid.IsPartition)

            Defining a partial order on partitions as the partial order on their induced equivalence relations.

            Equations
            def Setoid.Partition.orderIso (α : Type u_1) :
            Setoid α ≃o { C : Set (Set α) // Setoid.IsPartition C }

            The order-preserving bijection between equivalence relations on a type α, and partitions of α into subsets.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance Setoid.Partition.completeLattice {α : Type u_1} :
              CompleteLattice (Subtype Setoid.IsPartition)

              A complete lattice instance for partitions; there is more infrastructure for the equivalent complete lattice on equivalence relations.

              Equations
              @[simp]
              theorem Setoid.IsPartition.finpartition_parts {α : Type u_1} {c : Finset (Set α)} (hc : Setoid.IsPartition c) :
              hc.finpartition.parts = c
              def Setoid.IsPartition.finpartition {α : Type u_1} {c : Finset (Set α)} (hc : Setoid.IsPartition c) :
              Finpartition Set.univ

              A finite setoid partition furnishes a finpartition

              Equations
              • hc.finpartition = { parts := c, supIndep := , sup_parts := , not_bot_mem := }
              Instances For
                theorem Finpartition.isPartition_parts {α : Type u_1} (f : Finpartition Set.univ) :

                A finpartition gives rise to a setoid partition

                structure IndexedPartition {ι : Type u_1} {α : Type u_2} (s : ιSet α) :
                Type (max u_1 u_2)

                Constructive information associated with a partition of a type α indexed by another type ι, s : ι → Set α.

                IndexedPartition.index sends an element to its index, while IndexedPartition.some sends an index to an element of the corresponding set.

                This type is primarily useful for definitional control of s - if this is not needed, then Setoid.ker index by itself may be sufficient.

                • eq_of_mem : ∀ {x : α} {i j : ι}, x s ix s ji = j

                  two indexes are equal if they are equal in membership

                • some : ια

                  sends an index to an element of the corresponding set

                • some_mem : ∀ (i : ι), self.some i s i

                  membership invariance for some

                • index : αι

                  index for type α

                • mem_index : ∀ (x : α), x s (self.index x)

                  membership invariance for index

                Instances For
                  theorem IndexedPartition.eq_of_mem {ι : Type u_1} {α : Type u_2} {s : ιSet α} (self : IndexedPartition s) {x : α} {i : ι} {j : ι} :
                  x s ix s ji = j

                  two indexes are equal if they are equal in membership

                  @[simp]
                  theorem IndexedPartition.some_mem {ι : Type u_1} {α : Type u_2} {s : ιSet α} (self : IndexedPartition s) (i : ι) :
                  self.some i s i

                  membership invariance for some

                  theorem IndexedPartition.mem_index {ι : Type u_1} {α : Type u_2} {s : ιSet α} (self : IndexedPartition s) (x : α) :
                  x s (self.index x)

                  membership invariance for index

                  noncomputable def IndexedPartition.mk' {ι : Type u_1} {α : Type u_2} (s : ιSet α) (dis : Pairwise fun (i j : ι) => Disjoint (s i) (s j)) (nonempty : ∀ (i : ι), (s i).Nonempty) (ex : ∀ (x : α), ∃ (i : ι), x s i) :

                  The non-constructive constructor for IndexedPartition.

                  Equations
                  • IndexedPartition.mk' s dis nonempty ex = { eq_of_mem := , some := fun (i : ι) => .some, some_mem := , index := fun (x : α) => .choose, mem_index := }
                  Instances For
                    instance IndexedPartition.instInhabitedUnivOfUnique {ι : Type u_1} {α : Type u_2} [Unique ι] [Inhabited α] :
                    Inhabited (IndexedPartition fun (_i : ι) => Set.univ)

                    On a unique index set there is the obvious trivial partition

                    Equations
                    • IndexedPartition.instInhabitedUnivOfUnique = { default := { eq_of_mem := , some := default, some_mem := , index := default, mem_index := } }
                    theorem IndexedPartition.exists_mem {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                    ∃ (i : ι), x s i
                    theorem IndexedPartition.iUnion {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                    ⋃ (i : ι), s i = Set.univ
                    theorem IndexedPartition.disjoint {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                    Pairwise fun (i j : ι) => Disjoint (s i) (s j)
                    theorem IndexedPartition.mem_iff_index_eq {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {x : α} {i : ι} :
                    x s i hs.index x = i
                    theorem IndexedPartition.eq {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (i : ι) :
                    s i = {x : α | hs.index x = i}
                    @[reducible, inline]
                    abbrev IndexedPartition.setoid {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :

                    The equivalence relation associated to an indexed partition. Two elements are equivalent if they belong to the same set of the partition.

                    Equations
                    Instances For
                      @[simp]
                      theorem IndexedPartition.index_some {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (i : ι) :
                      hs.index (hs.some i) = i
                      theorem IndexedPartition.some_index {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                      hs.setoid.Rel (hs.some (hs.index x)) x
                      def IndexedPartition.Quotient {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                      Type u_2

                      The quotient associated to an indexed partition.

                      Equations
                      Instances For
                        def IndexedPartition.proj {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                        αhs.Quotient

                        The projection onto the quotient associated to an indexed partition.

                        Equations
                        • hs.proj = Quotient.mk''
                        Instances For
                          instance IndexedPartition.instInhabitedQuotient {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) [Inhabited α] :
                          Inhabited hs.Quotient
                          Equations
                          • hs.instInhabitedQuotient = { default := hs.proj default }
                          theorem IndexedPartition.proj_eq_iff {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {x : α} {y : α} :
                          hs.proj x = hs.proj y hs.index x = hs.index y
                          @[simp]
                          theorem IndexedPartition.proj_some_index {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                          hs.proj (hs.some (hs.index x)) = hs.proj x
                          def IndexedPartition.equivQuotient {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                          ι hs.Quotient

                          The obvious equivalence between the quotient associated to an indexed partition and the indexing type.

                          Equations
                          Instances For
                            @[simp]
                            theorem IndexedPartition.equivQuotient_index_apply {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                            hs.equivQuotient (hs.index x) = hs.proj x
                            @[simp]
                            theorem IndexedPartition.equivQuotient_symm_proj_apply {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                            hs.equivQuotient.symm (hs.proj x) = hs.index x
                            theorem IndexedPartition.equivQuotient_index {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                            hs.equivQuotient hs.index = hs.proj
                            def IndexedPartition.out {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                            hs.Quotient α

                            A map choosing a representative for each element of the quotient associated to an indexed partition. This is a computable version of Quotient.out' using IndexedPartition.some.

                            Equations
                            • hs.out = hs.equivQuotient.symm.toEmbedding.trans { toFun := hs.some, inj' := }
                            Instances For
                              @[simp]
                              theorem IndexedPartition.out_proj {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                              hs.out (hs.proj x) = hs.some (hs.index x)

                              This lemma is analogous to Quotient.mk_out'.

                              theorem IndexedPartition.index_out' {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : hs.Quotient) :
                              hs.index (Quotient.out' x) = hs.index (hs.out x)

                              The indices of Quotient.out' and IndexedPartition.out are equal.

                              @[simp]
                              theorem IndexedPartition.proj_out {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : hs.Quotient) :
                              hs.proj (hs.out x) = x

                              This lemma is analogous to Quotient.out_eq'.

                              theorem IndexedPartition.class_of {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {x : α} :
                              setOf (hs.setoid.Rel x) = s (hs.index x)
                              theorem IndexedPartition.proj_fiber {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : hs.Quotient) :
                              hs.proj ⁻¹' {x} = s (hs.equivQuotient.symm x)
                              def IndexedPartition.piecewise {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {β : Type u_3} (f : ιαβ) :
                              αβ

                              Combine functions with disjoint domains into a new function. You can use the regular expression def.*piecewise to search for other ways to define piecewise functions in mathlib4.

                              Equations
                              • hs.piecewise f x = f (hs.index x) x
                              Instances For
                                theorem IndexedPartition.piecewise_apply {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {β : Type u_3} {f : ιαβ} (x : α) :
                                hs.piecewise f x = f (hs.index x) x
                                theorem IndexedPartition.piecewise_inj {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {β : Type u_3} {f : ιαβ} (h_injOn : ∀ (i : ι), Set.InjOn (f i) (s i)) (h_disjoint : Set.univ.PairwiseDisjoint fun (i : ι) => f i '' s i) :
                                Function.Injective (hs.piecewise f)

                                A family of injective functions with pairwise disjoint domains and pairwise disjoint ranges can be glued together to form an injective function.

                                theorem IndexedPartition.piecewise_bij {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {β : Type u_3} {f : ιαβ} {t : ιSet β} (ht : IndexedPartition t) (hf : ∀ (i : ι), Set.BijOn (f i) (s i) (t i)) :
                                Function.Bijective (hs.piecewise f)

                                A family of bijective functions with pairwise disjoint domains and pairwise disjoint ranges can be glued together to form a bijective function.