2. Objects and relations

Most statements relate a few objects: an element belongs to a set, one set lies inside another, a function sends an input to an output. Definograph keeps one identity for each object and draws each relation with the role each object plays in it. In this lesson you follow objects through the relations of two statements and tell what a statement assumes from what it requires.

A statement about sets

This is Definograph's example Sets, membership, and inclusion:

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

Set ℝ is the type of sets of real numbers, so (A B : Set ℝ) introduces two sets. Between conditions, → means "implies", and a chain of them groups to the right: A ⊆ B → x ∈ A → x ∈ B means "if A ⊆ B, then if x ∈ A, then x ∈ B". So A ⊆ B and x ∈ A are assumptions, and x ∈ B is what the statement requires. The statement is true: if every element of A is in B, and x is in A, then x is in B.

The Relationships view

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

The Relationships view gives each relation a numbered card.

• The small heading on a card names the kind of relation: Set inclusion or Membership.
• Each object appears with its role in the relation: subset and superset, element and set. The gray badge before a name shows the kind of object: { } for a set, a for a number. The other badges in this lesson are ↦ for a function, T for a type, ⋯ for an expression built from other objects, and x for a variable of any other type.
• The tags above the objects place the relation in the logic of the statement. Card 01 is a Premise of an implication. Card 02 is Conditional on the premise, is itself a Premise of an implication, and sits Under 1 assumption. Card 03 is Conditional on the premise and sits Under 2 assumptions.

Card 03 is the only relation that is not a premise. It is the conclusion, required under the two assumptions in cards 01 and 02.

To follow an object, find every card it appears in. x is the element in cards 02 and 03. A is the subset in card 01 and the set in card 02. B is the superset in card 01 and the set in card 03. Definograph links these appearances because they are the same variable of the statement, not because they print the same letter.

Read the statement in order

The Visual sequence, which Definograph shows first, presents the same statement one step at a time. Here it has five steps: the variables, the step Given → then that sets out the implications, the inclusion, and the two memberships.

The small capitals above a step's title name the kind of step. Objects and choices introduces variables. Logical structure sets out implications and other connectives. Condition reads a relation such as membership or inclusion, whether it is assumed or required. Compare reads an equation or inequality between two expressions. Construction reads how an object is built, for example by applying a function.

This is step 3, the inclusion condition:

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

• In scope lists the variables available at this step: A, B and x, each introduced by ∀.
• Given assumption says where the condition sits in the statement: it is assumed, not asserted.
• The figure draws A inside B. The note under it states the figure's limits: "Every element of the inner set belongs to the outer set. The sets may be equal; spacing does not express proper inclusion."
• Lean fragment and source context holds the Lean text of the part being read, here A ⊆ B.

Step 5 is the conclusion:

∀ (A B : Set ℝ) (x : ℝ),
  A ⊆ B → x ∈ A → x ∈ B

• The line under In scope reads Conditional conclusion twice, once for each implication that encloses this step.
• 2 assumptions in scope lists A ⊆ B and x ∈ A.
• The figure places x in B, with the note "Membership condition · the named element belongs to the region". This is what the statement requires under those two assumptions.

These figures show single steps. In Definograph, Next and the Reading step menu move between steps, and an outline of the whole statement sits beside them: for every A, B, x; given A is contained in B; given x belongs to A; then x belongs to B. Below the steps, Full visual statement shows the whole reading at once.

Follow an object through a chain of maps

The second statement is Definograph's example An equation between two map paths:

∀ (A B C : Type) (f : A → B) (g : B → C)
  (h : A → C) (x : A), g (f x) = h x

(A B C : Type) introduces three arbitrary types, that is, three collections of objects of any kind. f : A → B is a function from A to B. Lean writes function application without brackets: f x is f applied to x, and g (f x) applies g to that result.

The statement says that applying f and then g to any x in A gives the same result as applying h, whatever the types A, B, C and the functions f, g, h between them. Here f(x) lies in B, and g(f(x)) and h(x) both lie in C, so the equation compares two elements of C.

Here is the last step of the Visual sequence:

∀ (A B C : Type) (f : A → B) (g : B → C)
  (h : A → C) (x : A), g (f x) = h x

Two routes start at x. The upper passes through f and then g and ends at g(f(x)). The lower passes through h and ends at h(x). The = between the two ends is the condition: "Compare the outputs of these map paths: they are required to agree."

Below the figure, the collapsed section Inside this expression holds the three applications that build f(x), g(f(x)) and h(x). In Definograph it opens to show them, with the note "These are parts of the expression, not separate assertions." Writing g(f(x)) builds an object; it claims nothing about it.

The Relationships view lists the same four relations as cards:

∀ (A B C : Type) (f : A → B) (g : B → C)
  (h : A → C) (x : A), g (f x) = h x

Card 01 is the equation. Cards 02 to 04 are the applications, each with an input, a function and an output. The type under each object says where it lives. x has the badge x because its type A is arbitrary; f(x), g(f(x)) and h(x) have ⋯ because they are built from other objects.

f(x) is the output of card 03 and the input of card 02. That shared object joins f and g into one route.

The Structure tab under Explore a sample draws all the objects and relations at once, with a line for each role. The types A, B and C appear as objects too, with the badge T. Selecting an object highlights its lines. Here x is selected:

∀ (A B C : Type) (f : A → B) (g : B → C)
  (h : A → C) (x : A), g (f x) = h x

The two highlighted lines from x are its roles as input 1 in the applications of f and of h. The other lines are dimmed.

The Visual sequence can show the same thing. In Definograph, when you select x in one of its figures, a dashed line, the identity thread, joins every place in the Visual sequence where x appears. The thread says only that these are one object, the x introduced at the start of the statement. Its route means nothing. Definograph draws the thread from the positions of the elements on its page, so this site has no recording of it.

What these views do not tell you

• That an assumption holds. A ⊆ B has a card and a figure, but only as a premise. In the words of the Structure view: "A relation may occur inside an assumption, negation, or alternative; its presence is not a claim that it holds."
• That the statement holds. The second statement is false (Exercise 2.3). Definograph draws it anyway, because it is a well-formed statement.
• Geometry. "These are diagrams of mathematical roles. Relative position and distance carry no geometric meaning." The subset figure does not say that A is smaller than B; the two sets may be equal. The curves of the lines in the Structure view mean nothing either.
• How many elements. No figure says how many elements a set has, or that it has any.

Exercises

Exercise 2.1. In the Relationships view of the sets statement, which card is the conclusion? How can you tell without reading the Lean?

Exercise 2.2. Remove the first assumption:

∀ (A B : Set ℝ) (x : ℝ), x ∈ A → x ∈ B

Is the statement still true? Which card of the Relationships view has no counterpart now?

Exercise 2.3. Is the map-path statement true?

Exercise 2.4. Trace f(x) in the Relationships view of the map-path statement. In which cards does it appear, and in which roles?

Exercise 2.5. Definograph's example Functions between arbitrary types is:

∀ (α β : Type) (f : α → β),
  Function.Injective f →
  ∀ x y : α, f x = f y → x = y

Function.Injective f says that f is injective. Which conditions are assumptions, and which one is required? If you have Definograph running, open the Relationships view of this example and compare its tags with your answer.