Typeclass for types with a set-like extensionality property

The Membership typeclass is used to let terms of a type have elements. Many instances of Membership have a set-like extensionality property: things are equal iff they have the same elements. The SetLike typeclass provides a unified interface to define a Membership that is extensional in this way.

The main use of SetLike is for algebraic subobjects (such as Submonoid and Submodule), whose non-proof data consists only of a carrier set. In such a situation, the projection to the carrier set is injective.

In general, a type A is SetLike with elements of type B if it has an injective map to Set B. This module provides standard boilerplate for every SetLike: a coe_sort, a coe to set, a PartialOrder, and various extensionality and simp lemmas.

A typical subobject should be declared as:

structure MySubobject (X : Type*) [ObjectTypeclass X] :=
  (carrier : Set X)
  (op_mem' : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)

namespace MySubobject

variable {X : Type*} [ObjectTypeclass X] {x : X}

instance : SetLike (MySubobject X) X :=
  ⟨MySubobject.carrier, fun p q h => by cases p; cases q; congr!⟩

@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl

@[ext] theorem ext {p q : MySubobject X} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q := SetLike.ext h

/-- Copy of a `MySubobject` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. See Note [range copy pattern]. -/
protected def copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) : MySubobject X :=
  { carrier := s
    op_mem' := hs.symm ▸ p.op_mem' }

@[simp] lemma coe_copy (p : MySubobject X) (s : Set X) (hs : s = ↑p) :
  (p.copy s hs : Set X) = s := rfl

lemma copy_eq (p : MySubobject X) (s : Set X) (hs : s = ↑p) : p.copy s hs = p :=
  SetLike.coe_injective hs

end MySubobject

An alternative to SetLike could have been an extensional Membership typeclass:

class ExtMembership (α : out_param <| Type u) (β : Type v) extends Membership α β :=
  (ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)

While this is equivalent, SetLike conveniently uses a carrier set projection directly.

Tags

subobjects

class SetLike (A : Type u_1) (B : outParam (Type u_2)) : Type (max u_1 u_2)

A class to indicate that there is a canonical injection between A and Set B.

This has the effect of giving terms of A elements of type B (through a Membership instance) and a compatible coercion to Type* as a subtype.

Note: if SetLike.coe is a projection, implementers should create a simp lemma such as

@[simp] lemma mem_carrier {p : MySubobject X} : x ∈ p.carrier ↔ x ∈ (p : Set X) := Iff.rfl

to normalize terms.

If you declare an unbundled subclass of SetLike, for example:

class MulMemClass (S : Type*) (M : Type*) [Mul M] [SetLike S M] where
  ...

Then you should not repeat the outParam declaration so SetLike will supply the value instead. This ensures your subclass will not have issues with synthesis of the [Mul M] parameter starting before the value of M is known.

• coe : A → Set B

  The coercion from a term of a SetLike to its corresponding Set.

• coe_injective' : Function.Injective SetLike.coe

  The coercion from a term of a SetLike to its corresponding Set is injective.

theorem SetLike.coe_injective' {A : Type u_1} {B : outParam (Type u_2)} [self : SetLike A B] : Function.Injective SetLike.coe

The coercion from a term of a SetLike to its corresponding Set is injective.

instance SetLike.instCoeTCSet {A : Type u_1} {B : Type u_2} [i : SetLike A B] : CoeTC A (Set B)

Equations

• SetLike.instCoeTCSet = { coe := SetLike.coe }

@[instance 100]

instance SetLike.instMembership {A : Type u_1} {B : Type u_2} [i : SetLike A B] : Membership B A

Equations

• SetLike.instMembership = { mem := fun (p : A) (x : B) => x ∈ ↑p }

@[instance 100]

instance SetLike.instCoeSortType {A : Type u_1} {B : Type u_2} [i : SetLike A B] : CoeSort A (Type u_2)

Equations

• SetLike.instCoeSortType = { coe := fun (p : A) => { x : B // x ∈ p } }

def SetLike.delabSubtypeSetLike : Lean.PrettyPrinter.Delaborator.Delab

For terms that match the CoeSort instance's body, pretty print as ↥S rather than as { x // x ∈ S }. The discriminating feature is that membership uses the SetLike.instMembership instance.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SetLike.coe_sort_coe {A : Type u_1} {B : Type u_2} [i : SetLike A B] (p : A) : ↑↑p = { x : B // x ∈ p }

theorem SetLike.exists {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : { x : B // x ∈ p } → Prop} : (∃ (x : { x : B // x ∈ p }), q x) ↔ ∃ (x : B) (h : x ∈ p), q ⟨x, h⟩

theorem SetLike.forall {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : { x : B // x ∈ p } → Prop} : (∀ (x : { x : B // x ∈ p }), q x) ↔ ∀ (x : B) (h : x ∈ p), q ⟨x, h⟩

theorem SetLike.coe_injective {A : Type u_1} {B : Type u_2} [i : SetLike A B] : Function.Injective SetLike.coe

@[simp]

theorem SetLike.coe_set_eq {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : ↑p = ↑q ↔ p = q

theorem SetLike.coe_ne_coe {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : ↑p ≠ ↑q ↔ p ≠ q

theorem SetLike.ext' {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} (h : ↑p = ↑q) : p = q

theorem SetLike.ext'_iff {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : p = q ↔ ↑p = ↑q

theorem SetLike.ext {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} (h : ∀ (x : B), x ∈ p ↔ x ∈ q) : p = q

Note: implementers of SetLike must copy this lemma in order to tag it with @[ext].

theorem SetLike.ext_iff {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : p = q ↔ ∀ (x : B), x ∈ p ↔ x ∈ q

@[simp]

theorem SetLike.mem_coe {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : B} : x ∈ ↑p ↔ x ∈ p

@[simp]

theorem SetLike.coe_eq_coe {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {x : { x : B // x ∈ p }} {y : { x : B // x ∈ p }} : ↑x = ↑y ↔ x = y

@[simp]

theorem SetLike.coe_mem {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : { x : B // x ∈ p }) : ↑x ∈ p

theorem SetLike.mem_of_subset {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {s : Set B} (hp : s ⊆ ↑p) {x : B} (hx : x ∈ s) : x ∈ p

theorem SetLike.eta {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} (x : { x : B // x ∈ p }) (hx : ↑x ∈ p) : ⟨↑x, hx⟩ = x

@[instance 100]

instance SetLike.instPartialOrder {A : Type u_1} {B : Type u_2} [i : SetLike A B] : PartialOrder A

Equations

• SetLike.instPartialOrder = PartialOrder.mk ⋯

theorem SetLike.le_def {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S : A} {T : A} : S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T

@[simp]

theorem SetLike.coe_subset_coe {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S : A} {T : A} : ↑S ⊆ ↑T ↔ S ≤ T

theorem SetLike.coe_mono {A : Type u_1} {B : Type u_2} [i : SetLike A B] : Monotone SetLike.coe

@[simp]

theorem SetLike.coe_ssubset_coe {A : Type u_1} {B : Type u_2} [i : SetLike A B] {S : A} {T : A} : ↑S ⊂ ↑T ↔ S < T

theorem SetLike.coe_strictMono {A : Type u_1} {B : Type u_2} [i : SetLike A B] : StrictMono SetLike.coe

theorem SetLike.not_le_iff_exists {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : ¬p ≤ q ↔ ∃ x ∈ p, x ∉ q

theorem SetLike.exists_of_lt {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : p < q → ∃ x ∈ q, x ∉ p

theorem SetLike.lt_iff_le_and_exists {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p : A} {q : A} : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p