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 x, 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 x, a b) :

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

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

    Makes the equivalence classes of an equivalence relation.

    Instances For
      theorem Setoid.mem_classes {α : Type u_1} (r : Setoid α) (y : α) :
      theorem Setoid.classes_ker_subset_fiber_set {α : Type u_1} {β : Type u_2} (f : αβ) :
      Setoid.classes (Setoid.ker f) Set.range fun y => {x | f x = y}
      theorem Setoid.finite_classes_ker {α : Type u_2} {β : Type u_3} [Finite β] (f : αβ) :
      theorem Setoid.card_classes_ker_le {α : Type u_2} {β : Type u_3} [Fintype β] (f : αβ) [Fintype ↑(Setoid.classes (Setoid.ker f))] :
      theorem Setoid.eq_iff_classes_eq {α : Type u_1} {r₁ : Setoid α} {r₂ : Setoid α} :
      r₁ = r₂ ∀ (x : α), {y | Setoid.Rel r₁ x y} = {y | Setoid.Rel r₂ 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 : α} :
      Setoid.Rel r x y c, c Setoid.classes r x c y c
      theorem Setoid.classes_inj {α : Type u_1} {r₁ : Setoid α} {r₂ : Setoid α} :
      r₁ = r₂ Setoid.classes r₁ = Setoid.classes r₂

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

      The empty set is not an equivalence class.

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

      Equivalence classes partition the type.

      theorem Setoid.eq_of_mem_classes {α : Type u_1} {r : Setoid α} {x : α} {b : Set α} (hc : b Setoid.classes r) (hb : x b) {b' : Set α} (hc' : b' Setoid.classes r) (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 x, a b) {s : Set α} {y : α} (hs : s c) (hy : y s) :
      s = {x | Setoid.Rel (Setoid.mkClasses c H) 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 x, a b) {y : α} :
      {x | Setoid.Rel (Setoid.mkClasses c H) 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 x, a b) {x : α} :
      {y | Setoid.Rel (Setoid.mkClasses c H) x y} c
      theorem Setoid.eqv_classes_disjoint {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b x, a b) :

      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 : Set.PairwiseDisjoint c id) (a : α) :
      ∃! b x, a b

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

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

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

      Instances For
        theorem Setoid.mkClasses_classes {α : Type u_1} (r : Setoid α) :
        Setoid.mkClasses (Setoid.classes r) (_ : ∀ (a : α), ∃! b x, a b) = 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 α) :
        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.

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

          A partition of α does not contain the empty set.

          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.Rel (Setoid.mkClasses c (_ : ∀ (a : α), ∃! b x, a b)) 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.classes (Setoid.mkClasses c (_ : ∀ (a : α), ∃! b x, a b)) = 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.

          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.

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

          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.

            def Setoid.IsPartition.finpartition {α : Type u_1} {c : Finset (Set α)} (hc : Setoid.IsPartition c) :
            Finpartition Set.univ

            A finite setoid partition furnishes a finpartition

            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)
              • 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 : ι), IndexedPartition.some s i s✝ i

                membership invariance for some

              • index : αι

                index for type α

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

                membership invariance for index

              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.

              Instances For
                noncomputable def IndexedPartition.mk' {ι : Type u_1} {α : Type u_2} (s : ιSet α) (dis : ∀ (i j : ι), i jDisjoint (s i) (s j)) (nonempty : ∀ (i : ι), Set.Nonempty (s i)) (ex : ∀ (x : α), i, x s i) :

                The non-constructive constructor for IndexedPartition.

                Instances For
                  instance IndexedPartition.instInhabitedIndexedPartitionUniv {ι : 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

                  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) {i : ι} {j : ι} :
                  i jDisjoint (s i) (s j)
                  theorem IndexedPartition.mem_iff_index_eq {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {x : α} {i : ι} :
                  theorem IndexedPartition.eq {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (i : ι) :
                  s i = {x | IndexedPartition.index hs x = i}
                  @[inline, reducible]
                  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.

                  Instances For
                    @[simp]
                    theorem IndexedPartition.index_some {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (i : ι) :
                    theorem IndexedPartition.some_index {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (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.

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

                      The projection onto the quotient associated to an indexed partition.

                      Instances For
                        theorem IndexedPartition.proj_eq_iff {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {x : α} {y : α} :
                        @[simp]
                        def IndexedPartition.equivQuotient {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :

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

                        Instances For
                          @[simp]
                          @[simp]
                          theorem IndexedPartition.equivQuotient_symm_proj_apply {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :
                          theorem IndexedPartition.equivQuotient_index {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :
                          def IndexedPartition.out {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) :

                          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.

                          Instances For
                            @[simp]
                            theorem IndexedPartition.out_proj {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : α) :

                            This lemma is analogous to Quotient.mk_out'.

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

                            This lemma is analogous to Quotient.out_eq'.

                            theorem IndexedPartition.class_of {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) {x : α} :
                            theorem IndexedPartition.proj_fiber {ι : Type u_1} {α : Type u_2} {s : ιSet α} (hs : IndexedPartition s) (x : IndexedPartition.Quotient hs) :