José Grimm
email: jose.grimm@inria.fr

Implementation of Bourbaki's Elements of Mathematics in Coq: Part Three Structures

Keywords: Gaia, Coq, Bourbaki, structure, morphism, isomorphisms Gaia, Coq, Bourbaki, structure, morphisme, isomorphisme Tbase: nat -> Tree | Tpowerset : Tree -> Tree |

proof assistant of the Theory of Sets of Bourbaki. It explains Book I, Chapter III, Section 7 (Inverse limits and direct limits) and the start of Book I, Chapter IV (structures). The code is available on the Web, under http://www-sop.inria.fr/marelle/gaia.

Chapter 1

Introduction

In this document, we explain the implementation in COQ of Chapter IV of the Theory of Sets, entitled "Structures" as described in [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF]. This Chapter (minus the appendix) is included in [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF], translated in English in [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]. The implementation of Chapter II and Chapter III is described in [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets[END_REF] and [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF] respectively. Section 7 of Chapter III ("Inverse limits and direct limits") forms the last chapter of this document, see page 43. Chapter I ("Description of Formal Mathematics") is discussed in [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets[END_REF].

Chapter IV starts with « The purpose of this chapter is to describe once and for all a certain number of formative constructions and proofs (cf. Chapter I, §1, no. 3 and §2, no. 2) which arise very frequently in mathematics. » In fact, the idea is to study mathematical structures (ordered sets, groups, topologic spaces etc), functions between structures (morphisms, isomorphisms), and deductions of structures (induced structures, products, quotients, tensor products, etc). However, the exposition is abstract, there is no link to other books, and the ideas presented here are not used elsewhere (neither by Bourbaki, nor by anybody else; people prefer to use a "theory of categories", that has the same purpose). There are some small examples, but the notion of "group" is already too complicated to be given in detail; the way groups are defined in the Book of Algebra [START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF] gives no indication of how a group structure could be defined (see details below).

Chapter IV contains no theorem at all, but some criteria CST1 through CST23. An example of a criterion is: « C14. Let A be a relation in T and let T be the theory obtained by adjoining A to the axioms of T . If B is a theorem in T then A =⇒ B is a theorem in T . » Some of the criteria of the chapter have a similar form: if, in the theory obtained by adding to T some axioms, some relation holds, then some other relation holds in T . Chapter I, §1, no. 3 explains (among other things) what is a valid object in the theory; in particular, there are terms (aka sets) and relations; a letter is a term. The object (∀x)R is valid and a relation whenever x is replaced by a letter and R by a relation. In C14 A is not considered as a letter but as a name. Recall that a theorem is a statement with a proof (in the sense of Chapter I, §2, no. 2). For instance x = x is the first theorem proved by Bourbaki. It follows that (∀x)(x = x) is a theorem.

Bourbaki uses a first order logic: quantification is only over sets. The expression (∀A)(A =⇒ A) it not a formative construction, whatever A (after the quantifier, there must be a letter, which is a set, and cannot be on the LHS of the implication sign). Hence, Bourbaki needs some criteria. For instance, by CF5, if A is a relation, so is A =⇒ A, and C8 says: « If A is a relation in T , then A =⇒ A is a theorem in T . » In our implementation of Bourbaki, we allow Chapter IV considers a theory T stronger than the Theory of Sets (the theory itself, or some extension of it). Whenever x and y are two sets, then x ∈ y is a relation, as well as x ⊂ y. The relation x = y is equivalent to x ⊂ y and y ⊂ x. One can construct {x, y}, x ∪ y, (x, y), x × y, P(x), x y , F (x; y), etc. Recall that a function f is a triple (a, b, c) where a is the source, b the target and c the graph; it belongs to the set of functions F (a; b). The function f → c is the canonical isomorphism F (a; b) → b a ; the target is the set of all functional graphs with domain a, the range being a subset of b. Bourbaki writes somewhere « we shall often use the word "function" in place of "functional graph". » This may be confusing because a function has a target and a functional graph has none. For this reason, we shall signal these abuses of language. For Bourbaki, a "mapping of A into B" is a function whose source is equal to A and whose target is equal to B. The subtle difference is that "mapping" is never used alone (there are however some exceptions, so that we shall use "mapping" as a synonym of "function"). For Bourbaki, x → x + 2(x ∈ N, x + 2 ∈ N) is a function (source and target being N). A more common notation is f : N → N, x → x + 2. The source and target may be indicated in a different way, or perhaps omitted. For us, the COQ object 'fun x => x.+2' will be a function (it is not a Bourbaki object, as its type is nat→nat). If x + 2 denotes the double ordinal successor, then x → x +2 will be considered a function; this is not a Bourbaki function in that it has no source and no target (there is no set containing all ordinals); this is in fact not a Bourbaki object at all. Three strategies are used: (a) the object is considered as a term with some free variables, x, y, etc, denoted by Täxä or Täx, yä, etc, instantiation is denoted by Tä1ä or Tä2, 3ä, etc. In such a notation, there may be other free variables; (b) there a notation, P(x), x + y, x y, x * , etc. The notation may be overloaded (as in x + y) or generic (in what follows x y is the generic law of a group); (c) the object is named by a letter (or a sequence Inria of letters), the value being an index. For instance, Bourbaki says: « Put ℵ α = Card(ω α ); ℵ α is said to be the aleph of index α. » Here ω is not the name of the function, so that ω = ω 0 makes sense.

In Chapter IV there is a footnote that says « We use the notion of integer in the same manner as in Chapter I, that is to say, in the metamathematical sense of marks arranged in a certain order; this use has nothing to do with the mathematical theory of integers which was developed in Chapter III. » There is a section that explains when Räx 1 , . . . , x n , s 1 , . . . , s p ä is a transportable relation for the typification Täx 1 , . . . , x n , s 1 , . . . , s p ä. In the special case n = 2, p = 1, this explains when Räx 1 , x 2 , s 1 ä is a transportable relation for the typification Täx 1 , x 2 , s 1 ä.

There is a definition for "echelon construction scheme S on n terms", and of 〈x 1 , . . . , x n 〉 S . The first criterion is then CST1. If f i is a mapping of E i into E i , and if f i is a mapping of E i into E i (1 ≤ i ≤ n), then for every echelon construction scheme S on n terms we have

〈 f 1 • f 1 , f 2 • f 2 , . . . , f n • f n 〉 S = 〈 f 1 f 2 , . . . , f n 〉 S • 〈 f 1 , f 2 , . . . , f n 〉 S .
The objective is to convert this criterion into a theorem. Take n = 2. The criterion becomes:

If f 1 is a mapping of E 1 into E 1 , if f 2 is a mapping of E 2 into E 2 , if f 1 is a mapping of E 1 into E 1 , if f 2 is
a mapping of E 2 into E 2 , then for every echelon construction scheme S on 2 terms we have

〈 f 1 • f 1 , f 2 • f 2 〉 S = 〈 f 1 , f 2 〉 S •〈 f 1 , f 2 〉 S .
This could be converted into a theorem, if only we could quantify over S (this is impossible, as S is not in the theory T ). Moreover, to say that S is a scheme on 2 terms cannot be expressed in T , and the expression 〈 f 1 , f 2 〉 S cannot be constructed in T . Take for S the sequence (0, 1), (0, 2), (1,0), [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]0), [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF]0), [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF][START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF]. In this example 〈 f 1 , f 2 〉 S can be effectively constructed. Moreover, there are sets A 6 and A 6 such that, if f 1 and f 2 are as above, then 〈 f 1 , f 2 〉 S is a mapping of A 6 into A 6 . For this particular S, the criterion becomes a theorem by quantifying over the ten sets.

The amusing point is that, since T is stronger than the theory of sets, it is possible to use its integers, in the sense indicated above. It is possible to consider S as object in this theory. Now, if n = 2, the criterion becomes a theorem (proof by induction on the length of S), where 〈 f 1 , f 2 〉 S is defined by induction on the length of S. Finally, we consider lists of objects in T , and the criterion becomes: whatever the integer n, whatever f, f , E, E , E lists of length n, satisfying some property, if f • f has the obvious meaning, then for every echelon construction scheme S on n terms we have 〈f • f〉 S = 〈f 〉 S • 〈f〉 S . This is a statement in T with no free variables that happens to be a theorem (bold face letters are sometimes used in this sense in the Appendix of the Chapter).

The first example of a structure given by Bourbaki is: « take T to be the theory of sets, and consider the species of structures which has no auxiliary base set, one principal base set A, the typical characterization s ∈ P(A × A), and the axiom s • s = s and s ∩ s -1 = ∆ A (∆ A being the diagonal of A × A), which is a transportable relation with respect to the typification s ∈ P(A × A), as is easily verified. It is clear that this species of structures is just the theory of ordered sets (Chapter III,§1,[START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]. » Let's try to understand the example. In the case of a vector space E over a field K, there is a significative distinction between E and K; the former is called the principal base set, the latter is called the auxiliary base set. Here we have only one set, the principal base set. The expression s ∈ P(A × A) says that s is a set of pairs (x, y) with x ∈ A and y ∈ A. The notation s •s denotes the composition of graphs (a variant of the composition of functions introduced above), and s -1 is the inverse graph. The relation s ∩ s -1 = ∆ A is equivalent to: if x ∈ A then (x, x) ∈ s and if (x, y) ∈ s and (y, x) ∈ s then x = y. So s • s = s and s ∩ s -1 = ∆ A means that the relation (x, y) ∈ s is an order relation. We shall see later what it means for the relation to be

José Grimm

transportable and why this is important.

In the appendix of [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF] (not translated into English), one can find the example of a group; it will be discussed in details below. The typical characterization has the form s ∈ P((E×E)×E), and the axiom is a bit complicated. Let's admit the Axiom of Unique Choice (AUC) in the form: if P(x, y) is a relation that depends on x (maybe on y and some other variables), such that (under some assumptions on y and the other variables) there is a unique x satisfying P, then we can consider "the" x that satisfies P. For instance, if P does not depend on y we may denote it by x 0 , otherwise, we may denote it by x P (y), or some other notations. Example: if P denotes "x and y are integers and y = 2x," then the x will be denoted by y/2. This makes sense when y is an even integer. Bourbaki uses τ x (P) for its Axiom of Choice, this is defined whatever P. How should we interpret y/2 when y is not an even integer? in a typed theory like COQ, if y → y/2 is of type nat→nat, then the expression becomes ill-typed when y is not an integer. Here typification comes into play: y of type nat is replaced by the typification y ∈ N. In COQ, you can use dependent types; this means that y/2 can be a function of two arguments, an integer and a proof that it is even. In some cases this is the right choice. However, using such a mechanism for defining the multiplicative inverse of an element of the field (that exists only for non-zero elements) is much too complicated; using an option type (i.e., saying that y/2 is in the disjoint union of N and some singleton) is sometimes possible, sometimes complicated. In SSREFLECT the half of y is defined by (y -1)/2 when y is odd. The specification of a unit ring says:

if x • y = y • x = 1, then x is a unit; if x is a unit then x • x -1 = x -1 • x = 1.
The specification of a field says that every non-zero element is a unit, and 0 -1 = 0. One could define y/2 to be some default value x 0 ; however, this should meet the typification (if the typification is x ∈ E, this requires E to be non-empty; in SSREFLECT, a ring has at least two elements since 0 = 1 is assumed. Another solution would be to define y/2 to be y (this works whenever y and y/2 have the same typification).

The axiom of the group structure implies that s is a functional graph. Hence there exists an operation a b, defined whenever a and b are in E such that s is the set of all ((a, b), a b) for a and b in E (note that s is uniquely defined by and E). Moreover the law is associative; there is a unit, every element has an inverse. Using AUC, one may denote the unit by e, the inverse by x * , and prove that the axiom is equivalent to the usual axiom of a group.

What is a group? the short answer is E and s, the long answer is E, x y, e, x * . The second item is the function x, y → x y; it could be replaced by , when it is clear that is a binary operator; it could be replaced by top, if x y is a notation for top(x, y). The last item is the function x → x * ; in this case omitting the variable is rare. Note that is not an object of the theory of sets of Bourbaki, and not uniquely defined by the group (only a b for a and b in E is uniquely defined). So a group could be defined by E, E , e, * E (introducing the graphs of the functions; these are objects of the theory). Alternatively, it could be E and a triple ( E , e, * E ). In the case of a group E is exactly s. The question is now: how to express relations of the form x x * = e, given that the group contains E and * E . One solution would be to split the axiom into a conjunction A∧B, where A implies that E , * E , etc, are functional graphs, defined on E × E, E, etc. It justifies the use of and * in the B-part of the axiom. In practice, people say: a group is a set E, with a binary operation x y and a unary operation x * satisfying B.

Consider now the definition of a group ([5, page 30]): A set with an associative law of composition, possessing an identity element, and under which every element is invertible, is called a group. The definition is interesting in that nothing is named. This definition refers to another one, page 15: « let E be a unital magma, its law of composition, e its identity element and x and x two elements of E. x is called an inverse of x if x x = x x = e.

Inria

An element x of E is called invertible if it has an inverse. A monoid all of whose elements are invertible is called a group. » The definition explains also what is a left inverse, a right inverse, and is followed by a remark explaining that the inverse is unique.

We once tried to implement algebraic structures in COQ, but it was complicated and unusable (see previous discussion on and E ). However, is a COQ object, especially if we replace "if a and b belong to E, then a b belongs to E" by "if a and b are of type E, then a b is of type E". Moreover ∀x, x x * = e is also a COQ object (there is no need to assume x ∈ E, this simplifies the axiom). Finally, one can pack, in the same object, the functions and the axiom. Here is an example.

Record mixin_of (V : Type) : Type := Mixin { zero : V; opp : V -> V; add : V -> V -> V; _ : associative add; _ : commutative add; _ : left_id zero add; _ : left_inverse zero opp add }.

As you can see, the definition is straightforward. There is a complicated mechanism, described in [START_REF] Garillot | Packaging Mathematical Structures[END_REF], that explains how to implement concrete commutative groups (by the way, the previous structure is called Zmodule in the file ssralg of SSREFLECT). A more complicated object is the following.

This is the definition of a finite group in SSREFLECT. It is preceded by the following comment

We split the group axiomatisation in two. We define a class of "base groups", which are basically monoids with an involutive antimorphism, from which we derive the class of groups proper. This allows use to reuse much of the group notation and algebraic axioms for group subsets, by defining a base group class on them. We use class/mixins here rather than telescopes to be able to interoperate with the type coercions. Another potential benefit (not exploited here) would be to define a class for infinite groups, which could share all of the algebraic laws.

José Grimm

An important part of the definition of a group, ring, etc, is the interface: the internal structure is completely hidden, and there are many useful definitions. A typical example is the order of an element x. By lines 4 and 5, the order of x is the cardinal of the set generated by {x}; this is a natural number as T is a finite set. Line 3 says that the subgroup generated by A is the intersection of all subgroups G of T, such A ⊂ G; that this is a subgroup follows by induction on the number of elements in the intersection (which is finite, because P(T) is finite). Line 2 is part of many lines of the code that helps COQ to expand correctly all notations; it defines groupT as the type of all subgroups, the type of all A (elements of P(T)) satisfying the property of line 1. If A and B are in P(T) and A B is the set of all x * y for x ∈ A and b ∈ B, then makes P(T) a group. So, on line 1, COQ sees to groups, T and P(T) and correctly interprets the unit and the law. The lemma says that the inverse of x is x n , where n is one less than the order of x, and

Definition

x n = x * . . . * x.

Additional code

We consider here an implementation of a list x 1 , x 2 , . . . , x n . The first idea would be a function graph with domain [1, n]. It is sometimes more interesting to start indices with zero. So f (0) = x 1 , f (1) = x 2 , etc. This means x i = f (i -1). The domain of f becomes now I n , the set of integers < n. Our implementation relies on the fact that I n = n. This simplifies the definition from: a functional graph for which there exists an integer n such that the domain is I n to: a functional graph whose domain is an integer. The length of the list is the number of elements of the domain, the cardinal of I n , hence n; this is another simplification.

(forall i, \1c <=c i -> i <=c slength f -> (Vl f i = Vl g i)) -> f =g . Lemma Vl_p1 f E x : slist_E f E -> \1c <=c x -> x <=c (slength f) -> inc (Vl f x) E.
We consider now a technique called "induction on a stratified collection". The collection is defined by a property W and a rank ρ. It is not necessary that there exists a set containing all objects satisfying W, but it is assumed that if W(x) holds then ρ(x) is an ordinal, and that, for every ordinal α there is a set W α containing those x such that W(x) holds and ρ(x) < α. This implies that there is a set W α such containing those x such that W(x) holds, and ρ(x) = α. Let H(x, f ) be a functional term. One can define a unique functional term f such that f (x) = H(x, f x ), whenever x satisfies W, where f x is the (unique surjective) function defined on W ρ(x) such that f x (a) = f (a), whatever a. The idea is to define by transfinite induction a function f α on W α that depends on the f β for β < α. We recall here the assumptions and the main result.

Hypothesis OS_idx: forall x, W x -> ordinalp (idx x). Hypothesis Wi_coll: forall i, ordinalp i -> exists E, forall x, inc x E <-> (W x /\ idx x <o i).

Lemma stratified_fct_pr x (f := stratified_fct):

W x -> f x = H x (Lg (stratified_set (idx x)) f).
Recall that 'functions X Y' is the set of all functions X → Y, and 'bijections X Y'

is the set of all bijections X → Y. If X is a set, f a function, then f 〈X〉 is the set of all f (x)
for x ∈ X. This induces a function P(X) → P(Y) called "canonical extension of f to sets of subsets", denoted here by \Pof (analogous to \Po, the powerset), or P( f ). The properties we shall use here are the following: if f is a bijection so is P( f ) and P(f -1 ) = P( f ) -1 ; P( f • g ) = P( f ) • P(g ), P(I E ) = I P(E) if I E is the identity function of E.

Given a family of functions f i : E i → F i one can consider the product, the function E i → F i that maps a sequence x i to a sequence y i with y i = f i (x i ). In what follows, we consider two functions f : E → F, g : E → F , the product will be denoted by f \ftimes g. We have ( f × g )(x, y) = ( f (x), f (y)). If both functions are bijections, so is the product and ( f × g

) -1 = f -1 × g -1 , ( f × g ) • ( f × g ) = ( f • f ) × (g • g ); I E × I F = I E×F .
We need two additional lemmas: if 1 ≤ i ≤ k, and k is an integer, then i -1 is an integer, i = (i -1) + 1 and i -1 < k. Our induction principle (version 6) says if p(0) holds, if p(n + 1) is true whenever p holds for all integers ≤ n, then p holds everywhere. We replace it by: if p(n) is true whenever p holds for all integers < n, then p holds everywhere.

Lemma Nat_induction6' (P : property):

(forall n, natp n -> (forall k, k <c n -> P k) -> P n) -> forall n, natp n -> P n.

Lemma cpred_pr6' k i: natp k -> \1c <=c i -> i <=c k -> [/\ natp (cpred i), i = csucc (cpred i) & cpred i <c k ].

Example: the structure of a group

The definition of a group structure in the appendix of [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF] uses an unusual form of associativity. For this reason, we start with some preliminaries.

Recall that B•A is the set of all (a, b) such that there is c such that (a, c) ∈ A and (c, b) ∈ B. In the case where A is a functional graph, there is a function v A such that (a, v A (a)) ∈ A whenever a is in the domain of A. If A and B are composable (the domain of B is a subset of the domain of A), and if B is a functional graph, then v B•A (a) = v B (v A (a)) whenever a is in the domain of A. This leads to an alternate definition of composition (note that there is a third definition, for functions). Composition is associative (this is always the case for the definition given here, is true under conditions for the two other definitions).

Let's consider A = s • (s ⊗ I E ). This makes sense when s ⊂ ((E × E) × E)). There is a simple formula for x ∈ A, considering the complexity of the definition of ⊗. If s is a law, this is the set of all (((a, b), c), (a b) c), for a, b, and c in E. Consider now B = s • (I E ⊗ s). The result is similar. The formula B • J E is similar too.

Lemma Sprod_case1 s E x (f := s \cg (Sprod s (GE_I E))): sub s ((E \times E) \times E) -> (inc x f <-> exists a b c d t, [/\ x = J (J (J a b) c) d, inc (J (J t c) d) s & inc (J (J a b) t) s]). Lemma Sprod_case_l1 s E x (f := s \cg (Sprod s (GE_I E))): Law s E -> (inc x f <-> exists a b c, [/\ inc a E, inc b E, inc c E & x = J (J (J a b) c) (VL s (VL s a b) c) ]). Lemma Sprod_case2 s E : Law s E -> s \cg (Sprod s (GE_I E)) = fun_image ((E\times E) \times E) (fun z=> J z (VL s (VL s (P (P z)) (Q (P z))) (Q z))). Lemma Sprod_case3 s E x (f := s \cg (Sprod (GE_I E) s)): sub s ((E \times E) \times E) -> (inc x f <-> exists a b c d t, [/\ x = J (J a (J b c)) d, inc (J (J a t) d) s & inc (J (J b c) t) s]). Lemma Sprod_case4 s E x (f := (s \cg (Sprod (GE_I E) s)) \cg (GE_J E)): sub s ((E \times E) \times E) -> (inc x f <-> exists a b c d t, [/\ x = J (J (J a b) c) d, inc (J (J a t) d) s & inc (J (J b c) t) s]). Lemma Sprod_case_l2 s E x (f := (s \cg (Sprod (GE_I E) s)) \cg (GE_J E)): Law s E -> (inc x f <-> exists a b c, [/\ inc a E, inc b E, inc c E & x = J (J (J a b) c) (VL s a (VL s b c)) ]).

José Grimm

Associativity is now s

• (s ⊗ I E ) = s • (I E ⊗ s) • J E . Lemma Bourbaki_assoc s E : Law s E -> ( (s \cg (Sprod s (GE_I E))) = ((s \cg (Sprod (GE_I E) s)) \cg (GE_J E)) <-> forall a b c, inc a E -> inc b E -> inc c E -> VL s a (VL s b c) = VL s (VL s a b) c).

The group axiom

We shall describe and comment here the group axiom. It has the form R 1 ∧ R 2 ∧ R 3 ∧ R 4 , and depends on two parameters E and s.

We assume moreover (1.1)

s ∈ P(E × E × E).
This is called the typification, it says that an element of s is a triple of elements of E. Axiom R 1 is

∀a ∈ E, ∀b ∈ E, ∃c, (a, b, c) ∈ s, ∀x ∈ s, ∀y ∈ s, pr 1 x = pr 1 y =⇒ x = y. (1.2)
We say that is a law of composition if a b belongs to E, whenever a and b belong to E. We can consider as a function f : E × E → E, or a functional graph g . Note that f is a triple with source E × E, target E, and graph g . Bourbaki often identifies f and g .

Section GroupExample.

Definition GT E s := inc s (\Po ((E\times E) \times E)).

Definition is_law E f := forall x y, inc x E -> inc y E -> inc (f x y) E. Definition GL E s := (forall a b, inc a E -> inc b E -> exists c, inc (J (J a b) c) s) /\ (forall a b, inc a s -> inc b s -> P a = P b -> a = b).

Definition Op E f := Lg (E\times E) (fun z => f (P z) (Q z)).

Definition Opfun E f := Lf (fun z => (f

(P z) (Q z))) (E \times E) E. Lemma GEl_prop1 E f: is_law E f -> function_prop (Opfun E f) (E\times E) E. Lemma GEl_prop2 E f: Op E f = graph (Opfun E f). Lemma GEl_prop3 E f: is_law E f -> GT E (Op E f). Lemma GEl_prop4 E f: is_law E f -> GL E (Op E f).
Bourbaki says: the relation (1.2) is transportable for the typification s 1 ∈ P(x 1 × x 1 ). This is obviously a mistake: it should be s 1 ∈ P(x 1 × x 1 × x 1 ), with s 1 replaced by s and x 1 by E.

In this case, transportable means: whenever F is a set, g a bijection E → F, ĝ its extension, s = ĝ (s), and

s ∈ P(E × E × E), then R is transportable if R(E, s) is equivalent to R(F, s ).
For simplicity, we do not write down ĝ , just say that s = ĝ (s), is the set of all (g (a), g (b), g (c)) where (a, b, c) ∈ s.

Definition transport s g := fun_image s (fun x => J (J (Vf g (P (P x))) (Vf g (Q (P x)))) (Vf g (Q x))).

Inria

Lemma transport_p1 E F s g: GT E s -> bijection_prop g E F -> GT F (transport s g). Lemma transport_p2 E s: GT E s -> (transport s (identity E)) = s. Lemma transport_p3 E F G s g h: GT E s -> bijection_prop g E F -> bijection_prop h F G-> transport (transport s g) h = transport s (h \co g).

The typification is transportable. Relation (1.2) is transportable.

efinition transportable R:= forall E F s g, bijection_prop g E F -> GT E s -> (R E s <-> R F (transport s g)).
Lemma transportable_GT: transportable GT. Lemma transportable_GL: transportable GL.

If s satisfies (1.1) and (1.2) then s is a law in the sense introduced above. If is the operation associated to the law, then is a law, and its graph is s. Consider a bijection g : E → F. We know that s is a law, hence induces an operation ⊥ on F. We have g (a)⊥g (b) = g (a b).

Lemma GE_prop1 E s a: GT E s -> inc a s -> [/\ pairp a, pairp (P a), inc (P (P a)) E, inc (Q (P a)) E & inc (Q a) E]. Lemma GE_prop2 E s: GT E s -> GL E s -> Law s E. Lemma GE_prop2_stable E s : GT E s -> GL E s -> forall a b, inc a E -> inc b E -> inc (VL s a b) E. Lemma GE_prop3 E s (f := VL s) : GT E s -> GL E s -> is_law E f /\ (Op E f) = s.
Lemma transport_op E F g s: bijection_prop g E F -> GT E s -> GL E s -> forall a b, inc a E -> inc b E -> Vf g (VL s a b) = VL (transport s g) (Vf g a) (Vf g b).

Bourbaki says that the second part of the axiom is s

• (s × I E ) = s • (I E × s) • J.
This makes no sense. The correct relation is

(1.3) s • (s ⊗ I E ) = s • (I E ⊗ s) • J E .
Its equivalent (modulo the first part of the axiom) to

(1.4) ∀a, b, c ∈ E a (b c) = (a b) c.
The conjunction of the two axioms is transportable. Proof. For any typification T of s, if R 1 is transportable, if g is a bijection E → F, and s the transport of s, then R 1 ∧R 2 is transportable if, assuming T(s), R 1 (E, s), T(s ), R 1 (F, s ), then R 2 (E, s) is equivalent to R 2 (F, s ). In this context R 2 is equivalent to (1.4) and the result is obvious.

Definition GA E s := s \cg (Sprod s (GE_I E)) = (s \cg (Sprod (GE_I E) s)) \cg (GE_J E). Lemma GE_prop4 E s (f := VL s): GT E s -> GL E s -> (GA E s <-> forall a b c, inc a E -> inc b E -> inc c E -> f a (f b c) = f (f a b) c).
Lemma transportable_GA: transportable (fun E s => GL E s /\ GA E s).

José Grimm

Assume now that we have a unit. The Bourbaki definition (first line) uses s 1 (a, b) = c; we prefer (a, b, c) ∈ s (second line). The unit is unique; by AUC we may name it. We have e ∈ E and a e = e a = a.

(∃z)(z ∈ x 1 and(∀z )((z ∈ x 1 ) =⇒ (s 1 (z, z ) = z ands 1 (z , z) e, z, z) ∈ s and(z, e, z) ∈ s. (1.5) e ∈ E and ∀a ∈ E, a e = e a = a.

= z ))). ∃e ∈ E, ∀x ∈ E, (
Definition GU Z s:= exists2 z, inc z E & forall z', inc z' E -> inc (J (J z z') z') s /\ inc (J (J z' z) z') s. Definition unit E s e:= forall z, inc z E -> VL s e z = z /\ VL s z e = z. Definition un E s := select (unit E s) E. Lemma GE_prop5 E s : GT E s -> GL E s -> GU E s -> exists2 z, inc z E & unit E s z. Lemma GE_prop6 E s z z': inc z E -> unit E s z -> inc z' E -> unit E s z' -> z = z'. Lemma GE_prop7 E s : GT E s -> GL E s -> GU E s -> inc (un E s) E /\ unit E s (un E s).
Bourbaki says: R 1 ∧R 2 ∧R 3 is transportable. The reason is that « R 3 is transportable for the typification "T and z ∈ x 1 and z ∈ x 1 ".» This statement is a bit strange. Why is it true? Since z and z are bound variables in R 3 , it is transportable (by CT8) for the typification T in the theory obtained from the current theory by adjoining the axiom x 1 = . However, adjoining

x 1 = contradicts R 1 ∧ R 2 ∧ R 3 . He deduces that R 1 ∧ R 2 ∧ R 3 is transportable.
The trick is that, if E has a unit e, then g (e ) is the unit of F, hence R 3 holds for F. Bourbaki says that the unit it is relatively transportable of type x 1 for the typification T 0 . Its definition of a unit is

τ z (z ∈ x 1 and (∀z )((z ∈ x 1 ) =⇒ (s 0 (z, z ) = z and s 0 (z , z) = z ))). Lemma GE_prop7_rev E s: GT E s -> GL E s -> forall x, inc x E -> unit E s x -> GU E s. Lemma transport_unit E F g s x: bijection_prop g E F -> GT E s -> GL E s -> (inc x E /\ unit E s x) -> (inc (Vf g x) F /\ unit F (transport s g) (Vf g x)). Lemma transport_un E F g s: bijection_prop g E F -> GT E s -> GL E s -> GU E s -> un F (transport s g) = Vf g (un E s). Lemma transportable_GU: transportable (fun E s => (GL E s /\ GA E s) /\ GU E s).
We consider now the final axiom.

(

1.6) ∀z, z ∈ E, ∃u ∈ E, (z, u, z ) ∈ s and ∃v ∈ E, (v, z, z ) ∈ s.
It is equivalent to: for every x and y, there is a and b such that x a = y and b x = y. Taking for y the unit, one gets that every element has a left inverse (as well as a right inverse). If a is Inria a left inverse and b a right inverse then a = b. So, the left inverse is unique. By AUC, we may denote it x * . This is also the right inverse.

Definition GI E s: forall z z', inc z E -> inc z' E -> (exists2 z'', inc z'' E & inc (J (J z z'') z') s) /\ (exists2 z''', inc z''' E & inc (J (J z''' z') z') s). Definition left_inverse E s (x x': Set) := inc x' E /\ VL s x' x = un E s. Definition right_inverse E s (x x': Set) := inc x' E /\ VL s x x' = un E s. Definition inverse E s x := select (fun x' => VL s x' x = un E s) E. Lemma GE_prop8l E s: GT E s -> GL E s -> GU E s -> GI E s -> forall x, inc x E -> exists a, left_inverse E s x a. Lemma GE_prop9 E s : GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x a b, inc x E -> left_inverse E s x a -> right_inverse E s x b -> a = b. Lemma GE_prop10l E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x a b, inc x E -> left_inverse E s x a -> left_inverse E s x b -> a = b. Lemma GE_prop11l E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x, inc x E -> left_inverse E s x (inverse E s x). Lemma GE_prop11r E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x, inc x E -> right_inverse E s x (inverse E s x). Lemma GE_prop12l E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x y, inc x E -> inc y E -> VL s x (VL s (inverse E s x) y) = y.
If every element has a left and a right inverse, then axiom R 4 holds. If y is a left inverse (or the inverse) of x, then g (y) is a left inverse (or the inverse) of g (x). It follows that the conjunction of the four axioms is transportable. Bourbaki says that the inverse is relatively transportable of type x 1 for the typification "T 0 and u ∈ x 1 ". His definition of the inverse of u is τ z (z ∈ x 1 and s 0 (z, u) = e and s 0 (u, z) = e).

Lemma GE_prop13a E s: GT E s -> GL E s -> GU E s -> GA E s -> (forall x , inc x E -> exists y, left_inverse E s x y /\ right_inverse E s x y) -> bijection_prop g E F -> GT E s -> GL E s -> GU E s -> inc x E -> left_inverse E s x y -> left_inverse F (transport s g) (Vf g x) (Vf g y).
Lemma transport_inv E F g s x y:

bijection_prop

g E F -> GT E s -> GL E s -> GU E s -> inc x E -> left_inverse E s x y -> left_inverse F (transport s g) (Vf g x) (Vf g y). Lemma transport_inverse E F g s x: bijection_prop g E F -> GT E s -> GL E s -> GA E s -> GU E s -> GI E s -> inc x E -> Vf g (inverse E s x) = inverse F (transport s g) (Vf g x). Lemma transportable_GI: transportable (fun E s => ((GL E s /\ GA E s) /\ GU E s) /\ GI E s).
Section GroupExample.

José Grimm :

Properties

A group is defined by its typification and its axiom, here

R 1 ∧ R 2 ∧ R 3 ∧ R 4 .
There are alternative definitions. For instance, in R 4 , it suffices to take for z the unit. Since the left inverse is the right inverse, one can write it as: whenever a ∈ E, there is

b ∈ E such that a b = b a = e. The relation R s (∀z), ((z ∈ v) =⇒ (z -1 ∈ v and (∀z )((z ∈ v =⇒ (s 0 (z, z ) ∈ v))))
is relatively transportable for the typification T 0 and v ∈ P(x 1 ). Proof. Same notations as above. Assume v ⊂ E; then v is the set of all g (x) for x ∈ v. Denote by x * the inverse in E, by x -1 the inverse in F. Take x ∈ v , so that x = g (x) for some x ∈ v. Note that x ∈ E, and

g (x) is well defined. The relation R s says x * ∈ v, so that g (x * ) ∈ v . But g (x * ) = x -1 . Assume y ∈ v , so that y = g (y) with y ∈ v. Now, x y ∈ v so x ⊥y = g (x y) ∈ v . The conclusion follows.
The relation R s is interpreted as v is a subgroup. The subgroup generated by w is relatively transportable of type P(x 1 ) for the typification T 0 and w ∈ P(x 1 ). The relation

(∃z )(∃z )(z ∈ x 1 and z ∈ x 1 and z = s 0 (z , s 0 (s , s 0 (z -1 , z -1 ))))
is read: z is a commutator. It is transportable for the typification T 0 and z ∈ x 1 . So: the commutator subgroup is relatively transportable of type P(x 1 ).

Note: it should be easy to formalize the notion of: R(z) is relatively transportable of type A for a typification T and T (z); then prove the previous statements in COQ.

Trees

Recall that (1.1) says x ∈ P(E × E × E). Write it in the form s ∈ S(E). If g is a bijection E → F, we consider its extension g S : S(E) → S(F). In what follows, S will be implemented by an echelon. However, there is more than one echelon such that S(E) = P(E × E × E), and it is not clear whether these echelons give the same g S . For this reason we shall consider another formalism: that of a tree. In the case of a vector set E over a field K, there are two sets, E and K. These are called the base sets, and numbered x 1 , x 2 .

There are three possibilities for a tree: There is a base case T b (for instance if x = T b (0) then S(x) = E); there is the case of a product, for instance, if

y = T x (T x (x, x), x) then S(y) = (E × E) × E; there is the case of the power set, for instance S(T p (y)) = P((E × E) × E).
We show here an example of tree, in COQ, and show two functions on trees, depth and size.

Recall the definition by stratified induction. It depends on a property W (being a tree) a function ρ (the depth), an operator H, specified below. We first must show that ρ(x) is an ordinal, whenever W(x) holds; this is trivial. We then must show that there is a set W α (for every ordinal α), such that x ∈ W α if and only if x is a tree of depth < α. If α = 0, then W α must be empty; if α is infinite then W α = T since all trees have a finite depth. If n is finite, then W n+1 = T n .

Inria

The principle of induction of COQ allows us to define a function of any type; but in Bourbaki, we are limited to sets (in particular, we cannot define a function that associates a Tree to a tree). What we can do is define a boolean, and convert it to a proposition. If zero means false and one means true, then the min function corresponds to boolean or. We first state a lemma that says that our function f takes only 0 and 1 as values. We then get: the tree (0, n) is positive if and only if n is non-zero, the tree (1, x) is positive if and only if x is positive, and (2, (x, x )) is positive if and only if x and x are positive. We define here by induction the size of a tree.

Definition tree_size := tree_rec id id cmax. We define now a function that maps a Tree to a tree. This is a bijection. It respects all the properties defined above.

José Grimm

Inria Chapter 2

Structures and isomorphisms

In the example of the introduction we had one set E, one structure s, and an axiom. We considered a second set F, a bijection g , then deduced s . We showed that the axiom was transportable: this means that if the axiom holds for E and s, if holds for F and s . We have also seen that if v is a subgroup, so is v . The way s , v , etc, are constructed depends only on the typification of s, v, etc. For instance, v is the set of all g (x) for x ∈ v. Since v is a subset of the source of g , this is well defined and is a subset of the target of g , namely F. The idea behind the typification is to provide a systematic way to transport objects. In the case of vector space E over K, there are two laws, with typification

s 1 ∈ P((E × E) × E) and s 2 ∈ P((K × E) × E); so that (s 1 , s 2 ) ∈ P((E × E) × E) × P((K × E) × E). This has the form (s 1 , s 2 ) ∈ S(E, K).
What we want to do is to formalise the quantity S(E, K). This is called "echelon construction of scheme S on E and K", where S is called an "echelon construction scheme"; for simplicity, we just say echelon for S. The relation is equivalent to "s 1 ∈ S 1 (E, K) and s 2 ∈ S 2 (E, K)". Such a relation is called a typification of the letters s 1 and s 2 . There is a small problem here: Bourbaki assumes that S 1 and S 2 are echelons on two terms (this makes sense, as they are applied to two terms). However S 1 (E, K) is independent of K, so is morally an echelon on one term. It is however possible to modify S 1 such that it has the correct size, without changing the value. The problem is now: if we transport our terms with the modified echelon, do we get the same value or not?

For this reason, we shall give two implementations; in the first variant an echelon will be a tree and there will be uniqueness. The second implementation a linearized version of the tree, i.e., a list with some properties.

We proceed as follows: take

A 1 = E, A 2 = A 1 × A 1 , A 3 = A 2 × A 1 , A 4 = P(A 3 ), A 5 = K, A 6 = A 5 ×A 1 , A 7 = A 6 ×A 1 , A 8 = P(A 7 ), A 9 = A 4 ×A 8 . Now S(E, K) is the last set in the list, namely A 9 .
In order to define S as a function of two arguments, we replace E by x 1 , and K by x 2 . We can reduce the length of this character string: first remove every equal sign and what is on the left (this is redundant information); second, in the case of a product, just keep the indices; in the case of a powerset, keep the index, followed by 0, otherwise keep the index, preceded by zero (this works as no index is zero). We get 0,1,1,1,2,1,...,4,8, a list of 18 integers. Add some parentheses; we get (0, 1), (1,1), [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF]1), [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]0), (0, 2), [START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF]1), [START_REF] Garillot | Packaging Mathematical Structures[END_REF]1), [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets[END_REF]0), [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF][START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF].

We get a list of 9 pairs of integers. This is an example of an echelon, in the Bourbaki sense.

We shall consider below the case of (0,1), (0,2), (1,0), [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]0), [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF]0), [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF][START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF], denoted S 3 , and show that this gives S 3 (E, F) = P(P(E))×P(F). Bourbaki considers also (0,2), (0,1), (1,0), (2,0), (4,0), [START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF][START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF], denoted S 4 , says S 4 (E, F) = S 3 (E, F) and deduces « Distinct schemes may therefore give rise to the same echelon on the same terms. » There is a simpler example: if we add [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF][START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF] (the last term of S 3 ) to the right of S 4 we get a longer scheme with the same behavior. This new scheme is not minimal (some sets are useless). The scheme (0,1), (1,1), (1,1), [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF][START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF] is not minimal, as it could be replaced by (0,1), (1,1), [START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF][START_REF] Bourbaki | Éléments de mathématiques, I les structures fondamentales de l'analyse[END_REF]. In the example above both schemes are minimal, yet are different and behave the same.

Add now before each pair its index: we get (0,0,1),(1,1,1),(2,2,1),(3,3,0),(4,0,2),(5,5,1),(6,6,1), [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets[END_REF][START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets[END_REF]0), [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF][START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF][START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF].

What we get now is a list of triples. If the triple is (i , a, b), we must have a ≤ i and b ≤ i (except when a = 0, case where 1 ≤ b ≤ 2 is required in order to apply it to n terms). In the first chapter, we manipulated lots of triples, of the form ((a, b), c). Here they are of the form (i , (a, b)). With this interpretation, the set of these elements is a functional graph, whose domain is a subset of N, and whose range is a subset of N × N.

Echelons

« An echelon construction scheme is a sequence c 1 , c 2 , . . . , c m of ordered pairs of natural integers c i = (a i , b i ) satisfying the following conditions: (a) if b i = 0, then 1 ≤ a i ≤ i -1, (b) if a i = 0 and b i = 0, then 1 ≤ a i ≤ i -1 and 1 ≤ b i ≤ i -1.
If n is the largest of the integers b i which appear in the pairs (0, b i ) then c 1 , c 2 , . . . , c m is said to be an echelon construction scheme on n terms. » As mentioned above, an echelon will be a functional graph, with some properties. The integer m is called the length of the list, and n the size of the list. Because our indices start at zero, the condition 1 ≤ a i ≤ i -1 becomes 1 ≤ a i ≤ i ; we say that a i is good (with respect to i ); this relation implies 0 ≤ a i -1 < i . It particular, it is false when i = 0. Thus a 1 = 0 and b 1 > 0, and the size is well defined (provided that m non-zero). Our definition of the size works in any case (the size of the empty list being zero; it is non-zero otherwise). In the Appendix to Chapter IV, in a footnote, Bourbaki explains how to build a scheme from other schemes, so that s

(E) = P(s(E)) or s (E) = s 1 (E) × s 2 (E).
We consider a third case, it produces an echelon of length one from an integer.

Definition Ech_base n := Lg \1c (fun z => (J \0c n)). Lemma Ech_base_prop n (c:= Ech_base n): natp n -> \0c <c n -> [/\ echelon c, Vg c \0c = J \0c n, \0c <c slength c & esize c = n].
The second operation is easy; if s is of length m, it suffices to add (m, 0) at the end. The third operation is more complex. If m 1 and m 2 are the sizes of s 1 and s 2 , we construct a list of size s 1 + s 2 + 1 formed of s 1 , a modified version of s 2 and a final term. If m 1 and m 2 are zero, this final term is (0,0), and the construction is invalid. If m 1 is non-zero, m 2 is zero, we get an object that evaluates as s 1 (E) × s 2 (E).

Definition ech_shift n v:= Yo (P v = \0c) v (Yo (Q v = \0c) (J (P v +c n) \0c) (J (P v +c n) (Q v +c n))). Definition ech_product1 f g n m i:= Yo (i <c n) (Vg f i) (Yo (i = n +c m) (J n (n +c m)) (ech_shift n (Vg g (i -c n)))). Definition Ech_product f g := let n := (slength f) in let m := (slength g) in Lg (csucc (n +c m))(ech_product1 f g n m). Lemma ech_product_prop1 f g n m i (v:= ech_product1 f g n m): natp n -> natp m -> [/\ i <c n -> v i = (Vg f i), v(n +c m) = (J n (n +c m)) & i <c m -> v (n +c i) = ech_shift n (Vg g i)].
Lemma Ech_product_prop f g (n := slength f) (m:= slength g)

(h := Ech_product f g): echelon f -> echelon g -> \0c <c n -> [/\ echelon h, slength h = csucc (n +c m), esize h = cmax (esize f) (esize g) & [/\ forall i, i <c n -> Vg h i = (Vg f i), Vg h (n +c m) = (J n (n +c m)) , forall i, i <c m -> Vg h (n +c i) = ech_shift n (Vg g i) & forall i, n <=c i -> i <c n +c m -> Vg h i = ech_shift n (Vg g (i -c n))]].
What we would like to do now is: define a function that maps an echelon to a tree, and conversely. This second operation is easy to do. The converse operation is a bit trickier. It requires a new induction principle. As previously, we consider three functions h 1 , h 2 and h 3 . We combine them into a single function p, that takes 3 arguments; f , a, b, and is defined by: if a = 0, then h The idea is to define by transfinite induction a function f on the set of all integers, then restrict its graph to I m , where m is the domain of the echelon. The resulting list is the unique one that satisfies the relation. We then state:

) : [/\ forall n, natp n -> f (Tb n) = Ech_base (csucc n), forall x, treep x -> f (Tp x) = Ech_powerset (f x) & forall x y, treep x -> treep y -> f (Tx x y) = Ech_product (f x) (f y)].
if c i = (a, b) then in case a = 0, we have 1 ≤ b ≤ n and f i = h 1 (b); in case b = 0, we have 1 ≤ a ≤ i and f i = h 2 ( f (a)),
= Q (Vg c i) in [/\ a = \0c -> Vg f i = h1 b, b = \0c -> Vg f i = h2 (Vl f a) & a <> \0c -> b <> \0c -> Vg f i = h3 (Vl f a) (Vl f b)]) -> f = echelon_recdef c. Lemma erecdef_prop2 c (m := slength c)(f := echelon_recdef c) (n:= esize c): echelon c -> forall i, i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> [/\ \1c <=c b, b <=c n & Vg f i = (h1 b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg f i = h2 (Vl f a) ] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg f i = h3 (Vl f a) (Vl f b)]].
Define g (c) as f (i ) where i is the length of c.

If c = P(c) then g (c ) = h 2 (g (c)), if c = c ×c , then g (c ) = h 3 (g (c), g (c )
). The first property is easy; the second is a bit more complicated because the product of two echelon is non-trivial. Example. Take h 1 (x) = T b (x -1), h 2 = T p and h 3 = T x . It is easy to show, by induction, that the result is a list of trees. We now rewrite this result using Trees.

Lemma ET_val1 c i (f := echelon_to_trees c): echelon c -> i <c (slength c) -> P (Vg c i) = \0c -> exists n, Q (Vg c i) = csucc (nat_to_B n) /\ Vg f i = Tree_to_tree (Tbase n). Lemma ET_val2 c i (f := echelon_to_trees c): echelon c -> i <c (slength c) -> Q (Vg c i) = \0c -> exists2 E, Tree_to_tree E = (Vl f (P (Vg c i))) & Tree_to_tree (Tpowerset E) = Vg f i. Lemma ET_val3 c i (f := echelon_to_trees c) (a := (P (Vg c i))) (b := Q (Vg c i)): echelon c -> i <c (slength c) -> a <> \0c -> b <> \0c -> exists E F, [ /\ Tree_to_Tree E = Vl f a, Tree_to_Tree F = Vl f b& Tree_to_Tree (Tproduct E F) = Vg f i ].
We are now ready to continue with the Bourbaki text.

Inria « Given an echelon construction scheme S = (c 1 , c 2 , . . . , c m ) on n terms, and given n terms E 1 , E 2 , . . . , E n in a theory T which is stronger than the theory of sets, an echelon construction of scheme S on E 1 , . . . , E n is defined to be a sequence A 1 , A 2 , . . . , A m of m terms in the theory T , defined step by step by the following conditions:

(a) if c i = (0, b i ), then A i is the term E b i , (b) if c i = (a i , 0), then A i is the term P(A a i ), (c) if c i = (a i , b i ) where a i = 0 and b i = 0, then A i is the term A a i × A b i .
The last term A m of the echelon construction of scheme S on E 1 , . . . , E n is called the echelon of scheme S on the base sets E 1 , . . . , E n ; in the general arguments that follow, it will be denoted by the notation S(E 1 , . . . , E n ). »

We shall denote by S(E) the list of the A i , so that S(E) = S(E) m . The lemmas that follow are trivial. We can evaluate a tree in the same way as an echelon. If T is a tree, converted to an echelon S, then, whatever E, T(E) = S(E). Lemma echelon_of_base_of_tree t E: treep t -> echelon_of_base (tree_to_echelon t) E = tree_value E t.

Tree evaluation is injective. This means that if we have two trees, T and T , such that, for every E, T(E) = T (E) holds, then T = T . In what follows, we consider a property P, and the assumption H P that, whenever E satisfies P, then T(E) = T (E). We can make strong assumptions on P, for, if Q is such that Q =⇒ P, then H Q implies H P . We may for instance assume that E is a list of length m with n < m and n < m, where n and n are the sizes of T and T . If the condition fails, at least one of T(E) and T (E) is not correctly defined (note that E 3 is defined even if E = , but whether or not this is equal to E 4 is left unspecified). We may assume that E has length 1 + max(n, n ), for we can always restrict the list to a smaller one. We may assume that the elements of E are 1 and 3. This means that only a finite number of lists have to be checked.

The proof is by induction. There are six cases to consider, since T can be T b (n), T p (x), T x (x, x ), likewise for T which could be T b (m), T p (y), T x (y, y ). The evaluation has the form E n , P(X), X × X , E m , P(Y), Y × Y . Assume E n = E m ; in order to get n = m, it suffices to allow two distinct values for E. Assume P(X) = P(Y); then X = Y, since X ∈ P(X), thus X ∈ P(Y), so X ⊂ Y, we conclude by extensionality. Assume X × X = Y × Y . It could be that X and Y are empty. We exclude this case by assuming E i non-empty, so that T(E) is non-empty, whatever T. In this case X = Y and X = Y . We now must show that E n = P(X) is absurd. Here we take E n = 3 (our proof relies in the fact that 0 = , 1 = {0}, 2 = {0, 1} and 3 = {0, 1, 2}; but obviously a set with three elements cannot be a power set, since the cardinal of a power set is a power of two). Note that P(X) = Y × Y . If pairs are defined via an axiom (as was the case in earlier versions of Bourbaki), this statement is hard to prove (maybe false with our limited choice of sets for E). However, defining pairs as doubletons ensures that the empty set is not a pair; it belongs to the power set, but not to the product. Finally, we have to exclude the case E n = Y × Y . It suffices to take E n = 1 (recall that 1 is the powers et of 0).

Lemma tree_val_ne n E : (forall i, i <c n -> nonempty (Vg E i)) -> forall t, treep t -> tree_size t <c n -> nonempty(tree_value E t).

Lemma powerset_injective: injective powerset. The proof is a bit long (160 lines) but is straight forward.

Definition slist_good n m E := [/\ slistp E, slength E = csucc(cmax n m) & forall i, i <c slength E -> (Vg E i) = \1c \/ (Vg E i) = \3c ].

Inria

Lemma tree_value_injective t1 t2: treep t1 -> treep t2 -> (forall E, slist_good (tree_size t1) (tree_size t2) E -> tree_value E t1 = tree_value E t2) -> t1 = t2.

Let S be an echelon converted to a tree list T 1 . . . T m . Then A i = T i (E) for every index i . In particular S(E), the last element of the list is T m (E). If S is another echelon such that the last tree T k is equal to T m , then S(E) = S (E). Lemma tree_value_commmute_bis E c1 c2: echelon c1 -> echelon c2 -> \0c <c slength c1 -> \0c <c slength c2 -> echelon_to_tree c1 = echelon_to_tree c2 -> echelon_of_base c1 E = echelon_of_base c2 E.

Example

Bourbaki considers the scheme (0, 1), (0, 2), (1, 0), (3, 0), (2, 0), [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF][START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF], and a similar one. This requires to introduce the integer 6 (the length of the list) and some properties (omitted here).

Definition card_six := csucc card_five. Notation "\5c" := card_five. Notation "\6c" := card_six.

We define now the lists a, b, and a, b, c, d , e, f of length 2 and 6, then show that we have two echelons, of size 2. Definition scheme_ex1 := slist6 (J \0c \1c) (J \0c \2c) (J \1c \0c) (J \3c \0c) (J \2c \0c) (J \4c \5c).

(b) if c i = (a i , 0), so that A i = P(A a i ) and A i = P(A a i ) then A i is the canonical extension ĝa i of g a i to the set of subsets (Chapter II, §5, no. 1),

(c) if c i = (a i , b i ) where a i = 0 and b i = 0, so that A i = A a i × A b i and A i = A a i × A b i
, then A i is the canonical extension g a i × g b i of g a i and g b i to A a i × A b i (Chapter II, §3, no. 9).

The last term g m of this sequence is called the canonical extension, with scheme S, of the mappings f 1 , . . . , f n , and will be denoted by 〈 f 1 , . . . , f n 〉 S . »

The definition is as above. We can define the canonical extension of a tree in a similar but easier way. One has: if c is a scheme, f a family of functions, or whatever, if T is the tree of c, then 〈 f 〉 c = T( f ). More precisely, if c is of length m, and if the trees associated are T 1 , . . . , T m , then g i = T i ( f ) for every i . The important function is c( f ), namely g m , the important tree is T = T m , and we have: if c is another scheme, with tree T , then if T = T , then 〈 f 〉 c = 〈 f 〉 c . Recall that, in order to prove T = T , it suffices to check c(E) = c (E) for a finite family of sets E. Consider a third family E i , a sequence f i such that f i ∈ F (E i , E i ), and construct

g i ∈ F (A i ; A i ). Since f i • f i ∈ F (E i , E i )
one can also define g i . It happens that g i = g i •g i . Finally, assume f i surjective, let f i be the inverse of f i . In this case, g i is the identity function, so that g i is the inverse of g i .

Lemma Eextension_prop_comp c f f' E E' E'' (m := slength c) (n:= esize c) (f'' := Lg n (fun z => (Vg f' z) \co (Vg f z))) (g := echelon_extension c f) (g' := echelon_extension c f') (g'':= echelon_extension c f''): echelon c -> (forall i, i <c n -> inc (Vg f i) (functions (Vg E i) (Vg E' i))) -> (forall i, i <c n -> inc (Vg f' i) (functions (Vg E' i) (Vg E'' i))) -> forall i, i <c m -> Vg g'' i = (Vg g' i) \co (Vg g i).
Lemma Eextension_prop_composable c f f' (g := echelon_extension c f) (g' := echelon_extension c f'): echelon c -> (forall i, i <c esize c -> (Vg f' i) \coP (Vg f i)) -> forall i,i <c (slength c) -> (Vg g' i) \coP (Vg g i).

Transportable relations

« Let T be a theory which is stronger than the theory of sets, let x 1 , . . . , x n , s 1 . . . , s p be distinct letters which are distinct from the constants of T , and let A 1 . . . , A m be terms in T in which none of the letters x i (1 ≤ i ≤ n) and s j (1 ≤ j ≤ p) appears. Let S 1 , . . . S p be echelon construction schemes on n + m terms. Then the relation Täx 1 , . . . , x n , s 1 , . . . , s p ä:

(2.1) "s 1 ∈ S 1
s j = 〈 f 1 , . . . , f n , Id 1 , . . . , Id m 〉 S j (s j ) (1 ≤ j ≤ p).
There is an analogous but simpler definition in the case where there is no auxiliary set.»

For simplicity, we omitted the arguments, in the definition of T, they are, whatever the index, the list x 1 , . . . , x n , A 1 , . . . , A m . We have written f ∈ B(x, y) instead of " f is a bijection of x onto y".

Example: « if n = p = 2 and the typification T is "s 1 ∈ x 1 and s 2 ∈ x 1 " the relation s 1 = s 2 is transportable; the relation x 1 = x 2 is not transportable.» There is no auxiliary set in this example (m = 0). We have S 1 (x 1 , x 2 ) = x 1 and S 2 (x 1 , x 2 ) = x 1 . From this, we deduce T 1 = T 2 = T b (0) where T 1 and T 2 are the trees associated to S 1 and S 2 .

In this example, transportability means: "s 1 ∈ x 1 and s 2 ∈ x 2 and f 1 is a bijection of x 1 onto y 1 and f 2 is a bijection of x 2 onto y 2 " implies R(x 1 , x 2 , s 1 , s 2 ) ⇐⇒ R(y 1 , y 2 , s 1 , s 2 ). Take for R the relation x 1 = x 2 . We get x 1 = x 2 ⇐⇒ y 1 = y 2 . This is a relation with a lot of free variables, in order to check its validity, we have to quantify over everything. We eliminate s 1 and s 2 by saying that x 1 and x 2 are non-empty, we eliminate f 1 and f 2 by sating that x 1 is equipotent to y 1 and x 2 is equipotent to y 2 . For instance, we can take singleton. If x 1 = {a 1 }, x 2 = {a z }, etc, we get a 1 = a 2 ⇐⇒ b 1 = b 2 , and there are no more conditions; so the relation is false.

Take for R the relation s 1 = s 2 and modify our typification to be "s 1 ∈ x 1 and s 2 ∈ x 2 " (this makes x 2 useful). We get s 1 = s 2 ⇐⇒ s 1 = s 2 . We now use the fact that s 1 depends only on T 1 , not the unknown S 1 , and T 1 = T b (0). This means s 1 = f 1 (s 1 ), similarly s 2 = f 2 (s 2 ). Now we get

s 1 = s 2 ⇐⇒ f 1 (s 1 ) = f 2 (s 2 )
. Take the same sets as above, x 1 = {a 1 }, etc. Then we get s 1 = a 1 , etc, thus a 1 = a 2 ⇐⇒ b 1 = b 2 . Again the relation is not transportable. However, from s 2 ∈ x 2 we get s 2 = f 1 (s 2 ) and the relation becomes

s 1 = s 2 ⇐⇒ f 1 (s 1 ) = f 1 (s 2 )
. This holds by injectivity of f 1 , and the relation is transportable. This example explains how to formalise the notion of transportability: we have to quantify over everything: the x i , s i , f i , y i , the A i , the sizes n, p, etc. Note that A has a different status than x: it may depend on a parameter t , in particular, since R may depend on t , it may depend on A. As the example shows, the size of S i should be ≤ n + m (it makes no sense to arbitrarily increase the size in order to meet n + m.

We first must define the list x 1 , . . . , x n , A 1 , . . . , A m , let's denote it X, that appears in T. This is the concatenation of the lists x and A. We define F, the list f 1 , . . . , f n , Id 1 , . . . , Id m , and show that 〈F〉 S is a bijection S(X) → S(Y), where Y is like X, with y i instead of x i , provided that f i is a bijection x i → y i , and S is a non-trivial echelon of sise ≤ n + m. In case n = 0, 〈F〉 S is the identity function. Let S be the list S 1 , . . . , S p . We consider H(n, A, S) to be: n is an integer A and S are lists, for each i , S i is an echelon of size ≤ n + m (where m is the length of A). Now, a typification (n, A, S, x, s) is a bunch of objects such that H(n, A, S) holds, x is a list of length n, s a list of size p, moreover (2.1) holds.

Note: assume that S is empty; so that neither S(X) not 〈F〉 S makes sense; in this case we use the empty set instead of S(X). This means that s ∈ S(X) will be false, and 〈F〉 S will not be used. Note also: in what follows, Bourbaki considers only the case p = 1. For this reason, we shall give two pairs of definitions: the general case (with a suffix g), and the case p = 1, where S and s are not lists.

Species of structures

« Let T be a theory which is stronger than the theory of sets. A species of structures in T is a text Σ formed of the following assemblies:

(1) a certain number of letters x 1 , . . . , x n , s, distinct from each other and from the constants of T ; x 1 , . . . , x n are calle the principal base sets of the species of structure Σ;

(2) a certain number of terms A 1 , . . . , A m in T in which none of the letters x 1 , . . . , x n , s appears, and which are called the auxiliary base sets of Σ; Σ possibly contains no auxiliary base sets (but it must contain has at least one principal base set);

(3) a typification Täx 1 , . . . , x n , sä:

s ∈ S(x 1 , . . . , x n , A 1 , . . . A m ),
where S is an echelon construction scheme on n +m terms; Täx 1 , . . . , x n , sä is called the typical characterization of the species of structure Σ.

(4) a relation Räx 1 , . . . , x n , sä which is transportable (in T ) with respect to the typification T, the x i being the principle base sets and the A h the auxiliary base set; R is called the axiom of the species of structures Σ.

The theory T Σ which has the same axiom schemes as T and whose explicit axioms are those of T , together with the axiom "T and R", is called the theory of species of structures Σ. The constants of T Σ are therefore the constants of T and the letters that appear in T or R. One calls theory of species Σ the theory T Σ having the same axiom schemes as T and whose ecxplicit axioms are that of T and the axiom "T and R"; the constants of T Σ are hence the constants of T and the letters that appear in T or in R.» « Let T be a theory which is stronger than T , and let E 1 , . . . , E n , U be terms of T . In the theory cT , U is said to be a structure of species Σ on the principal base sets E 1 , . . . , E m with A 1 , . . . , A m as auxiliary base sets, if the relation TäE 1 . . . , E n , Uä and RäE 1 , . . . , E n , Uä is a theorem in T . When this is so, then for every theorem Bäx 1 , . . . , x n , sä in the theory T Σ the relation BäE 1 . . . , E n , Uä is a theorem in T . In T Σ the constant s is called the generic structure of species Σ.

In the theory T , the principal base sets E 1 , . . . , E n are said to be endowed with the structure U. Clearly, U ∈ S(E 1 , . . . , E n , A 1 , . . . , A m ). The set of elements V of S(E 1 , . . . , E n , A 1 , . . . , A m ) which satisfy the relation RäE 1 , . . . , E n , Vä is therefore the set of structures of species Si g ma on E 1 , . . . , E n , (and it may be empty).» For us, a species of structure Σ will be: n, A, S, R, where n is an integer, A a list of length m, and S an echelon of length ≤ n + m, R is transportable. With this definition, T(x, s) becomes equivalent to: x is a length of size n and s ∈ S(x). Note that x and s are not part of Σ.

Inverse limits and direct limits

In this chapter we implement §7 of chapter III (Ordered Sets, Cardinals, Integers) of Book I (Theory of Sets) of the work of Bourbaki [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]. We consider a family of sets (E i ) i ∈I and a family of functions E i → E j ; in case we have a function f : E i → E j and a function g : E j → E k , then g • f is the function E i → E k . The function f exists when i ≤ j , so that we require ≤ to be transitive. We also assume that the function E i → E i is the identity function of E i , this implies that ≤ is reflexive on I, thus is a preorder on I. One can take the product or the quotient, and obtain what is called the "inverse" or "direct" limit. We shall use here the alternate names "projective limit" and "inductive limit" (unless when quoting Bourbaki).

Inverse limits

« Let I be a preordered set and let (E α ) α∈I be a family of sets indexed by I. For each pair (α, β) of elements of I such that α ≤ β, let f αβ be a mapping of E β into E α . Suppose that the f αβ satisfy the following conditions:

(LP I ) The relations α ≤ β ≤ γ imply f αγ = f αβ • f βγ . (LP II ) For each α ∈ I, f αα is the identity mapping of E α .
By abuse of language, the pair ((E α ), ( f αβ )) (usually denoted by (E α , f αβ )) is called an inverse system of sets, relative to the index set I. » It is implicit in (LP I ) that the three indices belong to I. So, if r is the graph of ≤ on I, by assumption, r is a preorder on I, and it makes sense to consider the family f i j with domain r . This means that ((E i ) i ∈I , ( f i j ) i j ∈r ) is a pair of sets. For simplicity, we shall add to this pair the domains of E and f (i.e., I and r ). So, a (projective or inductive) system will be a quadruple, together with the conditions (LP I ), (LP II ), the fact that f i j is a function, and that r is a preorder on I. Packing the sets and the relation in a single object S will make lemmas shorter, but S is no more a set: we loose extensionality (two systems with the same data are not always equal), and we cannot consider families of systems (see Exercise 1 for instance). « Let G = α∈I E α be the product of the family of sets (E α ) α∈I , and let E denote the subset of G consisting in all x which satisfy each of the relations (3.1) pr

α x = f αβ (pr β x)
for each pair of indices (α, β) such that α ≤ β. E is said to be the inverse limit of the family (E α ) α∈I with respect to the family of mappings ( f αβ ), and we write E = lim ← --(E α , f αβ ) or simply Inria Definition prl_restr S J (H: sub J (psI S)) : projective_system. Definition projective_limit_restr S J (H: sub J (psI S)):= projective_limit (prl_restr H).

Lemma prl_restr_prop S J (H: sub J (psI S)): projective_system_on (prl_restr H) (restr (psE S) J) J (induced_order (psr S) J) (restr (psf S) (induced_order (psr S) J)). Lemma prl_restr_Iv2 S S' J (h1: sub J (psI S))(h2: sub J (psI S')):

prl_same_data S S' -> prl_same_data (prl_restr h1) (prl_restr h2).

« For each x ∈ E the element

(3.3) g (x) = ( f α (x)) α∈J
belongs to E by virtue of (3.2). The mapping g : E → E so defined is called canonical. »

Here E is lim ← --S, E is lim ← --S , the projective limit of the restricted system. Note that g (x) is the functional graph, defined on J that maps i to f i (x). Since f i is the restriction of pr i , we have f i (x) = pr i x, and, as mentioned above, f i (x) = x i . So g (x) is just the restriction of x to J.

Definition prl_restr_canonical S J (H: sub J (psI S)):= Lf (restr^~J) (projective_limit S) (projective_limit_restr H).

Lemma prl_restr_canonical_ax S J (H: sub J (psI S)) : lf_axiom (restr^~J) (projective_limit S) (projective_limit_restr H).

Lemma prl_restr_canonical_fp S J (H: sub J (psI S)): function_prop (prl_restr_canonical H) (projective_limit S) (projective_limit_restr H).

Lemma prl_restr_canonical_fun_ev S J (H: sub J (psI S)) x: inc x (projective_limit S) -> Vf (prl_restr_canonical H) x = restr x J. Lemma prl_restr_canonical_fun_ev2 S J (H: sub J (psI S)) x j: inc x (projective_limit S) -> inc j J -> Vg (Vf (prl_restr_canonical H) x) j = Vg x j.

« If J is a subset of J, and E the inverse limit of the family (E α ) α∈J , and if g : E → E and g : E → E are the canonical mappings, then by definition we have

(3.4) g = g • g . »
In the code that follows, we use K and K instead of J and J . Assume K ⊂ K ⊂ I. We define S to be S restricted to K, and S to be S restricted to K (note that H 2 , a proof of K ⊂ K, is also a proof of K ⊂ I(S ), where I(S ) is the index set of S ). We can also consider S as the restriction of S to K (since K ⊂ I). These two systems have the same index set, thus the same order, thus the same data.

Lemma projective_limit_restr_double_Iv S K K' (H1:sub K (psI S)) (H2: sub K' K): prl_same_data (prl_restr (H2: sub K' (psI (prl_restr H1)))) (prl_restr (sub_trans H2 H1)).

Lemma projective_limit_restr_double S K K' (H1:sub K (psI S)) (H2: sub K' K): projective_limit_restr (H2: sub K' (psI (prl_restr H1))) = projective_limit_restr (sub_trans H2 H1).

Lemma prl_restr_canonical_comp S K K' (H1:sub K (psI S)) (H2: sub K' K) (g := prl_restr_canonical H1) (g' := prl_restr_canonical (H2: sub K' (psI (prl_restr H1)))) (g'' := prl_restr_canonical (sub_trans H2 H1)): g' \coP g /\ g' \co g = g''.

Inverse systems of mappings

Proposition 1. « Let I be an ordered set, let (E α , f αβ ) be an inverse system of sets relative to I, let E = lim ← --E α be its inverse limit, and for each α ∈ I let

f α : E → E α
be the canonical mapping. For each α ∈ I, let u α be a mapping of a set F into E α such that

(3.5) f αβ • u β = u α whenever α ≤ β.
Then (a) there exists a unique mapping u of F into E such that

(3.6) u α = f α • u for all α ∈ I;
(b) the mapping u is injective if and only if, for each pair of distinct elements y, z of F, there exists α ∈ I such that u α (y) = u α (z). » g = g'. Lemma prl_map_ax S u F : prl_map_compat S u F -> lf_axiom (prl_map_val S u) F (projective_limit S).

Lemma projective_map_ev S u F x i:

prl_map_compat S u F -> inc x F -> inc i (psI S) -> Vg (Vf (projective_map S u F) x) i = Vf (Vg u i) x. Lemma prl_map_prop S u F : prl_map_compat S u F -> prl_map_property S u F (projective_map S u F). Lemma prl_map_inj S u F : prl_map_compat S u F -> (injection (projective_map S u F) <-> (forall y z, inc y F -> inc z F -> y <> z -> exists2 i, inc i (psI S) & (Vf (Vg u i) y <> Vf (Vg u i) z))).
Corollary 1. « Let (E α , f αβ ) and (F α , g αβ ) be two inverse systems of sets relative to the same index set I; let E = lim ← --E α , F = lim ← --F α , and let f α (resp. g α ) be the canonical mapping of E into E α (resp. of F into F α ) for each α ∈ I. For each α ∈ I, let u α be a mapping of E α into F α such that

(3.7) u α • f αβ = g αβ • u β whenever α ≤ β.
Then there exists a unique mapping u : E → F such that

(3.8) u α • f α = g α • u whenever α ∈ I. »
Bourbaki uses the following two commutative diagrams instead of formulas

E j u j / / f i j F j g i j E i u i / / F i E u / / f i F g i E i u i / / F i
A family satisfying the assumptions is called a projective systems of mappings; the mapping u is called the projective limit of the family, and denoted by lim ← --u α . The idea is to apply Proposition 1 to v i = u i • f i and the second system.

Definition prl_map2_compat S S' u:= [/\ fgraph u, domain u = psI S, forall i, inc i (psI S) -> function_prop (Vg u i) (Vg (psE S) i) (Vg (psE S') i) & forall i j, gle (psr S) i j -> (Vg u i) \co (Vg (psf S) (J i j)) = (Vg (psf S') (J i j)) \co (Vg u j)].
Definition prl_map2_property S S' u g:= function_prop g (projective_limit S) (projective_limit S') /\ forall i, inc i (psI S) -> (Vg u i) \co (prl_can_fun S i) = (prl_can_fun S') i \co g.

Definition prl_map2_aux S u := Lg (psI S) (fun i => (Vg u i) \co (prl_can_fun S i)). Definition projective_limit_fun S S' u := projective_map S' (prl_map2_aux S u) (projective_limit S).

Lemma prl_inv_hyp_prop2 S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> (forall i, inc i (psI S) -> bijection (Vg u i)) -> bijection (projective_limit_fun S S' u).

Direct image. With the same notations as above, consider the sets M i = u i 〈E i 〉 (this is the image of u i ). This family of sets form a projective family of subsets of M i . If u is the projective limit of u i , then the image of u is a subset of the projective limit of the M i . We have not always equality: for instance, assume u i surjective, so that M i = E i and lim ← --

M i = lim ← -- E i . It may happen that u is not surjective. Definition prl_dirim_set u := Lg (domain u) (fun i => Imf (Vg u i)).
Lemma prl_direct_hyp S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> prl_subfam_hyp S' (prl_dirim_set u).

Lemma prl_dirim_prop S S' u (Hsb: prl_same_index S S') (Hc: prl_map2_compat S S' u): sub (Imf (projective_limit_fun S S' u)) (projective_limit (projective_system_subsets (prl_direct_hyp Hsb Hc))).

Proposition 3. « Let I be a preordered set, let (E α , f αβ ) be an inverse system of sets relative to I and let E = lim ← --E α . Let J be a cofinal subset of I such that J is right directed, and let E be the inverse limit of the inverse system of sets obtained from (E α , f αβ ) by restricting the index set to J. Then the canonical mapping g of E into E (no. 1, formula (3.3)) is bijective. » We also assume that, whenever x ∈ I, there is y ∈ J such that x ≤ y. Note that "cofinal" implies J ⊂ d where d is the domain of r (i.e. I).

Bourbaki claims that if f i is the canonical mapping E → E i , then g is the unique mapping E → E such that f i = f i • g . He uses the criterion of Proposition 1 for injectivity. We proceed directly: given x and y in E, show x = y given that x and y have the same restrictions. Note that x and y are functional graphs with domain I, so it suffices to show x i = y i . Since J is cofinal, there is j ∈ J such that i ≤ j ; this implies x i = f i j (x j ); the result follows since x j = y j . In order to prove that g is surjective, consider x ∈ E . This is a functional graph on J and we have to extend it. If i ∈ I, there is j ∈ J such that i ≤ j . We want x i = f i j (x j ). The trick is that the RHS is independent of j .

In the special case where I has a greatest element ω, one can take J = {ω}. In this case, E is equal to the product i ∈J E i , hence isomorphic to E ω . We give a direct proof. The isomorphism is f ω .

Lemma right_directed_ind_prop r J: preorder r -> sub J (substrate r) -> right_directed_on r J -> right_directed_on (induced_order r J) J.

Lemma prl_rest_can_cofinal_bf S J (H: sub J (psI S)): cofinal (psr S) J -> right_directed_on (psr S) J -> bijection (prl_restr_canonical H).

Lemma prl_singleton_prop S k (f := Lf (Vg ^~k) (projective_limit S) (Vg (psE S) k)):

Double Inverse Limit

Assume that we have two preordered sets, I and L, and a projective family S on I × L. Bourbaki denotes the sets by E λ α and the functions by f λµ αβ where lower indices are in I, upper indices are in L (note the vertical alignments of the indices); the order is the product, so that (3.11)

f λν αγ = f λµ αβ • f µν βγ whenever α ≤ β ≤ γ and λ ≤ µ ≤ ν.
Fix λ ∈ L. Define g λ αβ = f λλ αβ so that the previous relation becomes

(3.12) g λ αγ = g λ αβ • g λ βγ whenever α ≤ β ≤ γ.
This allows us to define S λ a projective system on E λ α indexed by I; let F λ be its projective limit. Fix λ and µ; let h λµ α = f λµ αα . This is (again by (3.11)) a projective system of mappings, let denote its limit by h λµ . We have (3.13)

h λν = h λµ • h µν whenever λ ≤ µ ≤ ν,
so that we can define a projective system S on L. The objective is to prove that lim ← --S and lim ← --S are canonically isomorphic. The techniques are the same as in Exercise 1.

Proposition 4. If (E λ α , f λµ αβ
) is an inverse system of sets relative to a product I × L of preordered sets, then (up to a canonical bijection) we have

(3.14) lim ← -- α,λ E λ α = lim ← -- λ (lim ← -- α E λ α ).
We shall define later on the double direct limit; so we start with some common lemmas.

They are prefixed by 'pidl'. The two sets I and L are I1 and I2, ordered by r1 and r2. Note: if the two sets are right directed, so is the product; the converse holds provided that no factor is empty.

Lemma prl_dl_slice_p2 x: inc x (projective_limit S) -> inc (prl_dl_slice2 x) (projective_limit prl_dl_systemS'). Lemma prl_dl_canon_bijection: bijection_prop prl_dl_can_iso (projective_limit S) (projective_limit prl_dl_systemS'). (* 58 *) End DoubleInverseLimit.

Corollary 1. Let (E λ α , f µλ αβ ) be another inverse system of sets relative to I × L and for each (α, λ) ∈ I × L let u λ α be a mapping of E λ α into E λ α such that the u λ α for an an inverse system of mappings. Then (3.15) lim ← --

α,λ u λ α = lim ← -- λ (lim ← -- α u λ α ).
Bourbaki says that « the verification is similar to that of Proposition 4. » We consider a section, with the same assumptions as above. We consider two systems S and S and a family u, satisfying (3.7). We assume that S and S have the same index set I × L. We can now define the RHS of (3.15), the arrow at the bottom of the following diagram. It is equal to the LHS (the arrow at the top of the diagram), modulo the canonical bijections of Proposition 4 (the vertical arrows). lim ← --

α,λ E λ α lim ← -- α,λ u λ α / / lim ← -- α,λ E λ α lim ← -- λ (lim ← -- α E λ α ) lim ← -- λ (lim ← -- α u λ α ) / / lim ← -- λ (lim ← -- α E λ α )
Lemma prl_dl2_res3 (* 59 *) (pl1 := projective_limit_fun S S' u) (pl2 := projective_limit_fun prl_dl2_limlim prl_dl2_limlim' prl_dl2_v_fam) (bij1 := prl_dl_can_iso or1 or2 sr1 sr2 Sr) (bij2 := prl_dl_can_iso or1 or2 sr1 sr2 Sr'): [/\ bijection bij1, bijection bij2 & pl2 \co bij1 = bij2 \co pl1]. ) is an inverse system of sets relative to I , and (up to a canonical bijection) we have (3.16) lim ← --

α λ∈L E λ α = λ∈L (lim ← -- α E λ α ).
The assumption is that we have a projective system S(l ) for every set l , and that, when l ∈ L, the order is r , so that the substrate is I. We order L by the trivial order, then define the system S.

Lemma prl_dl3_ffam_ax ij: inc ij r -> ext_map_prod_axioms L (fun l : Set => Vg (psE (fS l)) (Q ij)) (fun l => Vg (psE (fS l)) (P ij)) (fun l => graph (Vg (psf (fS l)) ij)). Lemma prl_dl3_ffam_fun ij: inc ij r -> function_prop (Vg prl_dl3_ffam ij)(prl_dl3_Ep (Q ij)) (prl_dl3_Ep (P ij)). Lemma prl_dl3_ffam_id i: inc i I -> Vg prl_dl3_ffam (J i i) = identity (prl_dl3_Ep i).

Lemma prl_dl3_ffam_comp i j k: gle r i j -> gle r j k -> Vg prl_dl3_ffam (J i j) \co Vg prl_dl3_ffam (J j k) = Vg prl_dl3_ffam (J i k).

Definition prl_dl3_systemS': projective_system. Lemma prl_dl3_systemS'_val: projective_system_on prl_dl3_systemS' (Lg I prl_dl3_Ep) I r prl_dl3_ffam.

Lemma prl_dl3_res (X := (projective_limit prl_dl3_systemS)) (Y := projective_limit prl_dl3_systemS'): bijection_prop (Lf prl_dl3_mod X Y) X Y. End DoubleInverseLimit3.

Conditions for an inverse limit to be non-empty

Proposition 5. Assume that I is directed and has a countable cofinal subset. Assume that every f i j is surjective. Then every f i is surjective. In particular, if no E i is empty, then lim ← --E i is nonempty.

Assume f i j : E j → E i is surjective. Then E i is empty if and only if E j is empty. So, either all E i are empty, or all are non-empty. In the first case, every f i (whose target is empty) is thus surjective. So we shall consider the second case.

Since f i = f i j • f j , if f j is surjective so is f i , whenever i ≤ j . Assume that I has a greatest element, say j . It suffices to show that f j is surjective. Let x j ∈ E j . Define x i = f i j (x j ), and let x be i ∈ I → x i . Since x is in the projective limit, we have f j (x) = x j , and the conclusion holds. Assume that there is a finite cofinal set; by induction the finite set has an upper bound, which must be the greatest element.

Section ProjectiveLimitNonEmpty1.

Variable S: projective_system. Hypothesis rdr:right_directed_pre (psr S). Hypothesis sjf: forall i, inc i (psr S) -> surjection (Vg (psf S) i).

Definition prl_ne1_some_nonempty := (exists2 i, inc i (psI S) & nonempty(Vg (psE S) i)).

Lemma prl_ne1_allE_ne: prl_ne1_some_nonempty -> forall i, inc i (psI S) -> nonempty(Vg (psE S) i). Lemma prl_ne1_res1: ~prl_ne1_some_nonempty -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).

Example 2. Suppose all the E i equal to F, and take for f i j the identity. We get an inductive system S; let E be the limit. The relation C S (x, i ) = C S (y, j ) simplifies to x = y (since there is k such that i ≤ k and j ≤ k). Let f (x) = pr 1 R(x) ; this induces an injection lim --→ S → F. It is surjective when I is non-empty. Bourbaki identifies lim --→ S and F. Inria Lemma 1. Let S be an inductive system, E the limit, f i the canonical function. « (i) Let (x (i ) ) 1≤i ≤n be a finite system of elements of E. Then there exists α ∈ I and a finite system (x (i ) α ) 1≤i ≤n of elements of E α such that x (i ) = f α (x (i ) α ) for 1 ≤ i ≤ n. (ii) Let (y (i ) α ) 1≤i ≤n be a finite system of elements of some E α . If f α (y (i ) α ) = f α (y ( j ) α ) for each pair of indices (i , j ), then there exists β ≥ α such that f βα (y (i ) α ) = f βα (y ( j ) α ) for every pair (i , j ). » Note: we replace 1 ≤ i ≤ n by I ∈ F, where F is a finite set. In case n = 0, point (ii) becomes trivial and (i) holds when I is non-empty. Bourbaki uses the lemma only in the case n = 2; we never use it. The key relation is: every non-empty finite subset of I has an upper bound.

Proof of (i). We consider a family (

X i ) i ∈K of elements of E. Let R(X i ) = (x i , b i ), where b i ∈ I and x i ∈ E b i . Let Y i = f ab i (x i ). Then X i = f a (Y i ), provided that b i ≤ a. It suffices to choose a large enough. Lemma finite_preorder_directed_bounded r I E: preorder r -> substrate r = I -> right_directed_on r I -> nonempty E -> finite_set E -> sub E I -> exists2 x, inc x I & forall y, inc y E -> gle r y x. Lemma inl_Lemma5_1i S X (K:= domain X) (Y := fun a => Lg K (fun i => Vf (Vg (isf S) (J (Q (rep (Vg X i))) a)) (P (rep (Vg X i))))): fgraph X -> finite_set K -> nonempty K -> (forall i, inc i K -> inc (Vg X i) (inductive_limit S)) -> exists2 a, inc a (isI S) & [/\ fgraph (Y a), domain (Y a) = K & forall i, inc i K -> Vg X i = Vf (inl_can_fun S a) (Vg (Y a) i) ].
Definition constant_fun_on f X := forall i j, inc i X -> inc j X -> Vf f i = Vf f j.

Lemma inl_Lemma5_1ii S i X: inc i (isI S) -> sub X (Vg (isE S) i) -> finite_set X -> constant_fun_on (inl_can_fun S i) X -> exists2 j, gle (isr S) i j & constant_fun_on (Vg (isf S) (J i j)) X.

Direct systems of mappings

Proposition 6. (This is the equivalent of Proposition 1 for inductive systems). We consider an inductive system S, the inductive limit E, the canonical mapping f i . For each i ∈ I we assume there exists a function u

i : E i → F such that (3.21) u j • f j i = u i whenever i ≤ j.
Then (a) there exists a unique mapping u of E into F such that (3.22)

u i = u • f i for all i ∈ I.
(b) u is surjective if and only if F is the union of the sets u i (E i ).

(c) u is injective if and only if for each i ∈ I, the relations x ∈ E i , y ∈ E i , u i (x) = u i (y) imply that there exists j ≥ i such that f j i (x) = f j i (y).

(inductive_limit inl_remark_S) inl_remark_U.

End InlRemark.

Corollary 1.

[Compare with corollary 1 of Proposition 1]. « Let (E α , f βα ) and (F α , g βα ) be two direct systems of sets relative to the same index set I; let E = lim --→ E α , F = lim --→ F α , and for each α ∈ I let f α (resp. g α ) be the canonical mapping of E α (resp. F α ) into E (resp. F). For each α ∈ I let u α be a mapping of E α into F α such that (3.23)

g βα • u α = u β • f βα whenever α ≤ β.
Then there exists a unique mapping u : E → F such that

(3.24) g α • u α = u • f α whenever α ∈ I.
A family of functions that satisfies the conditions of Corollary 1 is called a direct system of mappings of (E α , f βα ) into (F α , g βα ) and the mapping defined by Corollary 1 is called the direct limit of the family (u α ) and is written u = lim --→ u α when there is no risk af ambiguity. » The associated commutative diagrams are

E i u i / / f j i F i g j i E j u j / / F j E i u i / / f i F i g i E u / / F
The idea is to apply Proposition 6 to the functions g i • u i .

Definition inl_map2_compat S S' u := [/\ fgraph u, domain u = isI S, forall i, inc i (isI S) -> function_prop (Vg u i) (Vg (isE S) i) (Vg (isE S') i) & forall i j, gle (isr S) i j -> Vg (isf S') (J i j) \co Vg u i = Vg u j \co Vg (isf S) (J i j) ].

Definition inl_map2_property S S' u g := function_prop g (inductive_limit S) (inductive_limit S') /\ forall i, inc i (isI S) -> (inl_can_fun S' i) \co (Vg u i) = g \co (inl_can_fun S) i.

Definition inl_map2_aux S u := Lg (psI S) (fun i => (inl_can_fun S i) \co (Vg u i)).

Lemma inl_map2_compat_prop0 S S' u x i j:

inl_same_index S S' -> inl_map2_compat S S' u -> inc x (Vg (isE S) i) -> gle (isr S) i j -> Vf (Vg (isf S') (J i j)) (Vf (Vg u i) x) = Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x).
Lemma inl_map2_compat_prop1 S S' u x i j: inl_same_index S S' -> inl_map2_compat S S' u -> inc x (Vg (isE S) i) -> gle (isr S) i j -> class (inl_equiv S') (J (Vf (Vg u i) x) i) = class (inl_equiv S') (J (Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x)) j). Lemma inl_map2_prop1 S S' u: inl_same_index S S' -> inl_map2_compat S S' u -> inl_map_compat S (inl_map2_aux S' u) (inductive_limit S').

One can apply Proposition 7, taking for u i the canonical injection j i : M i → E i . This gives an injection lim --→ j

i : lim --→ M i → lim --→ E i . It maps C M (x, i ) to C S (x, i ), for every x ∈ M i . So, lim --→ M i can be identified to a subset of lim --→ E i .
Lemma inl_subfam_compat S M (H:inl_subfam_hyp S M) (S' := (inductive_system_subsets H)) (ji := fun i => canonical_injection (Vg M i) (Vg (isE S) i)): inl_map2_compat S' S (Lg (isI S) ji).

Lemma inl_subfam_prop3 S M (H:inl_subfam_hyp S M) (S' := (inductive_system_subsets H))

(ji := fun i => canonical_injection (Vg M i) (Vg (isE S) i)) (u := (inductive_limit_fun S' S (Lg (isI S) ji))): forall i x, inc i (isI S) -> inc x (Vg M i) -> Vf u (class (inl_equiv S') (J x i)) = class (inl_equiv S) (J x i).
Lemma inl_subfam_prop4 S M (H:inl_subfam_hyp S M) (S' := (inductive_system_subsets H)) (ji := fun i => canonical_injection (Vg M i) (Vg (isE S) i)): injection_prop (inductive_limit_fun S' S (Lg (isI S) ji)) (inductive_limit S') (inductive_limit S).

Corollary. « Let (E α , f βα ) and (E α , f βα ) be two direct systems of sets, let (u α ) be a direct system of mappings, u α : E α → E α , and let u = lim --→ u α . (i) Let (M α ) be a direct system of subsets of the E α . Then (u α (M α )) is a direct system of subsets of the E α and we have

(3.26) lim --→ u α (M α ) = u(lim --→ M α ).
(ii) Let (a α ) α∈I be a family such that a α ∈ E α for each α ∈ I and f βα (a α ) = a β whenever α ≤ β.

Then the sets -1

u α (a α ) form a direct system of subsets of the E α and we have

(3.27) lim --→ -1 u α (a α ) = -1 u (a )
where a is the unique element of lim --→ E α which is the canonical image of a α for each α ∈ I. »

We open a section, introducing S, S and u, then two sections, one for (i), and one for (ii).

Section InductiveLimitCorollary.

Variables S S': inductive_system. Variable u: Set. Hypothesis sii:inl_same_index S S'. Hypothesis m2c: inl_map2_compat S S' u.

For (i), Bourbaki introduces the function v

i : M i → u i 〈M i 〉 that coincides with u i on M i . If j i is the canonical injection of u i 〈M i 〉 into E i , then u i = v i • j i . We have u i 〈M i 〉 = v i 〈M i 〉, v i is surjective, so that, by Proposition 7, lim --→ v i is surjective.
The reality is a bit more complicated.

Define M i = u i 〈M i 〉. This is obviously an inductive systems of subsets of E i .

Section InductiveLimitCorollary1.

Variable M: Set.

(inductive_limit (inl_restr H)) (inductive_limit S). Lemma inl_restr_cf_ev S J (H:sub_right_directed J (isr S)) i x: inc i J -> inc x (Vg (isE S) i) -> Vf (inl_restr_cf H) (class (inl_equiv (inl_restr H)) (Pair.J x i)) = class (inl_equiv S) (Pair.J x i).

Assume now that J ⊂ I is right directed, let S be the system obtained from S by restricting indices to J, and g the canonical functional. Assume now that J is a right directed subset of the index set of S , and define S and g accordingly. Since J is a directed subset of I we can define S and g and we have (3.28) g = g • g .

Lemma sub_right_directed_trans J J' r: preorder r -> sub_right_directed J r -> sub_right_directed J' (induced_order r J) -> sub_right_directed J' r. Lemma inl_restr_canonical_comp S J J' (H: sub_right_directed J (isr S)) (S' := inl_restr H) (H': sub_right_directed J' (isr S')) (g1 := inl_restr_cf H)(g2 := inl_restr_cf H') (g3 := inl_restr_cf (sub_right_directed_trans (is_preorder_r S) H H')): g1 \coP g2 /\ g3 = g1 \co g2. Proposition 8. « Let I be a directed set, let (E α , f βα ) be a direct system of sets relative to I, and let lim --→ E α be its direct limit. Let J be a cofinal subset of I, and let E be the direct limit of the direct system of sets obtained from (E α , f βα ) by restricting the index set to J. Then the canonical mapping g of E into E is bijective. » Note: if i and j belong to J they are bounded above in I by some k, so that there an upper bound k ∈ J of i and j . Injectivity: we use Proposition 6; assume f i (x) = f i (y), so that for some k, f ki (x) = f ki (y). Since J is cofinal, we may assume k ∈ J, and conclude. Surjectivity: we could use Proposition 6, but the direct proof is shorter. Let t = C S (x, i ), where i ∈ I, and j ∈ J such that i ≤ j . If y = f j i (x), then t = C S (y, j ) = g (C S (y, j )).

Lemma cofinal_directed S J: cofinal (isr S) J -> sub_right_directed J (isr S). Lemma inl_restr_cofinal S J (H:cofinal (isr S) J) (H' :=(cofinal_directed H)): bijection (inl_restr_cf H').

Double Direct Limit. Product of Direct Limits

[Compare with section "double inverse limit"]. Assume that we have two directed sets, I and L and an inductive family S on I × L. Bourbaki denotes the sets by E λ α and the functions by f µλ βα where lower indices are in I, upper indices are in L; the order is the product, so that 1 (3.29)

f νλ γα = f νµ γβ • f µλ βα whenever α ≤ β ≤ γ and λ ≤ µ ≤ ν.
1 The English version of Bourbaki has f µν γβ which is a typo.

Proposition 9. Bourbaki expresses the previous result by saying that, up to a canonical bijection, we have

(3.32) lim --→ α,λ E λ α = lim --→ λ (lim --→ α E λ α ).
Corollary. Let (E λ α , f µλ αβ ) be another direct system of sets relative to I × L, and for each (α, λ) ∈ I × L let u λ α be a mapping of E λ α into E λ α such that the u λ α form a direct system of mappings. Then Proposition 10. « Let (E α , f βα ) and (E α , f βα ) be two direct systems of sets, both relative to the same directed set I. Let E = lim --→ E α , E = lim --→ E α , and let f α : E α → E, f α : E α → E denote the canonical mappings, for each α ∈ I. Then (E α ×E α , f βα × f βα ) is a direct system of sets, ( f α × f α ) is a direct system of mappings and lim --→ ( f α × f α ) is a bijection

(3.34) lim --→ (E α × E α ) → (lim --→ E α ) × (lim --→ E α ). »
The first claim is obvious.

Definition inl_product_E S S':= Lg (isI S) (fun i => (Vg (isE S) i) \times (Vg (isE S') i)). Definition inl_product_f S S' := Lg (isr S) (fun i => (Vg (isf S) i) \ftimes (Vg (isf S') i)).

Definition inl_system_product S S' (sd: inl_same_index S S'): inductive_system.

Lemma inl_system_product_prop S S' (sd: inl_same_index S S'): inductive_system_on (inl_system_product sd) (inl_product_E S S') (isI S) (isr S) (inl_product_f S S').

The second property is obvious as well. Injectivity. We use Proposition 6. So consider two elements, with the same value. This means that there is an index i , elements x, y in E i , elements x , y in E i such tat f i (x) = f i (y) and f i (x ) = f i (y ). The first relation is C S (x, i ) = C S (y, i ) and says f ki (x) = f ki (y). The second relation is similar (with, perhaps a different k), but we can obviously take the same. Surjectivity. Consider an element of the product. This is a pair of classes, C S (x, i ) and C S (x , i ). We may assume i = i . Now C S ((x, x ), i ) is the desired result.

Definition inl_product_can_fun S S' := Lg (isI S) (fun i => (inl_can_fun S i) \ftimes (inl_can_fun S' i)).

Lemma inl_product_can_fun_compat S S' (sd: inl_same_index S S'): inl_map_compat (inl_system_product sd) (inl_product_can_fun S S') ((inductive_limit S) \times (inductive_limit S')).

Lemma inl_product_can_fun_bij S S' (sd: inl_same_index S S') (E:= inductive_limit S) (E' := inductive_limit S') (f:= inductive_map (inl_system_product sd) (inl_product_can_fun S S') (E \times E')): bijection_prop f (inductive_limit (inl_system_product sd)) (E \times E').

Corollary. « Let (F α , g βα ) and (F α , g βα ) be two direct systems of sets relative to I, and for each α ∈ I let u α : E α → F α , u α : E α → F α be mappings such that (u α ) and (u α ) are two direct systems of mappings. Then (u α × u α ) is a direct system of mappings, and (up to a canonical bijection) we have (3.35) lim --→ (u α × u α ) = (lim --→ u α ) × (lim --→ u α ). » Inria Let V(F, k) = f j k (m Fk (x)). We pretend that V has a minimum, under the condition that H(F, k) holds. Proof. Let A be the set of all V; since m Fk (x) ∈ E k we have A ⊂ E j . Next, A is nonempty (there is some i ∈ J, and, since I is right directed, there is k such that i ≤ k and j ≤ k, so that H({ j }, k) holds). So, by assumption A has a minimal element y. Take any element y ∈ A. There is y ∈ A such that y ≤ j y and y ≤ j y (proof below). By minimality, y = y, so y ≤ j y . So y is the least element of A.

Claim 1: V(F , k) ≤ V(F, k) when F is a subset of F and H(F , k) holds. Since f j k is increasing, it follows from m F k (x) ≤ k m Fk (x), and this holds since m is the greatest element of Y. Claim 2: V(F, k ) ≤ V(F, k) when k ≤ k . We use here (LP I ): if i ∈ J or i = j , then i ≤ k ≤ k so that f i k = f i k • f kk . As f j k is increasing, it suffices to show f kk (m Fk (x)) ≤ k m Fk (x). Write m = m Fk (x) for simplicity. As m Fk (x) is the greatest element of some Y, if suffices to show f kk (m) ∈ Y, hence, whenever i ∈ F, f i k ( f kk (m)) = x i . Now f i k (m)) = x i holds because m is in some Y. Claim 3: y exists. Assume y = V(F, k), y = V(F , k ), take F = F ∪ F , and for k an upper bound of k and k . Define y = V(F , k ). That H(F , k ) holds is clear so y ∈ A. We have V(F , k ) ≤ V(F, k ) ≤ V(F, k) and V(F , k ) ≤ V(F , k ) ≤ V(F , k ). Take (F 0 , k 0 ) minimizing V under the constraint H. By equation (3.37), if H(F, k) holds, then f j k 〈G k ∩ Y〉 = {y ∈ G j , y ≤ V}. Moreover, this set is non-empty; so that we can take an element x ∈ G j such that x ≤ V 0 . Whenever H(F, k) holds, we have x ≤ V; so that there exists u ∈ G k , x = f j k (u) and u ∈ Y Fk (x). Example: assume i ≤ j , where i ∈ J. Then H({i }, j ) holds. As j = k we have x = u ∈ Y. This says f i j (x ) = x i . Assume on the contrary j ≤ i , so that H({i }, i ) holds. Now x = f j i (u) and u ∈ Y says x i = f i i (x) = u. So x i = f i j (x ).

Extend now x to J = J ∪ { j } by defining x j = x . The previous discussion says: whenever i ≤ k are two indices in J we have x i = f i k (x k ), since this holds when the indices are in J. We have to show that for every finite non-empty subset K of J , the extension is K-coherent. Conditions (C 1 ) and (C 2 ) are easy. Condition C 3 holds as well.

Let's show (C 4 ), and consider an upper bounder k of K. Assume first K = { j }. The result follows from assumption G 6 . Assume j ∈ K. The result follows as x is K-coherent. So, assume K = K ∪ { j }, where K is non-empty. So H(K , k) holds, and there is u such that u ∈ G k , x = f j k (u) and u ∈ Y K k (x). Obviously G forms a projective system of subsets of S, and lim ← --G is nonempty if there is a coherent system x with domain I (recall that x ∈ I G i and x i = f i j (x j ) holds). Consider the set of all functional graphs whose domain is a subset of I and whose range is a subset of i G i .

  (one (mixin base)) (inv (mixin base)) (mul (mixin base)) }.

  group_set A := (1 \in A) && (A * A \subset A). Notation Local groupT := ... Definition generated A := \bigcap_(G : groupT | A \subset G) G. Definition cycle x := generated [set x]. Definition order x := #|cycle x|. Lemma invg_expg x : x^-1 = x ^+ #[x].-1.

  Definition tree_to_pos := tree_rec (fun n => Yo (n = \0c) \0c \1c) id (fun a b => (cmin a b)). Definition tree_is_pos x := tree_to_pos x = \1c. Lemma tree_rec_bool h1 (f := tree_rec_ h1 id (fun a b => (cmin a b))): (forall x, natp x -> h1 x <=c \1c) -> (forall x, treep x -> f x <=c \1c). Lemma tree_to_pos_p1: [/\ (forall x, natp x -> tree_to_pos (Tb (csucc x)) = \1c), (tree_to_pos (Tb \0c) = \0c), (forall x, treep x -> tree_to_pos (Tp x) = tree_to_pos x) & (forall x x', treep x -> treep x' -> tree_to_pos (Tx x x') = cmin (tree_to_pos x) (tree_to_pos x'))]. Lemma tree_to_pos_p2: [/\ (forall x, natp x -> (tree_is_pos (Tb x) <-> x <> \0c)), (forall x, treep x -> (tree_is_pos (Tp x) <-> tree_is_pos x)) & (forall x x', treep x -> treep x' -> (tree_is_pos (Tx x x') <-> ((tree_is_pos x) /\ (tree_is_pos x'))))].

  Lemma tree_size_p: [/\ (forall x, natp x -> tree_size (Tb x) = x), (forall x, treep x -> tree_size (Tp x) = tree_size x) & (forall x y, treep x ->treep y -> tree_size (Tx x y) = cmax (tree_size x) (tree_size y)) ]. Lemma NS_rree_size x: treep x -> natp (tree_size x).

Fixpoint

  Tree_to_tree e:= match e with | Tbase n => J \0c (nat_to_B n) | Tpowerset e' => J \1c (Tree_to_tree e') | Yproduct e' e'' => J \2c (J (Tree_to_tree e') (Tree_to_tree e'')) end. Lemma Tree_to_tree_prop e (t := Tree_to_tree e): [/\ treep t, tdepth t = nat_to_B (Tdepth e), tree_size t = nat_to_B (Tsize e)& tree_is_pos t <-> Tpositive e]. Lemma Tree_to_tree_injective: injective Tree_to_tree. Lemma Tree_to_tree_surjective x: treep x -> exists e, x = Tree_to_tree e.

  Definition ech_good x i := \1c <=c x /\ x <=c i. Definition echelon c := slist_E c (Nat \times Nat) /\ forall i, i <c (slength c) -> let a:= P (Vg c i) in let b:= Q (Vg c i) in (b = \0c -bo > ech_good a i) /\ (b <> \0c -> a <> \0c -> ech_good a i /\ ech_good b i). Definition esize c := \csup(range (Lg (domain c) (fun i=> Yo (P (Vg c i) = \0c) (Q (Vg c i)) \0c))). Lemma echelon_p1 c: echelon c -> \0c <c slength c -> exists b, [/\ natp b, \0c <c b, Vl c \1c = J \0c b]. Lemma echelon_p1' c: echelon c -> \0c <c slength c -> exists b, [/\ natp b, \0c <c b & Vg c \0c = J \0c b]. Lemma esize_empty c : echelon c -> slength c = \0c -> esize c = \0c. Inria Lemma esize_prop1 c (n:= esize c) (m:=slength c): echelon c -> \0c <c m -> [/\ natp n, \0c <c n, exists2 j, j <c m & Vg c j = J \0c n & forall j, j <c m -> P (Vg c j) = \0c -> Q (Vg c j) <=c n]. Lemma esize_prop2 c n (m:=slength c): echelon c -> (exists2 j, j <c m & Vg c j = J \0c n) -> (forall j, j <c m -> P (Vg c j) = \0c -> Q (Vg c j) <=c n) -> esize c = n. Lemma NS_esize c: echelon c -> natp (esize c).

Definition

  Ech_powerset c:= c +s1 J (slength c) (J (slength c) \0c). Lemma Ech_powerset_prop c (m := slength c)(c':= Ech_powerset c): echelon c -> \0c <c m -> [/\ echelon c', slength c' = csucc m, esize c' = esize c, Vg c' m = J m \0c & forall k, k <c m -> Vg c' k = Vg c k].

  Lemma tree_to_echelon_prop2 t: tree_to_echelon (Tree_to_tree t) = Tree_to_echelon t. Lemma tree_to_echelon_ok t (c := tree_to_echelon t): treep t -> [/\ echelon c, \0c <c slength c & esize c = csucc (tree_size t)].

  1 (b), if b = 0 then h 2 ( f (a)), otherwise h 3 ( f (a), f (b)). It satisfies the following property: if f 1 and f 2 agree for values < i , and c i is equal to (a, b), then p( f 1 , a, b) = p( f 2 , a, b). Definition Erecdef_combine h1 h2 h3 := Inria fun f a b => Yo (a = \0c) (h1 b) (Yo (b = \0c) (h2 (Vl f a)) (h3 (Vl f a) (Vl f b))). Definition echelon_recdef_prop c (p: Set -> Set -> Set -> Set):= forall g1 g2 i, i <c slength c -> (forall j, j <c i -> Vg g1 j = Vg g2 j) -> p g1 (P (Vg c i)) (Q (Vg c i)) = p g2 (P (Vg c i)) (Q (Vg c i)).Lemma erecdef_prop1 c: echelon c -> echelon_recdef_prop c (erecdef_combine h1 h2 h3).

  otherwise both a and b are between 1 and i and f i = h 3 ( f (a), f (b)). Definition echelon_recdef c (p := erecdef_combine h1 h2 h3) := restr (graph (transfinite_defined Nat_order (fun u => (p (graph u)(P (Vg c (source u))) (Q (Vg c (source u))))))) (slength c). Lemma erecdef_prop c (m := slength c)(f := echelon_recdef c) (p := erecdef_combine h1 h2 h3): echelon c -> [/\ fgraph f, domain f = m & forall i, i <c m -> Vg f i = p f (P (Vg c i)) (Q (Vg c i))].Lemma erecdef_unique c f (m := slength c) (p := erecdef_combine h1 h2 h3): echelon c -> slistpl f m -> (forall i, i <c m -> Vg f i = p f (P (Vg c i)) (Q (Vg c i))) -> f = echelon_recdef c. Lemma ecrecdef_unique1 c f (m := slength c): echelon c -> slistpl f m -> (forall i, i <c m -> let a:= P (Vg c i) in let b :

  Lemma erecdef_restr c n:José Grimmechelon c -> n <=c slength c -> echelon_recdef (restr c n) = restr (echelon_recdef c) n. Lemma echelon_recdef_extent2 c c' i: echelon c -> echelon c' -> i <=c slength c -> i <=c slength c' -> i <> \0c -> (forall k, k<c i -> Vg c k = Vg c' k) -> Vl (echelon_recdef c) i = Vl (echelon_recdef c') i. Definition echelon_recdef_last c := Vl (echelon_recdef c) (slength c). Lemma erecdef_base n (c := Ech_base n): natp n -> \0c <c n -> echelon_recdef_last c = h1 n. Lemma erecdef_powerset c (c' := Ech_powerset c): echelon c -> \0c <c slength c -> echelon_recdef_last c' = h2 ( echelon_recdef_last c). Lemma erecdef_product c c' (c'' := Ech_product c c'): echelon c -> echelon c' -> \0c <c slength c -> \0c <c slength c' -> echelon_recdef_last c'' = h3 (echelon_recdef_last c) (echelon_recdef_last c').

  Definition echelon_to_trees := echelon_recdef (fun b => Tb (cpred b)) Tp Tx. Lemma echelon_to_trees_prop c (m := slength c)(f := echelon_to_trees c) (n := esize c): echelon c -> [/\ fgraph f, domain f = m, forall i, i <c m -> treep (Vg f i) & forall i, i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> [/\ \1c <=c b, b <=c n & Vg f i = Tb (cpred b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg f i = Tp (Vl f a)] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg f i = Tx (Vl f a) (Vl f b)]]].

  Definition echelon_value c E := echelon_recdef (fun b => (Vl E b)) powerset product c. Definition echelon_of_base c E := Vl (echelon_value c E) (slength c). Lemma echelon_of_baseE c E: echelon_of_base c E = echelon_recdef_last (fun b => (Vl E b)) powerset product c. Lemma echelon_value_prop c E i (m := slength c)(f := echelon_value c E) (n:= esize c): echelon c -> i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> [/\ \1c <=c b, b <=c n & Vg f i = (Vl E b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg f i = \Po (Vl f a) ] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg f i = (Vl f a) \times (Vl f b)]].

Fixpoint

  => Vg E (nat_to_B n) | Tpowerset e' => \Po (Tree_value E e') | Tproduct e' e'' => (Tree_value E e') \times (Tree_value E e'') end. Lemma tree_value_prop E: [/\ (forall n, natp n -> tree_value E (Tb n) = Vg E n), José Grimm (forall x, treep x -> tree_value E (Tp x) = \Po (tree_value E x))& (forall x y, treep x -> treep y -> tree_value E (Tx x y) = (tree_value E x) \times (tree_value E y))]. Lemma Tree_value_compat E e: tree_value E (Tree_to_tree e) = Tree_value E e. Lemma tree_value_extent T E E': treep T -> (forall i, i<=c (tree_size T) -> Vg E i = Vg E' i) -> tree_value E T = tree_value E' T.

  Lemma product_injective A B C D: nonempty (C \times D) -> A\times B = C\times D -> A = C /\ B = D. Lemma not_a_powerset3 x: \3c <> powerset x. Lemma powerset_not_product x y z: powerset x <> y \times z. Lemma not_a_product1 x y: \1c <> x \times y.

  Lemma tree_value_commmutes E c (f := echelon_value c E) (t :=echelon_to_trees c) (g := Lg (domain c) (fun i => (tree_value E (Vg t i)))): echelon c -> f = g. Definition echelon_to_tree c := Vl (echelon_to_trees c) (slength c).

  Definition slist1 a:= Lg \1c (fun z => a). Definition slist2 a b := Lg \2c (fun z => Yo (z = \0c) a b). Definition slist6 a b c d e f:= Lg \6c (fun z => Yo (z = \0c) a (Yo (z = \1c) b (Yo (z = \2c) c (Yo (z = \3c) d (Yo (z = \4c) e f))))). Lemma slist1_prop a (s := slist1 a): slistpl s \1c /\ Vg s \0c = a. Lemma slist2_prop a b (c:= slist2 a b): [/\ slistpl c \2c, Vg c \0c = a & Vg c \1c = b]. Lemma slist6_prop a b c d e f (E:= slist6 a b c d e f): [/\ slistpl E \6c, Vg E \0c = a, Vg E \1c = b & [/\ Vg E \2c = c, Vg E \3c = d , Vg E \4c = e & Vg E \5c = f ]].

  f (m := slength c)(g := echelon_extension c f) : echelon c -> [/\ fgraph g, domain g = m & forall i, i <c m -> Vg g i = echelon_extension_aux f g (P (Vg c i)) (Q (Vg c i))]. Lemma Eextension_prop c f i (m := slength c)(g := echelon_extension c f) (n:= esize c): echelon c -> i <c m -> let a:= P (Vg c i) in let b := Q (Vg c i) in [/\ a = \0c -> [/\ \1c <=c b, b <=c n & Vg g i = (Vl f b)], b = \0c -> [/\ \1c <=c a, a <=c i & Vg g i = \Pof (Vl g a) ] & a <> \0c -> b <> \0c -> [/\ \1c <=c a, a <=c i, \1c <=c b, b <=c i & Vg g i = (Vl g a) \ftimes (Vl g b)]].

  Definition tree_extension f x := tree_rec Lemma Eextension_prop_bijsetL c E E' f: echelon c -> \0c <c slength c -> (forall i, i <c esize c -> inc (Vg f i) (bijections (Vg E i) (Vg E' i))) -> inc (echelon_can_extension c f) (bijections (echelon_of_base c E) (echelon_of_base c E')). Lemma Eextension_prop_id c f (g := echelon_extension c f) (is_identity := fun z => z = identity (source z)): echelon c -> (forall i, i <c esize c -> is_identity (Vg f i)) -> forall i, i <c slength c -> is_identity (Vg g i). Lemma Eextension_prop_idL c f E: echelon c -> (forall i, i <c esize c -> (Vg f i) = identity (Vg E i)) -> \0c <c slength c -> (echelon_can_extension c f) = identity (echelon_of_base c E).

  Definition slist_append x y := let n := slength x in let m := slength y in Lg (n +c m) (fun z => Yo (z <c n) (Vg x z) (Vg y (z -c n))). Definition Typ_with_id f A := slist_append f (Lg (domain A) (fun z => identity (Vg A z))). Lemma slist_append_list x y: slistp x -> slistp y -> slistp (slist_append x y) /\ slength (slist_append x y) = slength x +c slength y. Lemma slist_append_val1 x y i: slistp x -> slistp y -> i<c slength x -> Vg (slist_append x y) i = Vg x i. Lemma slist_append_val2 x y i: slistp x -> slistp y -> i<c slength y -> Vg (slist_append x y) ((slength x) +c i) = Vg y i. Lemma Typ_with_id_prop n S f x y A : slistpl x n -> slistpl y n -> slistpl f n -> slistp A -> echelon S -> slength S <> \0c -> esize S <=c n +c slength A -> (forall i, i <c n -> inc (Vg f i) (bijections (Vg x i) (Vg y i))) -> inc (echelon_can_extension S (Typ_with_id f A)) (bijections (echelon_of_base S (slist_append x A)) (echelon_of_base S (slist_append y A)) ). Lemma Typ_with_id_prop2 n S f x A: slistpl x n -> slistpl f n -> slistp A -> echelon S -> slength S <> \0c -> esize S <=c n +c slength A -> n = \0c -> echelon_can_extension S (Typ_with_id f A) = identity (echelon_of_base S (slist_append x A)).

Definition

  Typ_auxg n A S := [/\ natp n, slistp A, slistp S & forall i, inc i (domain S) -> echelon (Vg S i) /\ esize (Vg S i) <=c n +c slength A]. Definition Typ_schemeg x A S i:= Yo (slength (Vg S i) = \0c) emptyset (echelon_of_base (Vg S i) (slist_append x A)). Definition Typificationg n A S x s := [/\ Typ_auxg n A S, slistpl x n, slistpl s (slength S) & forall i, i <c slength s -> inc (Vg s i) (Typ_schemeg x A S i)]. Definition Typ_aux n A S := [/\ natp n, slistp A, echelon S & esize S <=c n +c slength A]. Definition Typ_scheme x A S:=

  Definition species_of_structure n A S R:= [/\ Typ_aux n A S, n <> \0c, slength S <> \0c & Transportable n A S R].Lemma species_of_structure_typification n A S R x s : species_of_structure n A S R -> (Typification n A S x s <-> (slistpl x n /\ inc s (echelon_of_base S (slist_append x A)))).InriaChapter 3

  Record projective_system: Type := ProjectiveSystem { psE : Set; psI : Set; psr : Set; psf : Set; ps_preorder_r: preorder psr; ps_substrate_r: substrate psr = psI;

Corollary 2 .

 2 Let (E λ α , f λ αβ ) λ∈L be a family of inverse systems of sets, relative to I. If λ∈L f λ αβ denotes the extensions to products (Chapter II, §5, No. 7, Definition 2) of the family of mappings ( f λ αβ ) λ∈L , then ( λ∈L E λ α , λ∈L f λ αβ

  F) I r (cst_graph r (identity F)). Lemma Inj_ex2_can_prop x y (E := (inl_sum Injex2_system)): related (inl_equiv Injex2_system) x y <-> [/\ inc x E, inc y E & P x = P y]. Lemma Inj_ex2_can_fun (E := (inductive_limit Injex2_system)): nonempty I -> bijection_prop (Lf (fun z => (P (rep z))) E F) E F. End InjExample2.

  introduce all variables and assumptions, and show that S and S have the same index set.Section DoubleDirectLimit2.Variables I1 I2 r1 r2: Set. Hypothesis (or1: preorder r1)(or2: preorder r2)InriaThis means that we can define v λ = lim --→ u λ , and equations(3.23) hold; so that we can define lim--→ v λ . Definition inl_dl2_v lam := inductive_limit_fun (inl_dl2_Slambda lam) (inl_dl2_Slambda' lam) (inl_dl2_ulam_famlam). Definition inl_dl2_v_fam := Lg I2 inl_dl2_v. Definition inl_dl2_limlim := (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr). Definition inl_dl2_limlim' := (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr'). Lemma inl_dl2_res2: inl_map2_compat inl_dl2_limlim inl_dl2_limlim' inl_dl2_v_fam. (* 120 *) What we have is not (3.33), but the following commutative diagram, where the vertical arrows are the canonical bijections hidden in (3Lemma inl_dl2_res3 (* 81 *) (bij1 := (inductive_map S (inl_dl_fu or1 or2 sr1 sr2 dr1 dr2 Sr) (inductive_limit (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr)))) (bij2 := (inductive_map S' (inl_dl_fu or1 or2 sr1 sr2 dr1 dr2 Sr') (inductive_limit (inl_dl_systemS' or1 or2 sr1 sr2 dr1 dr2 Sr')))) (pl1 := inductive_limit_fun S S' u) (pl2 := inductive_limit_fun inl_dl2_limlim inl_dl2_limlim' inl_dl2_v_fam): [/\ bijection bij1, bijection bij2 & pl2 \co bij1 = bij2 \co pl1]. End DoubleDirectLimit2.

  Er j) (Vf (ex5_f j k0) (ex5m F0 k0 (restr x F0))) (Vf (ex5_f j k) (ex5m F k (restr x F))). (* 123 *)

1

 1 Additional code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Example: the structure of a group . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.1 Preparation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.2 The group axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.3 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Structures and isomorphisms 2.1 Echelons . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Canonical Extensions of Mappings . . . . . . . . . . . . . . . . . . . . . . . . . . 2.3 Transportable relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.4 Species of structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Inverse limits and direct limits 3.1 Inverse limits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Inverse systems of mappings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Double Inverse Limit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 Conditions for an inverse limit to be non-empty . . . . . . . . . . . . . . . . . . 3.5 Direct limits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6 Direct systems of mappings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.7 Double Direct Limit. Product of Direct Limits . . . . . . . . . . . . . . . . . . . . 3.8 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

  (•) and s 2 ∈ S 2 (•) and . . . and s p ∈ S ≤ h ≤ m) as auxiliary base sets if the following condition is satisfied: let y 1 , . . . , y n , f 1 , . . . , f n be distinct letters which are distinct from the x i (1 ≤ i ≤ n), the s j (1 ≤ j ≤ p), the constants of T , and all the letters which appear in R or in the terms A h (1 ≤ h ≤ m) and let Id h (1 ≤ h ≤ m) denote the identity mapping of A h onto itself. Then the relation (2.2) "Täx 1 , . . . , x n , s 1 , . . . , s p ä and f 1 ∈ B(x 1 , y 1 ) and . . . and f n ∈ B(x n , y n )" Räx 1 , . . . x n , s 1 , . . . , s p ä ⇐⇒ Räy 1 , . . . y n , s 1 , . . . , s p ä,

	implies, in T , the relation
	(2.3)
	where
	(2.4)

p (•)"

is called a typification of the letters s 1 , . . . , s p .» « Let Räx 1 , . . . , x n , s 1 , . . . , s p ä be a relation in T which contains certain of the letters x i , s j (and possibly certain other letters as well). Then R is said to be transportable (in T ) with respect to the typification T, the x i (1 ≤ i ≤ n) being considered as principal base sets and the A h

(1

RR n°8997

Inria

RR n°8997RESEARCH CENTRE SOPHIA ANTIPOLIS -MÉDITERRANÉE 2004 route des Lucioles -BP 93 06902 Sophia Antipolis Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

José Grimm

Preparation

Recall that a graph s is a set of pairs, so is a subset of a cartesian product A × B. If A and B are the smallest possible, then A is called the domain and B the range (the domain is the set of all a such that for some b, (a, b) ∈ s, the range is defined similarly). The graph is functional if b is unique. This induces a mapping A → B. We say that a law s on E is a functional graph, with domain E × E, and whose range is a subset of E. The induced mapping will be denoted a b.

Recall that 'J a b' is the pair (a, b), 'P x' and 'Q x' are the first and second component of the pair x, denoted pr 1 x and pr 2 x, that 'Vg g x' and 'Vf f x' are the value of x by a functional graph g or a function f (see [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets[END_REF] and [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF] for more notations and definitions). We define here the identity on E and the canonical mapping (E×E)×E → E×(E×E). These objects are functional graphs, with a domain, target, evaluation function. Note that only the reflections lemmas are used in what follows.

Definition GE_I E := Zo (E\times E) (fun z => P z = Q z). Definition GE_J E := Zo (((E\times E) \times E)\times (E\times (E\times E))) (fun x => [/\ P (P (P x)) = P (Q x), Q (P (P x)

Lemma GE_I_incP E x: inc x (GE_I E) <-> [/\ pairp x, P x = Q x & inc (P x) E].

Lemma GE_I_fgraph E : fgraph (GE_I E).

Lemma GE_I_domain E : domain (GE_I E) = E.

Lemma GE_I_range E : range (GE_I E) = E.

Lemma GE_I_Ev E x: inc x E -> Vg (GE_I E) x = x.

Lemma GE_J_P E x: inc x (GE_J E) <-> exists a b c, [/\ inc a E, inc b E, inc c E & x = (J (J (J a b) c) (J a (J b c)))]. Lemma GE_J_fgraph E : fgraph (GE_J E). Lemma GE_J_domain E : domain (GE_J E) = (E\times E) \times E. Lemma GE_J_range E : range (GE_J E) = (E\times (E\times E)).

Lemma GE_J_Ev E a b c: inc a E -> inc b E -> inc c E -> Vg (GE_J E) (J (J a b) c) = (J a (J b c)).

We then define a complicated operation, denoted A ⊗ B. The interesting case is when A or B is the identity of E.

Can we have T = (1, T)? In an earlier version of Bourbaki, pairs were defined by an axiom, so the answer is: maybe. If we use the Kuratowski definition, then the answer is still maybe, but, if the foundation axiom holds then answer is no, if the anti-foundation axiom holds, then the answer is yes, and T is unique. If the answer is yes, we cannot define the depth of a tree, since the depth d of this tree would satisfy d = d + 1. Instead of 0, 1, 2, we could use other markers, in order to solve this difficulty; however, there is no guarantee that the tree will be finite. On the other hand, if we assume the existence of a depth function, one can proceed by induction (more technically by stratified induction, see above). We have studied in [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF] the set of formulas, and we use here the same techniques.

The idea is to consider the set of trees of depth ≤ n, defined by induction. We define by induction T n+1 = f (T n ), then T = n∈N T n . We say that an element x of T is a tree. We have either x ∈ T 0 , or there is an integer n such that x ∈ T n+1 and x ∈ T n .

Definition tset_index := induction_term (fun _ x => tset_next x) tset_base. Definition tset := unionf Nat tset_index. Definition treep x := inc x tset.

José Grimm

Definition scheme_ex2 := slist6 (J \0c \2c) (J \0c \1c) (J \1c \0c) (J \2c \0c) (J \4c \0c) (J \5c \3c).

Lemma scheme_ex1_ok1 (E := scheme_ex1): [/\ echelon E, slength E = \6c, esize E = \2c & [/\ Vg E \0c = J \0c \1c, Vg E \1c = J \0c \2c, Vg E \2c = J \1c \0c, Vg E \3c = J \3c \0c& (Vg E \4c =J \2c \0c /\ Vg E \5c =J \4c \5c) ]].

Lemma scheme_ex2_ok1 (E := scheme_ex2):

[/\ echelon E, slength E = \6c, esize E = \2c & [/\ Vg E \0c = J \0c \2c, Vg E \1c = J \0c \1c, Vg E \2c = J \1c \0c, Vg E \3c = J \2c \0c& (Vg E \4c =J \4c \0c /\ Vg E \5c =J \5c \3c) ]].

We can convert the echelon into a tree, and compute the value, step by step. We show the full result in the first case. The same can be done for the second example. The lists are different, but the last tree is the same. This means that, whatever the list l , S 1 (l ) = S 2 (l ). Lemma tree6_2: echelon_to_tree scheme_ex1 = echelon_to_tree scheme_ex2.

Evaluating S 1 on the list U, V is similar. We get (P(P(E)) × P(F)

Definition scheme_val1 U V:= slist6 U V (\Po U) (\Po(\Po U)) (\Po V) ((\Po(\Po U)) \times (\Po V)).

Lemma echelon_ex1_value U V: echelon_value scheme_ex1 (slist2 U V) = scheme_val1 U V. Lemma echelon_of_base_ex1 U V: echelon_of_base scheme_ex1 (slist2 U V) = ((\Po(\Po U)) \times (\Po V)).

Canonical Extensions of Mappings

« Let S = (c 1 , c 2 , . . . , c m ) be an echelon construction scheme on n term. Let E 1 , . . . , E n , E 1 , . . . E n be sets (terms in T ) and let f 1 , . . . f n be terms in T such that the relations " f i is a mapping of E i onto E i " are theorems in T for 1 ≤ i ≤ n. Let A 1 , . . . , A m (resp. A 1 , . . . , A m ) be the echelon construction of scheme S on E 1 , . . . , E n (resp. E 1 , . . . , E n ). We define step by step a sequence of m terms g 1 , . . . , g m such that g i is a mapping of A i into A i (for 1 ≤ i ≤ m) by the following conditions:

, then g i is the mapping f b i ,

José Grimm

(fun n => Vg f n) (fun t => extension_to_parts t) (fun t t' => ext_to_prod t t') x.

Lemma tree_extension_prop f: [/\ (forall n, natp n -> tree_extension f (Tb n) = Vg f n), (forall x, treep x -> tree_extension f (Tp x) = \Pof (tree_extension f x))& (forall x y, treep x -> treep y -> tree_extension f (Tx x y) = (tree_extension f x) \ftimes (tree_extension f y))]. Lemma tree_extension_commutes f c (t :=echelon_to_trees c) (g := Lg (domain c) (fun i => (tree_extension f (Vg t i)))): echelon c -> (echelon_extension c f) = g. Lemma tree_extension_commmute_bis E c1 c2: echelon c1 -> echelon c2 -> \0c <c slength c1 -> \0c <c slength c2 -> echelon_to_tree c1 = echelon_to_tree c2 -> echelon_can_extension c1 E = echelon_can_extension c2 E. Lemma can_extension_of_tree t E: treep t -> echelon_can_extension (tree_to_echelon t) E = tree_extension E t.

Let's now prove some theorems (including CST1, CST2 and CST3). First, we show that, if f i ∈ F (E i ; E i ), then g i ∈ F (A i ; A i ), where the A i are defined as above. If every f i is injective, surjective, bijective, identity, so is g i .

Lemma Eextension_prop_fct c E E' f

(A := echelon_value c E) (A' := echelon_value c E') (g := echelon_extension c f): echelon c -> (forall i, i <c (esize c) -> inc (Vg f i) (functions (Vg E i) (Vg E' i))) -> forall i, i <c (slength c) -> inc (Vg g i) (functions (Vg A i) (Vg A' i)).

Lemma Eextension_prop_inj c f (g := echelon_extension c f): echelon c -> (forall i, i <c (esize c) -> injection (Vg f i)) -> (forall i, i <c (slength c) -> injection (Vg g i)). Lemma Eextension_prop_surj c f (g := echelon_extension c f): echelon c -> (forall i, i <c (esize c) -> surjection (Vg f i)) -> (forall i, i <c (slength c) -> surjection (Vg g i)). Lemma Eextension_prop_bij_inv c f (g := echelon_extension c f) (lif := Lg (esize c) (fun z => inverse_fun (Vg f z))) (lig := echelon_extension c lif): echelon c -> (forall i, i <c (esize c) -> bijection (Vg f i)) -> forall i, i <c (slength c) -> bijection (Vg g i) /\ inverse_fun (Vg g i) = Vg lig i. Lemma Eextension_prop_bijset c E E' f (A := echelon_value c E) (A' := echelon_value c E') (g := echelon_extension c f): echelon c -> (forall i, i <c (esize c) -> inc (Vg f i) (bijections (Vg E i) (Vg E' i))) -> forall i, i <c (slength c) -> inc (Vg g i) (bijections (Vg A i) (Vg A' i)).

José Grimm

Yo (slength S = \0c) emptyset (echelon_of_base S (slist_append x A)).

Definition The typification is transportable. We have now (a) if p = 1, then the two transportability conditions are equivalent. (b) T(y, s ) holds, meaning that the typification is transportable. Special case n = 0 (no principal base set). Every relation is trxansportable (because s i = s i , whatever i ). In wat follows, at least one principal base set is required, since otherwise everything becomes trivial. Special case p = 0. « By abuse of language, in the theory of sets T 0 , the giving of n district letters x 1 , . . . , x n (with no typical characterization and no axiom) is considered as a species of structure Σ 0 , called the structure of a set on the n principle base sets x 1 , . . . , x n .» The next section explains some of the terms. The condition (2.3) simplifies to R(x) ⇐⇒ R(y) (in the code that follows, R has two arguments, the second being the list of the s i , thus is empty). Note that (2.3) says that there is a bijection x i → y i ; we rewrite this as card(x i ) = card(y i ).

Special case where R is independent of s (see example above with x 1 = x 2 ). Since s is not arbitrary, we assume R(x, s) ⇐⇒ R(x, s ) whenever s and s satisfy T(x, s) and T(x, s ). The relation becomes transportable when, whenever we have two families such that card(x i ) = card(y i ), whenever T(x, s) and T(y, s ), hold, then R(x, s) and R(y, s ) are equivalent.

Lemma slist_append_empty x: slistp x -> slist_append x emptyset = x. Lemma Typ_with_id_empty x: slistp x -> Typ_with_id x emptyset = x. Definition equipotent_fam n x y := forall i, i<c n -> cardinal (Vg x i) = cardinal (Vg y i).

Lemma transportable_spec1 n A S R: n = \0c -> Typ_auxg n A S -> Transportableg n A S R.

Lemma transportable_spec_p0 n A S R: slength S = \0c -> Typ_auxg n A S -> (Transportableg n A S R <-> (forall x y, slistpl x n -> slistpl y n -> equipotent_fam n x y -> (R x emptyset <-> R y emptyset))).

Lemma transportable_spec3 n A S R:

Example. We first say that (0, n) is an echelon of size n. We have S(E) = E n and 〈 f 〉 S = f n .

Definition slist1 a:= Lg \1c (fun z => a). Lemma slistp_0: slistpl emptyset \0c. Lemma slist1_prop a (s := slist1 a): slistpl s \1c /\ Vg s \0c = a. Lemma echelon_trivial n (S:= slist1 (J \0c n)): natp n -> n <> \0c -> echelon S /\ esize S = n. Lemma echelon_trivial_value n (S:= slist1 (J \0c n)) E:

We show that the relations considered above are transportable or not.

Definition Ex_scheme1 := slist2 (slist1 (J \0c \1c)) (slist1 (J \0c \1c)). Definition Ex_scheme2 := slist2 (slist1 (J \0c \1c)) (slist1 (J \0c \2c)).

Lemma Ex_typ_aux1: Typ_auxg \2c emptyset Ex_scheme1. Lemma Ex_typ_aux2: Typ_auxg \2c emptyset Ex_scheme2.

Lemma Ex_transportable1: Transportableg \2c emptyset Ex_scheme1 (fun _ s => Vg s \0c = Vg s \1c). Lemma Ex_transportable2: ~Transportableg \2c emptyset Ex_scheme1 (fun x _ => Vg x \0c = Vg x \1c). Lemma Ex_transportable3: ~Transportableg \2c emptyset Ex_scheme2 (fun _ s => Vg s \0c = Vg s \1c).

We define here a structure of species Σ and the set of all these structures.

Definition structure_of_species n A S R E U:= species_of_structure n A S R /\ Typification n A S E U.

Definition set_of_structure_of_species A S R E := Zo (echelon_of_base S (slist_append E A)) (R E).

Example. We consider 3 trees, and convert them to echelons. Each tree has size 0, so that each echelon has size 1. Needs to be formalized; Work in progress.

José Grimm

The restriction f α of the projection pr α to E is called the canonical mapping of E into E α , and we have the relation

A priori, pr i is the function defined on the product G, with values in E i that extracts the component of index i . This means that pr i x (note that parentheses are omitted) is x i . So the conditions (3.1) and (3.2) just say x i = f i j (x j ). If I is empty, then lim ← --E has a single element, the empty sequence.

Definition projective_limit S:= Zo (productb (psE S)) (fun x => forall i j, gle (psr S) i j -> (Vg x i) = Vf (Vg (psf S) (J i j)) (Vg x j)).

Definition prl_can_fun S i := Lf (fun x => Vg x i) (projective_limit S) (Vg (psE S) i).

Lemma prl_limitP S x:

Vf (prl_can_fun S i) x = Vg x i. Lemma prl_can_fun_fp S i: inc i (psI S) -> function_prop (prl_can_fun S i) (projective_limit S) (Vg (psE S) i). Lemma prl_can_fun_prop S i j (f := psf S) (fi := prl_can_fun S i) (fj := prl_can_fun S j): gle (psr S) i j -> (Vg f (J i j) \coP fj) /\ fi = (Vg f (J i j)) \co fj.

Lemma projective_limit_Iv S S':

prl_same_data S S' -> projective_limit S = projective_limit S'. Lemma prl_can_fun_Iv S S' i: prl_same_data S S' -> prl_can_fun S i = prl_can_fun S' i. Lemma prl_trivial S: psI S = emptyset -> projective_limit S = singleton emptyset.

Example 1. Assume that r is the diagonal of I, so that i ≤ j means i = j . Here (LP II ) says that all the functions are the identity. In this case, lim ← --S is the product of the E i .

José Grimm

Example 2. Assume that I is right directed, (E i ) is the constant family with value F, so that the product is I F , and f i j is the identity of F. Then lim ← --S is the diagonal of F I (the set of constant sequences). Proof: whatever i and j there is k such that i ≤ k and j ≤ k. We get x i = x k and x j = x k so that x i = x j .

Of course, I right directed has to be interpreted as: the preorder r is right directed. We prefer a mixed statement of the form: whenever x and y belong to I, there is z ∈ I such that x ≤ z and y ≤ z.

Example 3. Let E

This gives a projective system. Let x be in the projective limit. Then x i = x j + ( ji ). In particular, if i = 0, we get x 0 = x j + j . We get a contradiction if j = x 0 + 1. So the limit is empty. (For a less trivial example, see exercise 4.) Section Example3. Let r := Nat_order. Let f := fun i j => Lf (fun x => x +c (j -c i)) Nat Nat. Let ffam := Lg r (fun p => f (P p) (Q p)). Let Efam:= Lg Nat (fun i => Nat).

Lemma prl_exa3_prop1:

[/\ preorder r, substrate r = Nat & forall i j, gle r i j <-> [/\ natp i, natp j & i <=c j]]. Lemma prl_exa3_prop2 p: inc p r -> [/\ natp (P p), natp (Q p) & gle r (P p) (Q p)]. Lemma prl_exa3_prop3 i j: gle r i j -> lf_axiom (csum2^~(j -c i)) Nat Nat. Lemma prl_exa3_prop4 i j: gle r i j -> function_prop (f i j) Nat Nat. Definition prl_exa3_system: projective_system. Lemma prl_exa3_prop5: projective_system_on prl_exa3_system Efam Nat r ffam. Lemma prl_exa3_prop6 x: inc x (projective_limit prl_exa3_system) -> (natp (Vg x \0c) /\ forall i, natp i -> Vg x \0c = (Vg x i) +c i). Lemma prl_exa3_prop7: projective_limit prl_exa3_system = emptyset.

Restrictions. Let J be a subset of I. The set of all (i , j ) such that i ∈ J, j ∈ J and i ≤ j , ordered by ≤, is the preorder induced by r on J; denote it r . Let E and f be the restrictions of E and f to I and r , respectively. Then (E , J, r , f ) is a projective system, it is said to be obtained by restricting the index set to J. Note that prl_restr take as argument the proof that J ⊂ I, from which S and J are deduced.

Note: if we have two systems with the same data (in particular the same I), two proofs that J ⊂ I, then the restrictions have the same data.

Definition prl_map_compat S u F:=

[/\ fgraph u, domain u = psI S, forall i, inc i (domain u) -> function_prop (Vg u i) F (Vg (psE S) i) & forall i j, gle (psr S) i j -> Vg (psf S) (J i j) \co (Vg u j) = Vg u i].

Definition prl_map_property S u F g:= function_prop g F (projective_limit S) /\ forall i, inc i (domain u) -> (Vg u i) = (prl_can_fun S i) \co g.

Definition prl_map_val S u := fun y => Lg (psI S) (fun i => Vf (Vg u i) y).

Definition projective_map S u F := Lf (prl_map_val S u) F (projective_limit S).

Equation (3.6) says that if x = u(y), then x i = u i (y), so that u(y) is i → u i (y). This gives uniqueness and a definition of u.

Lemma prl_map_property_res1 S u F g i x:

prl_map_compat S u F -> prl_map_property S u F g -> inc i (psI S) -> inc x F -> Vf (Vg u i) x = Vg (Vf g x) i. Lemma prl_map_unique S u F g g':

prl_map_compat S u F -> prl_map_property S u F g -> prl_map_property S u F g' ->

José Grimm

Corollary 2 says that if we have three systems, S, S and S , then

Lemma prl_map2_prop1 S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> prl_map_compat S' (prl_map2_aux S u) (projective_limit S).

Lemma prl_map2_prop2 S u i t:

Lemma prl_map2_unique S S' u g g': prl_same_index S S' -> prl_map2_compat S S' u-> prl_map2_property S S' u g -> prl_map2_property S S' u g' -> g = g'.

Lemma prl_map2_prop S S' u (g := projective_limit_fun S S' u): prl_same_index S S' -> prl_map2_compat S S' u -> prl_map2_property S S' u g.

Lemma prl_map2_compat_aux S S' u x i j: prl_same_index S S' -> prl_map2_compat S S' u -> inc x (projective_limit S) -> gle (psr S) i j -> Vf (Vg u i) (Vg x i) = Vf (Vg (psf S') (J i j)) (Vf (Vg u j) (Vg x j)).

Lemma prl_map_val_aux2 S S' u (Ha :prl_same_index S S') (Hu: prl_map2_compat S S' u) (f := projective_limit_fun S S' u) i x:

Lemma prl_map2_prop3 S S' u (Ha :prl_same_index S S') (Hu: prl_map2_compat S S' u)

Product of systems. Consider two systems S and S on the same index set I. Recall that if f and g are functions E → E and F → F , then that f × g is the function E × E → F × F that maps (x, x ) to ( f (x), g (x )). This allows us to define the product of S and S .

Definition prl_product_E S S':=

Inria Lg (psI S) (fun i => (Vg (psE S) i) \times (Vg (psE S') i)). Definition prl_product_f S S' := Lg (psr S) (fun i => (Vg (psf S) i) \ftimes (Vg (psf S') i)).

Definition prl_system_product S S' (sd: prl_same_index S S'): projective_system. Lemma prl_system_product_prop S S' (sd: prl_same_index S S'): projective_system_on (prl_system_product sd) (prl_product_E S S') (psI S) (psr S) (prl_product_f S S').

Consider the canonical mappings, and their product f i × f i . These functions are compatible with the projections, so that lim ← -- Restricting the sets. « Let (E α , f αβ ) be an inverse system of sets, and for each α ∈ I, let M α be a subset of E α . If f αβ 〈M β 〉 ⊂ M α whenever α ≤ β, the M α are said to form an inverse system of subsets of the E α . Let g αβ be the mapping of M β into M α (where α ≤ β) whose graph is the same as that of the restriction of f αβ to M β . Then it is clear that (M α , g αβ ) is an inverse system of sets and that

Definition prl_subfam_fct S M := Lg (psr S) (fun z => restriction2 (Vg (psf S) z) (Vg M (Q z)) (Vg M (P z))).

Lemma prl_subfam_prop1 S M (g := prl_subfam_fct S M): prl_subfam_hyp S M -> [/\ forall z, inc z (psr S) -> restriction2_axioms (Vg (psf S) z) (Vg M (Q z)) (Vg M (P z)), forall i j x, gle (psr S) i j -> inc x (Vg M j) -> Vf (Vg g (J i j)) x = Vf (Vg (psf S) (J i j)) x, forall i, inc i (psr S)-> function_prop (Vg g i) (Vg M (Q i)) (Vg M (P i)),

José Grimm

forall i j k, gle (psr S) i j -> gle (psr S) j k -> Vg g (J i j) \co Vg g (J j k) = Vg g (J i k) & forall i, inc i (psI S) -> Vg g (J i i) = identity (Vg M i)]. Proposition 2. « Let (E α , f αβ ) and (E α , f αβ ) be two inverse systems of sets relative to I, and let u α be a mapping of E α into E α for each α ∈ I, such that the u α form an inverse system of

u α (x α ) form an inverse system of subsets of the E α , and

Definition prl_invim_set u x := Lg (domain u) (fun i => (Vfi1 (Vg u i) (Vg x i))).

Lemma prl_inv_hyp S S' u x: prl_same_index S S' -> prl_map2_compat S S' u -> inc x (projective_limit S') -> prl_subfam_hyp S (prl_invim_set u x).

Lemma prl_inv_hyp_prop S S' u x (Hsb: prl_same_index S S') (Hc: prl_map2_compat S S' u) (Hx: inc x (projective_limit S')): (Vfi1 (projective_limit_fun S S' u) x) = projective_limit (projective_system_subsets (prl_inv_hyp Hsb Hc Hx)).

Corollary.

If every u i is injective (resp. bijective) so is u. For injectivity, assume u(a) = u(b), and consider x = u(a). Then b is in the projective limit, each b i is in u

x is the family of x i , then u(x) = x . [For surjectivity, see Exercise 4].

Lemma prl_inv_hyp_prop1 S S' u:

prl_same_index S S' -> prl_map2_compat S S' u -> (forall i, inc i (psI S) -> injection (Vg u i)) -> injection (projective_limit_fun S S' u).

José Grimm

inc k (psI S) -> (forall i, inc i (psI S) -> gle (psr S) i k) -> bijection_prop f (projective_limit S) (Vg (psE S) k).

Remark 1. Let f i be the canonical projection E → E i , and E i its image. Then, the system of the E i is a projective system of subsets, the associated functions are surjective, the limits are the same, and

Note that the inclusion just says: if i ≤ j then Im f i ⊂ Im f i j , where Im g is the image of g .

Definition prl_proj_image S i := Imf (prl_can_fun S i). Definition prl_proj_image_fam S := Lg (psI S) (prl_proj_image S).

Lemma prl_proj_image_prop1 S i j: gle (psr S) i j -> sub (prl_proj_image S i) (Imf (Vg (psf S) (J i j))). Lemma prl_proj_image_prop2 S i: inc i (psI S) -> sub (prl_proj_image S i) (Vg (psE S) i). Lemma prl_proj_image_prop3 S: prl_subfam_hyp S (prl_proj_image_fam S). Lemma prl_proj_image_fam_fs S (fij' := prl_subfam_fct S (prl_proj_image_fam S)):

forall ij, inc ij (psr S) -> surjection (Vg fij' ij). Lemma prl_proj_image_prop4 S: projective_limit S = projective_limit(projective_system_subsets (prl_proj_image_prop3 S)).

Remark 2. « Let I be a (right) directed ordered set, let (E α , f αβ ) be an inverse system of sets relative to I, and for each α ∈ I, let u α : F → E α be a mapping such that the family (u α ) satisfies the formula (3.5). Consider the inverse system (F α , i αβ ) indexed by I, where F α = F for all α ∈ I and i αβ is the identity mapping of F. Then (no. 1, Example 2) F is canonically identified with lim ← --F α . If we consider u α as a mapping of F α into E α , then u α is an inverse system of mappings, and the mapping u : F → E defined by (3.6) is identified with the inverse limit of this system of mappings. Hence by abuse of language, we write u = lim ← --u α . »

The context is the following, and we instantiated the result of example 2. Recall that lim ← --F α is the set of all objects of the form c x , the constant graph that maps every i ∈ I to x, for x ∈ F. (This can be identified with F, in case I is non-empty).

Section Remark2. Variable S : projective_system. Variables u F: Set. Hypothesis compat: prl_map_compat S u F. Hypothesis rdr:right_directed_on (psr S) (psI S).

Definition prl_r2_sf := prl_exa2_system F (ps_preorder_r S) (ps_substrate_r S). Lemma prl_r2_sf_prop1: projective_system_on prl_r2_sf (cst_graph (psI S) F) (psI S) (psr S) (cst_graph (psr S) (identity F)). Lemma prl_r2_sf_prop2:projective_limit prl_r2_sf = diagonal_graphp F (psI S).

That u i is a projective system of mappings is obvious. What we get is: two functions with the same target E, and two sources F, F , where F is the diagonal of F I . If x ∈ F then Inria u(x) = u (c x ). Note: if I is empty, then the projective limit has a single element, the empty set. We cannot identify F and F (since F has a single element), but u(x) = whatever x. Remark 3. « Let I be an ordered set, and let (E α , f αβ ) be an inverse system of sets relative to I. For each finite subset J of I, let F J be the inverse limit of the (finite) inverse system obtained from (E α , f αβ ) by restricting the index set to J. If J and K are any two finite subsets of I such that J ⊂ K let g JK denote the canonical mapping (3.3) of F K into F J . Then the relation (3.4) shows that (F J , g JK ) is an inverse system of sets relative to the directed set (with respect to the relation ⊂) F(I) of finite subsets of I. Now for each J ∈ F(I) let h J : E → F J be the canonical mapping (3.3). By virtue of (3.4) and with the abuse of language mentioned in Remark 2, h J is an inverse system of mappings. Put h = lim ← --

The following lemma will also be used in Exercise 4. We first introduce the set F, show that it is right directed. Note that, if i ∈ I, then i ∈ {i } and {i } ∈ F; so that F = I; moreover, if i ≤ j , there is J ∈ F, such that i ∈ J and j ∈ J (one can choose {i , j }).

Section Remark3. Variable S: projective_system. Definition prl_r3_nI := Zo (powerset (psI S)) finite_set. Definition prl_r3_nr := sub_order prl_r3_nI. Lemma prl_r3_sr: substrate prl_r3_nr = prl_r3_nI. Lemma prl_r3_trans i j k: gle prl_r3_nr i j -> gle prl_r3_nr j k -> gle prl_r3_nr i k. Lemma prl_r3_nI_stable_union x y: inc x prl_r3_nI -> inc y prl_r3_nI -> inc (x \cup y) prl_r3_nI. Lemma prl_r3_directed_nr: right_directed prl_r3_nr. Lemma prl_r3_qprop0 i: inc i (psI S) -> inc (singleton i) prl_r3_nI. Lemma prl_r3_qprop1 i j: gle (psr S) i j -> exists J, [/\ inc J prl_r3_nI, inc i J & inc j J].

The technique is the same as in Exercise 1 (see details below); instead of L we have F. Instead of J λ we have the identity on F (this makes some lemmas simpler).

José Grimm

We introduce a system S J , via the axiom of choice. In case J ∈ F, this gives a subsystem, otherwise S. We deduce F J , g J and g KJ . We show that (F J , g JK ) is a projective system. Definition prl_r3_systemi J := match (ixm (inc J prl_r3_nI)) with | inl hx => prl_restr (prl_r3_prop4 hx) | inr _ => S end. Definition prl_r3_Fl J := projective_limit (prl_r3_systemi J).

Lemma prl_r3_res0 i (H: inc i prl_r3_nI): prl_r3_Fl i = (projective_limit (prl_restr (prl_r3_prop4 H))). Lemma rem3prop5a j: inc j prl_r3_nI -> j = psI (prl_r3_systemi j). Lemma prl_r3_prop5b i (H: sub i (psI S)): inc i prl_r3_nI -> prl_same_data (prl_restr H) (prl_r3_systemi i). Lemma prl_r3_res1 i: inc i prl_r3_nI -> function_prop (prl_r3_gi i) (projective_limit S) (prl_r3_Fl i). Lemma prl_r3_prop5 i j: gle prl_r3_nr i j -> sub i (psI (prl_r3_systemi j)). Lemma prl_r3_prop6 i j (lij: gle prl_r3_nr i j) :

prl_same_data (prl_restr (prl_r3_prop5 lij)) (prl_r3_systemi i). Lemma prl_r3_prop6a i j (lij: gle prl_r3_nr i j) :

(projective_limit_restr (prl_r3_prop5 lij)) = (prl_r3_Fl i). Lemma prl_r3_prop7 i j: gle prl_r3_nr i j -> lf_axiom (restr^~i) (prl_r3_Fl j) (prl_r3_Fl i). Lemma prl_r3_res2 i j: gle prl_r3_nr i j -> function_prop (prl_r3_gij (J i j)) (prl_r3_Fl j) (prl_r3_Fl i). Lemma prl_r3_res3 i: inc i prl_r3_nI -> prl_r3_gij (J i i) = identity (prl_r3_Fl i). Lemma prl_r3_pr4 i j k: gle prl_r3_nr i j -> gle prl_r3_nr j k -> prl_r3_gij (J i j) \co prl_r3_gij (J j k) = prl_r3_gij (J i k).

Definition prl_r3_F: projective_system. Lemma prl_r3_F_prop: projective_system_on prl_r3_F (Lg prl_r3_nI prl_r3_Fl) prl_r3_nI prl_r3_nr (Lg prl_r3_nr prl_r3_gij).

Definition prl_r3_restr_fun z:= Lg prl_r3_nI (fun i => restr z i). Definition prl_r3_F_can := Lf prl_r3_restr_fun (projective_limit S) (projective_limit prl_r3_F).

Lemma prl_r3_F_can_ax1 i z: inc i prl_r3_nI -> inc z (projective_limit S) -> inc (restr z i) (prl_r3_Fl i). Lemma prl_r3_F_can_ax: lf_axiom prl_r3_restr_fun (projective_limit S) (projective_limit prl_r3_F). Lemma prl_r3_F_can_fun: inc prl_r3_F_can (functions (projective_limit S) (projective_limit prl_r3_F)). Lemma prl_r3_F_can_bf: bijection prl_r3_F_can. End Remark3. Section DoubleProjInjLimit. Variables I1 I2 r1 r2: Set. Hypothesis (or1: preorder r1)(or2: preorder r2) (sr1: substrate r1 = I1)(sr2: substrate r2 = I2).

Lemma pidl_or: preorder_on (prod_of_relation r1 r2) (I1 \times I2). Lemma pidl_gleP i j: gle (prod_of_relation r1 r2) i j <-> [/\ pairp i, pairp j, gle r1

Lemma pidl_directed: right_directed_prop r1 -> right_directed_prop r2 -> right_directed_prop (prod_of_relation r1 r2).

Lemma pidl_directed_bis: nonempty I1 -> nonempty I2 -> right_directed_prop (prod_of_relation r1 r2) -> right_directed_prop r1 /\ right_directed_prop r2. End DoubleProjInjLimit.

José Grimm

We recall that if I and L are two sets, ≤ I and ≤ L are two order (resp. preorder) relations on I and L, then the relation "pr 1 a ≤ I pr 1 b and pr 2 a ≤ L pr 2 b" between two elements a and b of I × L is an order (resp. preorder) relation on I × L. We consider a system S whose preorder is this relation (so that the index set will be I × L).

Section DoubleProjectiveLimit. Variables I1 I2 r1 r2: Set. Hypothesis (or1: preorder r1)(or2: preorder r2) (sr1: substrate r1 = I1)(sr2: substrate r2 = I2). Variable S: projective_system. Hypothesis Sr: psr S = (prod_of_relation r1 r2). Lemma prl_dl_I: psI S = I1 \times I2.

We define now the families E, g for fixed lambda, and the system S λ . The system is defined only if λ ∈ L. For this reason, we define (via the axiom of choice) a system whatever λ, choosing S as default value. This allows us to define F λ .

Definition prl_dl_S_lambda lam (Hl: inc lam I2) : projective_system. Lemma prl_dl_S_lambda_prop lam (Hl: inc lam I2) : projective_system_on (prl_dl_S_lambda Hl) (prl_dl_Elam_fam lam) I1 r1 (prl_dl_glam_fam lam).

Definition prl_dl_system_S_lambda lam := match (ixm (inc lam I2)) with | inl hx => (prl_dl_S_lambda hx) | inr _ => S end.

Definition prl_dl_F_lambda lam := projective_limit (prl_dl_system_S_lambda lam).

Lemma prl_dl_F_lambda_prop lam (Hl: inc lam I2): prl_dl_F_lambda lam = projective_limit (prl_dl_S_lambda Hl).

Assume now λ ≤ µ. This gives two systems S λ and S µ with the same index set, and a projective system of mappings h l m a . Corollary 2 gives (3.13).

Definition prl_dl_halm_fam lam mu:= Lg I1 (fun i => Vg (psf S) (J (J i lam) (J i mu))).

Definition prl_dl_hlm lam mu (H: gle r2 lam mu) := projective_limit_fun (prl_dl_S_lambda (pidl_i2_L sr2 H)) (prl_dl_S_lambda (pidl_i1_L sr2 H)) (prl_dl_halm_fam lam mu).

Lemma prl_dl_halm_compat lam mu (H: gle r2 lam mu): prl_map2_compat (prl_dl_S_lambda (pidl_i2_L sr2 H)) (prl_dl_S_lambda (pidl_i1_L sr2 H)) (prl_dl_halm_fam lam mu).

Lemma prl_dl_hlm_compose l m n (Hlm : gle r2 l m) (Hmn: gle r2 m n): (prl_dl_hlm Hlm) \co (prl_dl_hlm Hmn) = (prl_dl_hlm (proj33 or2 _ _ _ Hlm Hmn)).

We now define h l m , via the axiom of choice. If x ∈ r 2 , then pr 1 x ≤ pr 2 x, and we can consider h x = h pr 1 x≤pr 2 x . Assume l ≤ m, and let x be the pair (l , m). Obviously, pr 1 x = l and pr 2 x = m but this does not imply h l m = h x , so this equality is not trivial. Also h i i is the identity function, but we have to work a bit. Finally, defining S is trivial.

Lemma prl_dl_hlm_fct lm: inc lm r2 -> function_prop (prl_dl_hlm_gen lm) (prl_dl_F_lambda (Q lm))(prl_dl_F_lambda (P lm)). Lemma prl_dl_S_lambda_Iv2 x y (H1: inc x I2) (H2: inc y I2) : x = y -> prl_same_data (prl_dl_S_lambda H1)(prl_dl_S_lambda H2). Lemma prl_dl_hml_invariant i j (H:gle r2 i j) :

prl_dl_hlm H = prl_dl_hlm_gen (J i j). Lemma prl_dl_hml_id i: inc i I2 -> Vg (Lg r2 prl_dl_hlm_gen) (J i i) = identity (prl_dl_F_lambda i).

Definition prl_dl_systemS': projective_system. Lemma prl_dl_systemS'_prop: projective_system_on prl_dl_systemS' (Lg I2 prl_dl_F_lambda) I2 r2 (Lg r2 prl_dl_hlm_gen).

Finally, we identify the two projective limits, via Chapter II, §5, no 5, Proposition 7. The proposition says that a product on a set A, partitioned in A i is isomorphic to a double product, the inner product being over all A i , the outer product over the index set of the partition. It does not apply, but we can think of the partition induced on the product by fixing one index. We may however use the same techniques. Take x ∈ lim ← --S, λ ∈ L; f λ (x) will be the functional graph i → x i λ , with domain I. The functional graph λ → f λ (x) with domain I belongs to lim ← --S .

Definition prl_dl_slice x l := Lg I1 (fun i => Vg x (J i l)). Definition prl_dl_slice2 x := Lg I2 (prl_dl_slice x). Definition prl_dl_can_iso := Lf prl_dl_slice2 (projective_limit S) (projective_limit prl_dl_systemS').

Lemma prl_dl_slice_p1 x lam: inc x (projective_limit S) -> inc lam I2 -> inc (prl_dl_slice x lam) (prl_dl_F_lambda lam).

Section DoubleInverseLimit2.

Variables I1 I2 r1 r2: Set. Hypothesis (or1: preorder r1)(or2: preorder r2) (sr1: substrate r1 = I1)(sr2: substrate r2 = I2).

Variables S S': projective_system. Variable u: Set.

Hypothesis Sr: psr S = prod_of_relation r1 r2. Hypothesis Sr': psr S' = prod_of_relation r1 r2. Hypothesis compat_u: prl_map2_compat S S' u.

Lemma psr_dl2_SrSr: prl_same_index S S'.

We define here S λ , S λ and u λ . The systems are defined as above, and u λ is a slice of u. Relations (3.7) hold whenever λ ∈ L. This allows to define v λ = lim ← --u λ , and the family (v λ ) λ∈L . This family satisfies (3.7) for the systems lim ← --S λ and lim ← --S λ .

Definition prl_dl2_ulam_fam lam := Lg I1 (fun i => Vg u (J i lam)). Definition prl_dl2_Slambda := (prl_dl_system_S_lambda or1 or2 sr1 sr2 Sr). Definition prl_dl2_Slambda':= (prl_dl_system_S_lambda or1 or2 sr1 sr2 Sr').

Lemma prl_dl2_res1 lam:inc lam I2 -> prl_same_index (prl_dl2_Slambda lam) (prl_dl2_Slambda' lam) /\ prl_map2_compat (prl_dl2_Slambda lam) (prl_dl2_Slambda' lam) (prl_dl2_ulam_fam lam).

Definition prl_dl2_v lam := projective_limit_fun (prl_dl2_Slambda lam) (prl_dl2_Slambda' lam) (prl_dl2_ulam_fam lam). Definition prl_dl2_v_fam := Lg I2 prl_dl2_v. Definition prl_dl2_limlim := (prl_dl_systemS' or1 or2 sr1 sr2 Sr). Definition prl_dl2_limlim' := (prl_dl_systemS' or1 or2 sr1 sr2 Sr'). Section DoubleInverseLimit3.

Variables I L r: Set. Variable fS: Set -> projective_system.

Hypothesis (or: preorder r)(sr: substrate r = I). Hypothesis fSr: forall l, inc l L -> psr (fS l) = r. Definition prl_dl3_or := prod_of_relation r (diagonal L).

Lemma prl_dl3_fSI l: inc l L -> psI (fS l) = I. Lemma prl_dl3_orL: preorder (diagonal L). Lemma prl_dl3_srL: substrate (diagonal L) = L. Lemma prl_dl3_osr: preorder_on (prl_dl3_or) (I \times L).

Lemma prl_dl3_or_prop1 p: inc p (prl_dl3_or) ->

José Grimm

[/\ pairp p, inc (P p) (I\times L), inc (Q p) (I\times L), inc (J (P (P p)

Definition prl_dl3_systemS: projective_system.

Lemma prl_dl3_systemS_prop: projective_system_on prl_dl3_systemS prl_dl3_E (I\times L) prl_dl3_or prl_dl3_f.

Obviously, we can apply Proposition 4. It says that there is a canonical isomorphism between S and S , for some S , which is a system on E. If we look at the definition, we see that this is the family F λ introduced above, i.e. lim ← -α E λ α . Moreover, the only functions of S are the identity functions (since L is trivially ordered) so that lim ← --S = E.

Lemma prl_dl3_systemS_sr: psr prl_dl3_systemS = prod_of_relation r (diagonal L).

Let iso:= (prl_dl_can_iso or prl_dl3_orL sr prl_dl3_srL prl_dl3_systemS_sr). Let S':= (prl_dl_systemS' or prl_dl3_orL sr prl_dl3_srL prl_dl3_systemS_sr).

Let E := Lg L(prl_dl_F_lambda or prl_dl3_orL sr prl_dl3_srL prl_dl3_systemS_sr).

Lemma prl_dl3_RHS: (projective_limit S') = productb E. Lemma prl_dl3_systemS_can: bijection_prop iso (projective_limit prl_dl3_systemS) (productb E).

Consider now the LHS, the projective limit of S. This is a subset of I×L , identified with I L , by considering a double family as a family of families. We introduce the function and show that it is injective.

We pretend that the target of the function is the projective system over I of the sets L E λ α ; the functions are the extensions to products of the f λ αβ . We study these extensions. Then prove the result.

José Grimm

Lemma prl_ne1_surj_rec i j (f := prl_can_fun S): gle (psr S) i j -> surjection (f j) -> surjection (f i).

Lemma prl_ne1_res2: (exists2 j, inc j (psI S) & forall i, inc i (psI S) -> gle (psr S) i j) -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).

Lemma prl_ne1_res3 A: cofinal (psr S) A -> finite_set A -> forall i, inc i (psI S) -> surjection (prl_can_fun S i).

We assume now that there is a countable cofinal set A. The case A finite (or empty) is not considered by Bourbaki, but is dealt with above. Enumerate A as a 0 , a 1 , . . .. Take for b n+1 an upper bound of a n and b n . By induction, there exists an increasing function b : N → I, whose range is cofinal. Bourbaki says « we need only prove the Proposition for the case I = N » (this is not really true, but the idea is there). Let's show that f k is surjective when k ∈ I. There is n such that k ≤ b(n); it suffices to show that f b(n) is surjective. Bourbaki says « It is clear that it suffices to prove that f 0 is surjective » (this really means: we need only consider b( j ) for j ≥ n. Take y ∈ E b(n) ; define a sequence y i by induction via

) and y 0 = y. This is possible, since b is increasing and the function that appears there is surjective. By induction

) by the previous remark, so that x i is independent of the choice of j . This trivially says that the sequence of the x i belongs to lim ← --S, and its value by f b(n) is y.

forall i, inc i (psI S) -> surjection (prl_can_fun S i). (* 97 *) End ProjectiveLimitNonEmpty1.

Theorem 1. Consider a projective system S on a right directed set I such that there is S satisfying properties (i), (ii), (ii) and (iv), described below. Then (a) (3.17)

In this statement, E is the projective limit of S and f i the canonical projection E → E i . Equation (3.17) can be written as Im f i = i ≤ j Im f i j . Assume E k = for some index k. In this case E is empty, as well as the RHS of (3.17). There exists j such i ≤ j and k ≤ j . Since E k is empty, so is E j as well as f i j 〈E j 〉 and the intersection. This means that (a) holds trivially, as well as (b).

Section ProjectiveLimitNonEmpty2.

Variable S: projective_system. Hypothesis rdr: right_directed_prop (psr S). Definition prl_ne2_res_RHS i := intersectionf (Zo (psI S) (gle (psr S) i))

(fun j => (Imf (Vg (psf S) (J i j)))). Definition prl_ne2_res_a:= forall i, inc i (psI S) -> Imf (prl_can_fun S i) = prl_ne2_res_RHS i.

Lemma prl_ne2_intP i j: inc j (Zo (psI S) (gle (psr S) i)) <-> (gle (psr S) i j). Lemma prl_ne2_int_i i: inc i (psI S) -> inc i (Zo (psI S) (gle (psr S) i)). Lemma prl_ne2_prop_trivial:

The assumption is that there exists a functional graph S on I, such that S i is formed of subsets of E i , and every intersection of sets belonging to S i also belongs to S i . This is condition (i). The case of the empty intersection is a bit tricky: it has to be interpreted as

Variable FS_fam: Set.

Hypothesis FS_fgraph: fgraph FS_fam. Hypothesis FS_domain: domain FS_fam = psI S. Hypothesis FS_range:

The second condition (ii) is: if a set of subsets F ⊂ S i is such that every finite intersection of sets belonging to F is non-empty, then M∈F M is non-empty. The variant (ii)' says if G ⊂ S i is left directed (with respect to inclusion) and does not contain the empty set, then M∈G M is non-empty [note that G has to be nonempty.] Note: assume (ii) true, and G left directed, if A a finite subset of G, by induction there is z ∈ G such that z ⊂ A. This shows (ii)'. Conversely, assume (ii)' true and let F be a set satisfying the hypothesis of (ii). Let G be the set of finite non-empty intersections of F. This is a subset of F (take singletons) and does not contain the empty set; it is also stable by intersection.

José Grimm

Condition (iii) says: if i ≤ j and x i ∈ E i we have f -1 i j (x i ) ∈ S j . The weaker condition (iii)' is: for each i ∈ I and each non-empty set M i ∈ S i there exists Lemma pr1_ne2_hyp3_weak_prop: pr1_ne2_hyp3_plain -> pr1_ne2_hyp3_weak.

Condition (iv) is: if i ≤ j and M j ∈ S j , then f i j 〈M j 〉 ∈ S i .

Hypothesis FS_prop_iv: forall i j M, gle (psr S) i j -> inc M (Vg FS_fam j) -> inc (Vfs (Vg (psf S) (J i j)) M) (Vg FS_fam i).

Hypothesis prl_ne2_ne: forall i, inc i (psI S) -> nonempty (Vg (psE S) i).

Bourbaki proves (b) as follows. Assume every E i non-empty. Fix i , let X i = f i j 〈E j 〉. Since E j is nonempty, it is non-empty. By (iv) it belongs to S i . The family is left directed, for if i ≤ j ≤ k then X k ⊂ X j , and given two indices j and j , there is an upper bound k. By (ii)' the intersection K i is non-empty. Now (a) implies (b) is as follows. First, there is nothing to prove if I is empty. So, let's take an index i . By (a), K i = f i (E), so that K i non-empty says E non-empty.

We consider Σ, the set of families A = (A α ) α∈I which satisfy the following conditions (3.18)

A α = , and A α ∈ S α for all α ∈ I;

The proof is divided in four steps. We first notice that Σ is non-empty (recall that E i is non-empty). We order it by: A ≤ A whenever A i ⊂ A i for every index i ∈ I. Step 1 shows that Σ is an inductive set for this ordering. Let L be a nonempty totally ordered subset of Σ. Let x i = z∈L z i . By (ii)', (x i ) i ∈I is in Σ, and is an upper bound of L.

Definition prl_ne2_sigma := Zo (productb FS_fam) (fun A => (forall i, inc i (psI S) -> nonempty (Vg A i)) /\ (forall i j, gle (psr S) i j -> sub (Vfs (Vg (psf S) (J i j)) (Vg A j)) (Vg A i))).

Definition prl_ne2_sigma_le A A' := forall i, inc i (psI S) -> sub (Vg A' i) (Vg A i). Definition prl_ne2_sigma_order := graph_on prl_ne2_sigma_le prl_ne2_sigma. Lemma prl_ne2_sigma_osr: order_on prl_ne2_sigma_order prl_ne2_sigma. Lemma prl_ne2_sigma_ne: nonempty prl_ne2_sigma.

Lemma prl_ne2_sigma_inductive:

(forall i, inc i (psI S) -> prl_ne1_condii i) -> inductive prl_ne2_sigma_order.

Step 2:

By (iv), f i j 〈A j 〉 ∈ S i . This is a non-empty set, so by (ii)', the intersection is non-empty; note that the set of f i j 〈A j 〉 is left directed (for inclusion, fixed i , and j varying in I). This because if

Since the converse inclusion holds we have equality.

Lemma prl_ne2_sigma_maximal_prop1 A: (forall i, inc i (psI S) -> prl_ne1_condii' i) -> maximal prl_ne2_sigma_order A -> (forall i j, gle (psr S) i j -> (Vg A i) = Vfs (Vg (psf S) (J i j)) (Vg A j)).

Step 3. Let A be as above. We pretend that each A i is s singleton. We start by choosing x i ∈ A i . Let C j = f -1 i j (x i ). We shall assume (iii)', in other words, we can chose x i such that C j ⊂ S j . We set B j = A j ∩ C j when i ≤ j and B j = A j otherwise. Then B j ∈ S j by (i). By the previous result, x i ∈ f i j 〈A j 〉, so x i = f i j (x j ) for some x j , and B j is non-empty. We have

and the property is easy. By maximality, B = A since A is maximal. This says:

Step 4. Proof of the theorem. We have to show that if (iii) holds, then (a) and (b) are true, and when (iii)' holds then (b) holds. Note that (b) says that the projective limit is non-empty; we have shown above that (a) implies (b); we give here a direct proof. By step 1 and Zorn's lemma, Σ has a maximal element, a family (A i ) i ; by step 3, A i = {x i }, and by step 2 x i = f i j (x j ). This says that the family (x i ) belongs to E.

José Grimm

Lemma prl_ne2_sigma_maximal_prop3 A (xi := fun i => union (Vg A i)):

We now prove (a). Fix i . Let X j = f i j 〈E j 〉. We have f i 〈E〉 ⊂ X j when i ≤ j (by definition of the projective limit). Let K be the intersection of the X j . Then

Bourbaki says: « Finally the proof of ( 4)

shows that if K = and if we choose an x α in this set such that B β ∈ S β whenever β ≥ α, there exists y ∈ E such that f α (y) = x α , which proves our assertion. » We have shown above that if no E i is empty, then K is non-empty. In this case (iii)' says that we can choose x i such that B j ∈ S j . We shall however assume (iii), it says B j ∈ S j , whatever j . We shall prove that, under this condition, x i is in the range of f i . So: (iii) says that every element of K is in f i 〈E〉, and (iii)' says that at least one element of K is in f i 〈E〉. We extend the family B by setting B j = E j for indices that do not satisfy i ≤ j . By definition of x i , B j is non-empty. Clearly, it is in Σ.

Since Σ is inductive (Step 1) there exists a maximal element A with B ≤ A. Since (iii)' holds, we know that A i = {t i } and t = (t i ) i ∈ E. We have f i (t ) = t i . However A i ⊂ B i says t i ∈ B i ; since f i i is the identity function B i = {x i }, so that t i = x i . (total size of the definitions + proof: 600 lines).

Lemma prl_ne2_sigma_maximal_ne A:

Direct limits

« Let I be a (right) directed preordered set and let (E α ) α∈I be a family of sets indexed by I. For each pair (α, β) of elements of I such that α ≤ β, let f βα be a mapping of E α into E β . Inria Suppose that the f βα satisfy the following conditions:

By abuse of language, the pair ((E α ), ( f βα )) (which is usually written (E α , f βα )) is called a direct system of sets, relative to the index set I. » We shall use the term "inductive" system instead of "direct" system, unless quoting Bourbaki. We shall use a record, as in the case of a projective system. We shall identify f j i with f (i , j ) . This means that, for every p ∈ r (where r is the preorder of I), f p is a function E pr 1 (p) → E pr 2 (p) . ; is_compose_f: forall i j k, gle isr i j -> gle isr j k -> Vg isf (J j k) \co Vg isf (J i j) = Vg isf (J i k); is_identity_f: forall i, inc i isI -> Vg isf (J i i) = identity (Vg isE i) }. We start with trivial properties, the same as for projective systems.

Definition inductive_system_on S E

Lemma inl_same_dataS S S': inl_same_data S S' -> inl_same_data S' S. Lemma inl_same_dataT S S' S'' : inl_same_data S S' -> inl_same_data S' S'' -> inl_same_data S S''.

Lemma inl_same_index_same_I S S': inl_same_index S S' -> isI S = isI S'. Lemma inl_prop0 S i j: gle (isr S) i j -> inc i (isI S) /\ inc j (isI S). Lemma inl_prop1 S i: inc i (isI S) -> inc (J i i) (isr S). Lemma inl_prop2 S i j k: gle (isr S) i j -> gle (isr S) j k -> Vg (isf S) (J j k) \coP Vg (isf S) (J i j). Lemma inl_prop3 S y i j k (f:= isf S): gle (isr S) i j -> gle (isr S) j k -> inc y (Vg (isE S) i) -> Vf (Vg f (J j k)) (Vf (Vg f (J i j)) y) = Vf (Vg f (J i k)) y. Lemma inl_prop4 S i j: gle (isr S) i j -> function_prop (Vg (isf S) (J i j)) (Vg (isE S) i) (Vg (isE S) j).

José Grimm

Lemma inl_prop5 S i x: inc i (isI S) -> inc x (Vg (isE S) i) -> Vf (Vg (isf S) (J i i)) x = x.

« Let G be the set which is the sum of the family of sets (E α ) α∈I (Chapter II, §4, no. 8); by abuse of language, we shall identify the E α with their canonical images in G, and for each x ∈ G we shall denote by λ(x) the unique index α ∈ I such that x ∈ E α . » Recall that G is the union of the E i × {i }. The canonical image of E i is the set of all (x, i ) for x ∈ E i , and λ(x) is just the second projection of x. « Let Räx, yä denote the following relation between two elements x, y of G: "there exists an element γ ∈ I such that γ ≥ α = λ(x) and γ ≥ α = λ(y) for which f γα (x) = f γβ (y)." » So we introduce the following definitions

Definition inl_equiv S := graph_on(inl_equiv_rel S) (inl_sum S) .

The relation R is an equivalence relation. We shall denote by C S (t ) the class of t for this relation. Assume i ≤ j , x ∈ E i , and let y = f j i (x) ∈ E j . Then C S (x, i ) = C S (y, j ). (Note that R is the least equivalence satisfying this property).

Lemma inl_equiv_reflexive S a: inc a (inl_sum S) -> inl_equiv_rel S a a. Lemma inl_equiv_esr S: equivalence_on (inl_equiv S) (inl_sum S).

Lemma inl_class_eq S x y: inc x (inl_sum S) -> inc y (inl_sum S) -> (class (inl_equiv S) x = class (inl_equiv S) y <-> inl_equiv_rel S x y).

Lemma inl_class_eq_bis S i j x y: inc i (isI S) -> inc j (isI S) -> inc x (Vg (isE S) i) -> inc y (Vg (isE S) j) -> (class (inl_equiv S) (J x i) = class (inl_equiv S) (J y j) <-> inl_equiv_rel S (J x i) (J y j)). Lemma inl_class_of_fij S i j x: gle (isr

« The quotient set E = G/R is called the direct limit of the family (E α ) α∈I with respect to the family of mappings ( f βα ), and is written E = lim --→ (E α , f βα ) or simply E = lim --→ E α . » We shall use the notation lim --→ S for the inductive limit of the inductive system S. We shall denote by R(t ) a representative of the class t in the quotient. This is a pair (x, i ) such that i ∈ I, x ∈ E i and t = C S (x, i ). Clearly, the inductive limit is non-empty if and only if there is an index i such that E i is non-empty.

Definition inductive_limit S := quotient (inl_equiv S).

Lemma inductive_limitP S x: inc x (inductive_limit S) <-> classp (inl_equiv S) x.

Lemma inl_class_in_lim S i x:

« We denote by f α the restriction to E α of the canonical mapping f of G into E = G/R; f α is called the canonical mapping of E α into E. We have the relation (3.20) just says that some functions can be composed and C S (x, i ) = C S ( f j i (x), j ).

Definition inl_can_fun S i :=

Lf (fun x => class (inl_equiv S) (J x i)) (Vg (isE S) i) (inductive_limit S).

Lemma inl_can_fun_ax S i : inc i (isI S) -> lf_axiom (fun x => class (inl_equiv S) (J x i)) (Vg (isE S) i) (inductive_limit S).

Lemma inl_can_fun_ev S i x: inc i (isI S) -> inc x (Vg (isE S) i) -> Vf (inl_can_fun S i) x = class (inl_equiv S) (J x i). Lemma inl_can_fun_fp S i: inc i (isI S) -> function_prop (inl_can_fun S i) (Vg (isE S) i) (inductive_limit S). Lemma inl_can_fun_prop S i j (f := isf S) (fi := inl_can_fun S i) (fj := inl_can_fun S j): gle (isr S) i j -> (fj \coP Vg f (J i j) /\ fi = fj \co (Vg f (J i j))).

We show that some quantities depend only on the data of S.

Lemma inl_equiv_Iv S S':

inl_same_data S S' -> inl_equiv S = inl_equiv S'. Lemma inductive_limit_Iv S S': inl_same_data S S' -> inductive_limit S = inductive_limit S'. Lemma inl_can_fun_Iv S S' i: inl_same_data S S' -> inl_can_fun S i = inl_can_fun S' i.

José Grimm

Assume

Bourbaki has a complicated argument to show existence: he starts by defining a mapping v : G → F that agrees with u i on E i for each i ∈ I. This is possible as the union is disjoint (Chapter II, §4, no. 7, Proposition 8). In fact, if x ∈ E i then v(x, i ) = u i (x). This function is compatible with the equivalence relation R (Chapter II, §6, no. 5) [if (x, i ) and (y, j ) are related by the equivalence, then v(x, i ) = v(y, j ), see above]. So, there is a unique mapping

Definition inl_map_property S u F g:= function_prop g (inductive_limit S) F /\ forall i, inc i (isI S) -> (Vg u i) = g \co (inl_can_fun S i).

Definition inl_map_val u := fun y => Vf (Vg u (Q (rep y))) (P (rep y)). Definition inductive_map S u F:= Lf (inl_map_val u) (inductive_limit S) F. Lemma inl_map_compat0 S u F i j x: inl_map_compat S u F -> gle (isr S) i j -> inc x (Vg (isE S) i) -> (Vf (Vg u i)) x = Vf (Vg u j) (Vf (Vg (isf S) (J i j)) x). Lemma inl_map_property_res1 S u F g i x:

inl_map_compat S u F -> inl_map_property S u F g -> inc i (isI S) -> inc x (Vg (isE S) i) -> Vf g (class (inl_equiv S) (J x i)) = Vf (Vg u i) x. Lemma inl_map_unique S u F g g':

inl_map_compat S u F -> inl_map_property S u F g -> inl_map_property S u F g' -> g = g'.

Remark. If every f i j is injective, so is f i . In this case, one can identify E i with f i 〈E i 〉, so consider E as the union of the E i .

Lemma inl_can_fun_inj S:

(forall p, inc p (isr S) -> injection (Vg (isf S) p)) -> (forall i, inc i (isI S) -> injection (inl_can_fun S i)).

Converse. Consider a directed set I, an increasing family of sets F i indexed by I (i ≤ j implies F i ⊂ F j ). Take for f i j the canonical injections F i → F j . This gives an inductive system S. Let F = lim --→ F i .

Section InlRemark.

Variables (I r F:Set).

Hypotheses (or: preorder r)(sr: substrate r = I) (rdr: right_directed_on r I).

Hypotheses (fgF: fgraph F) (df: domain F = I). Hypothesis Fmon: forall i j, gle r i j -> sub (Vg F i) (Vg F j).

Definition inl_remark_f := Lg r (fun p => (canonical_injection (Vg F (P p)) (Vg F (Q p)))).

Definition inl_remark_S: inductive_system. Lemma inl_remark_S_prop: inductive_system_on inl_remark_S F I r inl_remark_f.

Let u i be the canonical injection F i → F i . This family of functions satisfies the property of the Proposition, and by (b) and (c), there is is a bijection u : lim --→ F i → F i . This means that the two sets can be identified. The relation u i = u • f i allows us to identify f i with u i .

Definition inl_remark_U := unionb F. Definition inl_remark_ui := Lg I (fun i => canonical_injection (Vg F i) inl_remark_U).

Lemma inl_remark_sub i: inc i I -> sub (Vg F i) inl_remark_U. Lemma inl_remark_compat: inl_map_compat inl_remark_S inl_remark_ui inl_remark_U.

Lemma inl_remark_bijection: bijection_prop (inductive_map inl_remark_S inl_remark_ui inl_remark_U)

We can now define u.

Definition inductive_limit_fun S S' u := inductive_map S (inl_map2_aux S' u) (inductive_limit S').

Lemma inl_map2_prop S S' u (g := inductive_limit_fun S S' u): inl_same_index S S' -> inl_map2_compat S S' u -> inl_map2_property S S' u g.

Lemma inl_map2_unique S S' u g g': inl_same_index S S' -> inl_map2_compat S S' u-> inl_map2_property S S' u g -> inl_map2_property S S' u g' -> g = g'.

Lemma inl_map2_prop3 S S' u (f := inductive_limit_fun S S' u): inl_same_index S S' -> inl_map2_compat S S' u -> function_prop f (inductive_limit S) (inductive_limit S') /\ forall i x, inc i (isI S) -> inc x (Vg (isE S) i) -> Vf f (class (inl_equiv S) (J x i)) = class (inl_equiv S') (J (Vf (Vg u i) x) i).

Corollary 2. Consider three systems S, S , S and functions

Proposition 7. Same assumptions as in Corollary 1. If each u i is injective (resp. surjective), so is lim --→ u i .

Bourbaki proves injectivity via Proposition 6 and Lemma 1. The direct proof is as follows. Assume u(x) = u(y). Let's assume that x = C S (x , i ), so that u(x) = C S ((u i (x ), i ). Similarly, u(y) = C S (u j (y ), j ). So, there is k such that i ≤ k, j ≤ k and f ki (u i (x )) = f k j (u j (y )). This José Grimm can be rewritten as u k ( f ki (x )) = u k ( f ki (y )). By injectivity of u k , (x , i ) and (y , j ) belong to the same class. Surjectivity: if y ∈ lim --→ S , then there is y and i such that y = C S (y , i ). Since y ∈ E i and u i is surjective, there is x such that u i (x ) = y . Then u(C S (x , i )) = y. This is simpler than the argument of Bourbaki.

Lemma inl_limit_fun_inj S S' u:

inl_same_index S S' -> inl_map2_compat S S' u -> (forall i, inc i (isI S) -> injection (Vg u i)) -> injection (inductive_limit_fun S S' u).

Lemma inl_limit_fun_surj S S' u:

inl_same_index S S' -> inl_map2_compat S S' u -> (forall i, inc i (isI S) -> surjection (Vg u i)) -> surjection (inductive_limit_fun S S' u).

An inductive system of subsets of the E i is a family M i indexed by I such that M i ⊂ E i and f j i 〈M i 〉 ⊂ M j . Let g j i be the restriction of f j i as a function M i → M j . Then (M i , g i j ) is an inductive system.

Lemma inl_subfam_prop1 S M (g := inl_subfam_fct S M): inl_subfam_hyp S M -> [/\ forall z, inc z (isr S) -> restriction2_axioms (Vg (isf S) z) (Vg M (P z)) (Vg M (Q z)), forall i j x, gle (isr S) i j -> inc x (Vg M i) -> Vf (Vg g (J i j)) x = Vf (Vg (isf S) (J i j)) x, forall i, inc i (isr S)-> function_prop (Vg g i) (Vg M (P i)) (Vg M (Q i)), forall i j k, gle (isr S) i j -> gle (isr S) j k -> Vg g (J j k) \co Vg g (J i j) = Vg g (J i k) & forall i, inc i (isI S) -> Vg g (J i i) = identity (Vg M i)].

Definition inductive_system_subsets S M (H:inl_subfam_hyp S M) : inductive_system. Lemma inl_subsets_prop S M (H:inl_subfam_hyp S M) :

inductive_system_on (inductive_system_subsets H) M (isI S) (isr S) (inl_subfam_fct S M).

Lemma inl_subsets_prop_Iv S M (H H':inl_subfam_hyp S M) : inl_same_data (inductive_system_subsets H) (inductive_system_subsets H').

Lemma inl_subsets_prop_I2v S S' M (H:inl_subfam_hyp S M) (H':inl_subfam_hyp S' M) : inl_same_data S S' -> inl_same_data (inductive_system_subsets H) (inductive_system_subsets H').

José Grimm

Hypothesis Mhyp: inl_subfam_hyp S M. Definition inl_p7c1_M' := Lg (isI S) (fun i => Vfs (Vg u i) (Vg M i)).

Lemma inl_sub_fam_im1: inl_subfam_hyp S' inl_prop7_cor_M'.

We define now S M and S M the two inductive systems associated to M i and M i . So lim --→ M i = lim --→ S M and lim --→ u i 〈M i 〉 = lim --→ S M . Let j i and j i be the canonical inclusions M i → E i and M i → E i . In (3.26), Bourbaki identifies the source and image of lim --→ j i and lim --→

Let A be the image of lim --→ j i and A the image of lim --→ j i . The formula becomes u〈A〉 = A . Note that A is a subset of the source of u, so that the formula makes sense.

Assume t ∈ u〈A〉. There is i ∈ I and x ∈ M i such that t = u(C S (x, i )) = C S (u i (x), i ). By definition u i (x) ∈ M i so that t ∈ A . Conversely if t ∈ A then t = C S (y, i ) where y ∈ M i so that y = u i (x) for some x ∈ M i . So t = u(C S (x, i )). We conclude by noting that the argument of u belongs to A.

Lemma inl_p7c1_ji_prop : injection_prop inl_p7c1_ji_lim (inductive_limit inl_p7c1_MS) (inductive_limit S). Lemma inl_p7c1_ji'_prop : injection_prop inl_p7c1_ji_lim' (inductive_limit inl_p7c1_MS') (inductive_limit S').

Lemma inl_prop7_cor_i:

Imf inl_p7c1_ji_lim' = Vfs (inductive_limit_fun S S' u) (Imf inl_p7c1_ji_lim). End InductiveLimitCorollary1.

Part (ii). We first show that if M i ⊂ E i is such that f j i 〈M i 〉 ⊂ M j , then the family u -1 i (M i ) is a direct family of subsets. We then consider M i = {a i } and assume f j i (a i ) = a j . Then whenever i and j belong to I, we have C S (a i , i ) = C S (a j , j ). This relation holds in particular when j is the representative of I (note: i ∈ I says that I is non-empty). We write N i = u -1 i (a i ), and let j i be the canonical injection N i ⊂ E i . We define S to be the inductive system associated to N i , and lim --→ j i the inductive limit of the canonical injections, this is an injection lim --→ S → lim --→ S. Section InductiveLimitCorollary2.

Variable a_fam: Set. Hypothesis a_fam_prop: inl_inv_image_compat1 a_fam.

Lemma inl_sub_fam_im3: inl_subfam_hyp S inl_7c2_Ni. Lemma inl_sub_fam_im3_val: forall i, inc i (isI S) -> class (inl_equiv S') (J (Vg a_fam i) i) = class (inl_equiv S') (J (Vg a_fam (rep (isI S))) (rep (isI S))).

Definition inl_p7c2_S'' := (inductive_system_subsets inl_sub_fam_im3). Definition inl_p5c2_ip := inductive_limit_fun inl_p7c2_S'' S inl_p7c2_ci.

Let's prove the result: lim --→

Note that the RHS of this equation is a subset of the source of u, so a subset of lim --→ S; we pretend that it is the image of lim --→ j i (recall that Bourbaki identifies the source lim --→ S with the image).

Consider first t ∈ u -1 ( ā). This means u(t ) = ā, where t ∈ lim --→ S, so that t = C S (x i , i ) for some i ∈ I and x i ∈ E i . By definition of u, we have u(t ) = C S (u(x i ), i ). On the other hand, ā is (by definition) C S (a k , k) for some k ∈ I (as shown above, this is independent of k and we may chose k = i ). So C S (u(x i ), i ) = C S (a i , i ) and there exists j , such that i ≤ j and f j i (a i ) = f j i (u i (x i )). This simplifies to a j = u i ( f j i (x i )), and says that y = f j i (x i ) belongs to N j . Now

, so that t is in the image of lim --→ j i . Converse. Assume that t is in the image, so t = C S (x i , i ) for some x i ∈ N i . In particular

Lemma inl_sub_fam_im4: injection_prop inl_p7c2_ip (inductive_limit inl_p7c2_S'') (inductive_limit S).

José Grimm

Lemma inl_prop7_cor_ii (a := class (inl_equiv S') (J (Vg a_fam (rep (isI S))) (rep (isI S)))): Imf inl_p7c2_ip = Vfi1 (inductive_limit_fun S S' u) a. End InductiveLimitCorollary2. End InductiveLimitCorollary.

Remark.

Assume that u i is a family of functions satisfying (3.21), with target E instead of F. According to example 2, define E i = E and take for f j i the identity function. This gives an inductive system S , and lim --→ S can be identified with E . If u i is considered as a mapping E i → E i , then (u i ) is a direct system of mappings, and the function u defined by (3.22) can be identified with lim --→ u i .

Section InlRemark2.

Variables (S: inductive_system) (u E': Set). Hypothesis mcu: inl_map_compat S u E'.

Definition inl_rem2_S' := Injex2_system E' (is_preorder_r S) (is_substrate_r S) (@is_directed_r S).

Lemma inl_rem2_prop1: inl_map2_compat S inl_rem2_S' u.

Lemma inl_rem2_prop2 (u1 := inductive_map S u E') (u2:= inductive_limit_fun S inl_rem2_S' u) (can := Lf (fun z => (P (rep z))) (inductive_limit inl_rem2_S') E'): nonempty (isI S) -> can \coP u2 /\ u1 = can \co u2. End InlRemark2.

Consider a system S and a subset J of I, assumed to be right directed (every pair in J is bounded above by an element of J); this implies that the preorder r induced on J is right directed. If we restrict the sets and functions of S to J and r we get an inductive system, it is said to be obtained by restricting the index set to J. Let f i be the canonical mapping; then the ( f j ) j ∈J form an inductive system of mappings. Let g = lim --→ f i . This function is called canonical.

Definition sub_right_directed J r := sub J (substrate r) /\ (right_directed_on r J). Definition inl_restr S J (H:sub_right_directed J(isr S)) : inductive_system.

Lemma inl_restr_prop S J (H:sub_right_directed J(isr S)) :

inductive_system_on (inl_restr H) (restr (isE S) J) J (induced_order (isr S) J) (restr (isf S) (induced_order (isr S) J)).

Lemma inl_restr_cf_compat S J (H:sub_right_directed J(isr S)): inl_map_compat (inl_restr H) (Lg J (inl_can_fun S)) (inductive_limit S).

Definition inl_restr_cf S J (H:sub_right_directed J(isr S)):= (inductive_map (inl_restr H) (Lg J (inl_can_fun S)) (inductive_limit S)).

Lemma inl_restr_cf_compat2 S J (H:sub_right_directed J(isr S)): function_prop (inl_restr_cf H)

José Grimm

The inductive limit will be denoted by E or lim --→ α,λ E λ α . Fix λ ∈ L. Define g λ βα = f λλ βα so that the previous relation becomes

This allows us to define S λ an inductive system on E λ α indexed by I, let F λ be the inductive limit, and g λ α be canonical mapping. Fix λ and µ; let 2 h µλ α = f µλ αα . This is (again by (3.29)) an inductive system of mappings, let's denote its limit by h µλ . We have (3.31)

so that we can define an inductive system S on L. The objective is to prove that lim ← --S and lim ← --S are canonically isomorphic.

Section DoubleInductiveLimit.

Variables I1 I2 r1 r2: Set. Hypothesis (or1: preorder r1)(or2: preorder r2) (sr1: substrate r1 = I1)(sr2: substrate r2 = I2) (dr1: right_directed_on r1 I1) (dr2: right_directed_on r2 I2).

Variable S : inductive_system. Hypothesis Sr: isr S = prod_of_relation r1 r2.

Lemma inl_dl_I: isI S = I1 \times I2.

We define here S λ and F λ .

Definition inl_dl_Elam_fam lam := Lg I1 (fun i => Vg (isE S) (J i lam)). Definition inl_dl_glam_fam lam := Lg r1 (fun ij => Vg (isf S) (J (J (P ij) lam) (J (Q ij) lam))).

Lemma inl_dl_index_p1 lam i: inc lam I2 -> inc i r1 -> gle (isr S) (J (P i) lam) (J (Q i) lam). Lemma inl_dl_index_p2 lam mu i: gle r2 lam mu -> inc i I1 -> gle (isr S) (J i lam) (J i mu).

Definition inl_dl_S_lambda lam (Hl: inc lam I2) : inductive_system.

Lemma inl_dl_S_lambda_prop lam (Hl: inc lam I2) : inductive_system_on (inl_dl_S_lambda Hl) (inl_dl_Elam_fam lam) I1 r1 (inl_dl_glam_fam lam).

Definition inl_dl_system_S_lambda lam := match (ixm (inc lam I2)) with | inl hx => (inl_dl_S_lambda hx) | inr _ => S end.

Definition inl_dl_F_lambda lam := inductive_limit (inl_dl_system_S_lambda lam).

2 The English Edition of Bourbaki has h µλ α = f λµ αα , which is a typo.

We introduce h µλ α , the limit h µλ and prove (3.31).

Definition inl_dl_halm_fam lam mu:= Lg I1 (fun i => Vg (isf S) (J (J i lam) (J i mu))).

Definition inl_dl_hlm lam mu (H: gle r2 lam mu) := inductive_limit_fun (inl_dl_S_lambda (pidl_i1_L sr2 H)) (inl_dl_S_lambda (pidl_i2_L sr2 H)) (inl_dl_halm_fam lam mu).

Lemma inl_dl_halm_compat lam mu (H: gle r2 lam mu): inl_map2_compat (inl_dl_S_lambda (pidl_i1_L sr2 H)) (inl_dl_S_lambda (pidl_i2_L sr2 H)) (inl_dl_halm_fam lam mu).

Lemma inl_dl_hlm_compose l m n (Hlm : gle r2 l m) (Hmn: gle r2 m n): (inl_dl_hlm Hmn) \co (inl_dl_hlm Hlm) = (inl_dl_hlm (proj33 or2 _ _ _ Hlm Hmn)).

We now define h µλ everywhere via the axiom of choice, then S .

Definition inl_dl_hlm_gen x := match (ixm (inc x r2)) with | inl hx => (inl_dl_hlm (pidl_i3_L or2 hx)) | inr _ => emptyset end.

Lemma inl_dl_hlm_fct lm: inc lm r2 -> function_prop (inl_dl_hlm_gen lm) (inl_dl_F_lambda (P lm))(inl_dl_F_lambda (Q lm)).

Lemma inl_dl_S_lambda_Iv2 x y (H1: inc x I2) (H2: inc y I2) : x = y -> inl_same_data (inl_dl_S_lambda H1)(inl_dl_S_lambda H2).

Lemma inl_dl_hml_invariant i j (H:gle r2 i j) : inl_dl_hlm H = inl_dl_hlm_gen (J i j).

Lemma inl_dl_hml_id i: inc i I2 -> Vg (Lg r2 inl_dl_hlm_gen) (J i i) = identity (inl_dl_F_lambda i). Definition inl_dl_systemS': inductive_system.

Lemma inl_dl_systemS'_prop: inductive_system_on inl_dl_systemS'

(Lg I2 inl_dl_F_lambda) I2 r2 (Lg r2 inl_dl_hlm_gen).

So far, we followed the proof of the projective case. We consider now u λ α , the composition of the canonical mapping E λ α → F λ and F λ → F; we show that it forms a system of mappings, and that its limit is the desired bijection. We have

Justifications for the equalities: by definition of u α β ; by the properties of f ; by definition of g Lemma inl_dl_fg_prop1 i l (H:inc l I2): inl_dl_fg i l = (inl_can_fun (inl_dl_S_lambda H) i). Lemma inl_dl_fg_fp i l (Hi: inc i I1) (Hl: inc l I2):

function_prop (inl_dl_fg i l) (Vg (isE S) (J i l)) (inductive_limit (inl_dl_S_lambda Hl)).

Lemma inl_dl_fh_cp p (

Lemma inl_dl_fu_compat: inl_map_compat S inl_dl_fu (inductive_limit (inl_dl_systemS')).

Lemma inl_dl_bijection: bijection_prop (inductive_map S inl_dl_fu (inductive_limit inl_dl_systemS')) (inductive_limit S) (inductive_limit inl_dl_systemS').

End DoubleInductiveLimit.

The result is straightforward. What we prove is that the following diagram is commutative, where the vertical arrows are the bijections defined in Proposition 10.

(lim

Variables (SE SE' SF SF': inductive_system).

Variables u u': Set. Hypotheses (si1:inl_same_index SE SE') (si2:inl_same_index SE SF) (si3:inl_same_index SF SF'). Hypotheses (cu:inl_map2_compat SE SF u) (cu':inl_map2_compat SE' SF' u').

Exercises

The 1956 edition of Bourbaki [1] defines inductive and projective limits as no. 11 and 12 of §1, instead of §7, as applications of no. 10 (directed sets). Moreover conditions (LI II ) and José Grimm (LP II ) are missing. Exercises 24 and 29 explain that adding these constrains yields canonically isomorphic objects.

Let's consider a projective system E, I, r , f , but without the condition that f i i is the identity function, and define lim ← --E as the subset of E i formed of all sequences (x i ) i ∈I such that x i = f i j (x i ) whenever i ≤ j .

Variables E I r f: Set. Hypothesis (preorder_r: preorder r) (substrate_r: substrate r = I)

This relation says that the E i form a projective system S of subsets of the E i , and equation (3.9) reads lim ← --

and we shall prove this relation (without establish (3.9) in a context where (LP II ) is missing. Notre that, if

so that S satisfies (LP II ).

Definition noid_E := Lg I (fun i => Imf (Vg f (J i i))). Definition noid_f := Lg r (fun z => restriction2 (Vg f z)

Definition noid_proj_system: projective_system. Lemma noid_prop2: projective_system_on noid_proj_system noid_E I r noid_f. Lemma noid_prop3 : projective_limit(noid_proj_system) = noid_projlim. ProjectiveLimitNoId.

Consider now the case of an inductive limit. The assumptions are the same as above (we assume however that I is right directed). The set E i is defined as above, while g i j is the restriction (the other way around).

The following lemmas are proved as above. In particular we can define an inductive system S based on the sets E i .

Vf (Vg noid_g (J i j)) x = Vf (Vg f (J i j)) x. Lemma noid_prop5d i: inc i r -> function_prop (Vg noid_g i) (Vg noid_E' (P i)) (Vg noid_E' (Q i)). Lemma noid_prop5e i: inc i I -> Vg noid_g (J i i) = identity (Vg noid_E' i). Lemma noid_prop5f i j k: gle r i j -> gle r j k -> Vg noid_g (J j k) \co Vg noid_g (J i j) = Vg noid_g (J i k). Lemma noid_prop5g y i j k: gle r i j -> gle r j k -> inc y (

Definition noid_ind_system: inductive_system. Lemma noid_prop6: inductive_system_on noid_ind_system noid_E' I r noid_g.

Let's define an equivalence relation on the disjoint union of the E

equalities say that there is an upper bound k of i and j such that f ki (x) = f k j (y), where f can be replaced by g ). This equation means that we can define an injection φ :

Definition noid_inl_equiv := graph_on noid_inl_equiv_rel noid_inl_sum. Definition noid_limit := quotient noid_inl_equiv.

José Grimm

]. Lemma noid_inl_equiv_reflexive a: inc a noid_inl_sum -> noid_inl_equiv_rel a a. Lemma noid_inl_equiv_esr: equivalence_on noid_inl_equiv noid_inl_sum.

Lemma noid_inl_class_eq x y: inc x noid_inl_sum -> inc y noid_inl_sum -> (class noid_inl_equiv x = class noid_inl_equiv y <-> noid_inl_equiv_rel x y).

Lemma noid_inl_class_ii i x (y := Vf (Vg f (J i i)) x):

Lemma noid_inl_class_compat i j x y (R := (inl_equiv noid_ind_system) ): inc i I -> inc j I -> inc x (Vg noid_E' i) -> inc y (Vg noid_E' j) -> (class R (J x i) = class R (J y j) <-> class noid_inl_equiv (J x i) = class noid_inl_equiv (J y j)).

We now formally define φ and show that it is a bijection, which is rather trivial.

Definition noid_can x := class noid_inl_equiv (J (P (rep x)) (Q (rep x))). Lemma noid_inl_prop7 (A := inductive_limit noid_ind_system) (B:= noid_limit): bijection_prop (Lf noid_can A B) A B. End InductiveLimitNoId.

Exercise 1. « Let I be a directed set, let (J λ ) λ∈L be a family of subsets of I, indexed by a directed set L, such that (i) for each λ ∈ L, J λ is directed with respect to the induced ordering; (ii) the relation λ ≤ µ implies J λ ⊂ J µ ; (iii) I is the union of the family (J λ ). Let (E α , f αβ ) be an inverse system of sets relative to I, let E be its inverse limit, and for each λ ∈ L let F λ be the inverse limit of the system obtained from (E α , f αβ ) by restricting the index set to J λ . For λ ≤ µ, let g λµ be the canonical mapping of F µ into F λ . Show that (F λ , g λν ) is an inverse system of sets relative to L, and define a canonical bijection of F = lim ← --F λ onto E. »

It happens that all conditions are not necessary; for instance, we only need preorders, and L has to be directed. We denote by i ≤ I j the order relation on I, and by i ≤ L j the relation on L. So the context will be the following:

Variables I rI L rL Jf: Set. Variable S: projective_system. Hypothesis rS: (psr S = rI). Hypotheses (HIp :preorder rI) (HIs: substrate rI = I). Hypotheses (HLp :preorder rL) (HLs: substrate rL = L) (HLd:right_directed_pre rL). Hypothesis (HJg: fgraph Jf) (HJd: domain Jf = L) (HJI: unionb Jf = I) (HJm: forall i j, gle rL i j -> sub (Vg Jf i) (Vg Jf j)).

We start with some trivial properties. The last lemma says under which condition the order induced on J i by ≤ I would make it a directed set. Inria Lemma ex1_prop1 i: inc i L -> sub (Vg Jf i) I. Lemma ex1_prop2 i j: gle rL i j -> inc i L /\ inc j L. Lemma ex1_prop3: I = psI S. Lemma ex1_prop4 i: inc i L -> sub (Vg Jf i) (psI S). Lemma ex1_preorder i (ri:= induced_order rI (Vg Jf i)):

We define now the projective system S i obtained by restricting indices to J i , the projective limit F i , the canonical function g i : E → F i , and the functions g i j : F j → F i . Assume i ∈ L so that J i ⊂ I; in this case we can define S i ; in the general case, we use a version of the axiom of choice that says: it is decidable whether or not i ∈ L, and we can do case analysis in the definition.

The proof of the following lemmas is the following: unfold the definitions, exposing the match, then do a case analysis on (ixm (inc j L)); in the true case, the result is obvious, in the false case we have a contradiction with i ∈ L.

Lemma ex1_res0 i (H: inc i L): ex1_Fl i = (projective_limit (prl_restr (ex1_prop4 H))). Lemma ex1_prop5a j: inc j L -> (Vg Jf j) = psI (ex1_systemi j). Lemma ex1_prop5b i (H: sub (Vg Jf i) (psI S)): inc i L -> prl_same_data (prl_restr H) (ex1_systemi i).

A non-trivial property is ex1_prop6: if i ≤ L j , then S i has the same data as the system obtained by restricting the indices of S j to J i (we have to apply ex1_prop5b twice, then the property of double restriction). We deduce that g i j is a function M J → M i , which is the identity when i = j . A bit more complicated is that g i j • g j k = g i j . By ex1_res, the functions g i j and g j k can be composed; so that it suffices to prove g i j (g j k (x)) = g i j (x). it suffices to unfold g , and use ex1_prop7.

Lemma ex1_prop5 i j: gle rL i j -> sub (Vg Jf i) (psI (ex1_systemi j)). Lemma ex1_prop6 i j (lij: gle rL i j) :

prl_same_data (prl_restr (ex1_prop5 lij)) (ex1_systemi i). (* 7 *) Lemma ex1_prop6a i j (lij: gle rL i j) :

(projective_limit_restr (ex1_prop5 lij)) = (ex1_Fl i). Lemma ex1_prop7 i j: gle rL i j -> lf_axiom (restr^~(Vg Jf i)) (ex1_Fl j) (ex1_Fl i). (* 2 *) Lemma ex1_res2 i j: gle rL i j -> function_prop (ex1_gij (J i j)) (ex1_Fl j) (ex1_Fl i)).

José Grimm

Lemma ex1_res3 i: inc i L -> ex1_gij (J i i) = identity (ex1_Fl i). (* 2 *) Lemma ex1_pr4 i j k: gle rL i j -> gle rL j k -> ex1_gij (J i j) \co ex1_gij (J j k) = ex1_gij (J i k). (* 16 *)

We can now define the projective system with the functions g i j , let's call it S , and the projective limit E . If x is in the product of the E i , and i ∈ L we denote by (x) i the restriction of x to J i , and by (x) the functional graph x → x i . Moreover, we denote by φ the function x → (x). If x ∈ E, then (x) i ∈ M i , and φ(x) ∈ E (this is rather simple). Showing that φ is injective is easy, because (x) i (k) = x(k) whenever k ∈ J i (where t (k) is the value of t at k). In order to show that φ is surjective, we consider y and look for x such that (x) i = y(i ), so x(k) = y(i )(k); for every k in I there exists i such that k ∈ J i , but it is not unique. Claim 1: if i ≤ L i , then y(i ) is the restriction of y(i ) to J i (obvious by definition). Claim 2: if k ∈ J i and k ∈ J i , then y(i )(k) = y(i )(k). In fact, there is i ∈ L such that i ≤ L k and i ≤ L k . By claim 1, y(i )(k) and y(i )(k) are equal to y(i )(k). We can define (via the axiom of choice) a function i (k) such that k ∈ J i (k) , and a function x by x(k) = y(i (k))(k). Claim 3: if k ∈ J i , then x(k) = y(i )(k) (obvious). Claim 4: y(i ) belongs to the projective limit obtained from S, by restricting indices to J i , obvious by definition; this means y(i ) ∈ k∈J i E k and f ab (y(i )(b)) = y(i )(a) whenever a ≤ I b. Claim 5: x ∈ E k (by claim 4). Claim 6, φ(x) = y. Obviously, both terms are functional graphs defined on L; it suffices to show φ(x)(i ) = y(i ). Both quantities are functional graphs with domain J i , it suffices to show φ(x)(i )(k) = y(i )(k). By definition of φ, the LHS is x(k); the result holds by claim 3. Finally x ∈ E. This means:

. Take i such that i (a) ≤ L i and i (a) ≤ L i , and use claim 2 twice. We get f ab (y(i )(b)) = y(i )(a), which holds by claim 4.

Lemma ex1_F_can_bf: bijection ex1_F_can. (* 75 *) Exercise 2. « Let (E α , f αβ ) be an inverse system of sets relative to a directed index set, let E = lim ← --E α and let f α : E → E α be the canonical mapping for each α. Show that, if all the f αβ are injective, then f α is injective. » Proof. Consider x and y in E such that f i (x) = f i (y); this means x i = y i . In order to show x = y, it suffices to show x j = y j for every j . Assume the order right directed, so that for some k, we have i ≤ k and j ≤ k. Since x and y are in the limit, the assumption becomes f i k (x k ) = f i k (y k ) and the conclusion becomes f j k (x k ) = f kk (y k ). By injectivity x k = y k , the conclusion follows.

Lemma Exercise7_2 S:

right_directed (psr S) -> (forall i j, gle (psr S) i j -> injection (Vg (psf S) (J i j))) -> forall i, inc i (psI S) -> injection (prl_can_fun S i). (* 20 *)

Exercise 3. « Let (E α , f αβ ) and (F α , g αβ ) be two inverse systems of sets relative to the same index set I. For each α ∈ I, let u α be a mapping of E α into F α , such that the u α form an inverse system of mappings. Let G α ⊂ E α × F α be the graph of u α . Show that (G α ) is an inverse system of subsets of E α ×F α and that its inverse limit may be canonically identified with the graph of

Note that the main Bourbaki text does not define the product of the two systems, but we have considered it. Proving that (G i ) is a projective system of subsets is straightforward.

Variables S S': projective_system. Variable (u:Set). Hypothesis same_I: (prl_same_index S S'). Hypothesis (Hu: prl_map2_compat S S' u). Exercise 4. « Let I be a non-empty directed set with no greatest element, and let F be the set of all sequences x = (α 1 , α 2 , . . . , α 2n-1 , α 2n ) of an even number ≥ 2 of elements of I with the following properties:

(a) For each α ∈ I, let E α be the set of all x ∈ F such that r (x) = α. Then E α is non-empty. For α ≤ β in I, we define a mapping f αβ of E β into the set of all finite sequences of elements of I, as follows: if

let j be the least index such that α ≤ α 2 j -1 ; then

Show that f αβ (E β ) = E α , and that (E α , f αβ ) is an inverse system of sets relative to I.

José Grimm

(b) Show that if x α ∈ E α and x β ∈ E β are such that there exists an index γ for which γ ≥ α and γ ≥ β, and an element x γ ∈ E γ for which x α = f αγ (x γ ) and x β = f βγ (x γ ), then, provided also that x α and x β have the same length, we have s(x α ) = s(x β ).

(c) Deduce from (b) that, if E = lim ← --E α is not empty and if y = (x α ) ∈ E, then the set of elements s(x α ) is countable and cofinal in I.

(d) Let I be the set of all finite subsets of an uncountable set A, ordered by inclusion. Show that I has no countable cofinal subset, and hence deduce from (c) and example of an inverse system of sets (E α , f αβ ) in which the E α are non-empty and the f αβ are surjective, but for which E = lim ← --E α = .

(e) Deduce from (d) an example of an inverse system of mappings

Answer. We first introduce some properties (H) of I and its order r . Then we show that there is an example satisfying a stronger conditions (H ). We then prove (a), (b) and (c) in a context where (H) holds, then prove (d), (e). Note that (H) holds if I is the set of finite subsets of an infinite set, ordered by inclusion (if x ∈ I, it is a strict subset of A, so that there is t in A not in I). Assume B cofinal. Then B = A (if x ∈ A, then {x} is bounded above by an element y of B, so x ∈ y). Since elements of B are finite, A and B have the same cardinal (in fact, we show a weaker statement: if B is countable, so is A). As an example, we can take A = P(N). If x ∈ I, there is y not smaller than x; if x ≤ z and y ≤ z we cannot have x = z; so x < z. There are x 0 and x 1 such that x 0 < x 1 , this will say that F is non-empty. Section Exercise4. Variable I r: Set. Hypothesis ex4H:ex4_prop_IR I r. Lemma ex4_or_prop0 i j: gle r i j -> inc i I /\ inc j I. Lemma ex4_no_greater x: inc x I -> exists y, glt r x y. (* 7 *) Lemma ex4_or_prop1: exists x y, glt r x y.

Instead of the Bourbaki definition of F, we shall use a variant; an element will be a list of pairs, say (a i , b i ), where indices start with zero. So, r (x) = a n-1 and s(x) = b n-1 . Moreover α 2i -1 = a i and α 2i = b i . The conditions become: a i < b i for i < n and a i ≤ a j for j < i < n, where n is the length of the list. Note that F is the set of all z, such that (a) z is a functional graph, its domain is a subset of N, its range is a subset of I × I, and (b) the domain of z is a non-zero integer n and some other property holds (recall that n is equal to the set of integers < n, so is a subset of N). We now define E α and f αβ . This function is obtained by truncating its argument to the j first terms (operation that obvious yields an element of F) then modifying the value of r . This yields an element of F provided that the new value is ≤ r (x) (in order to preserve r < s) but not ≤ to the other a i .

Definition ex4_setEi i := Zo ex4_F (fun z => ex4_fct_r z = i). Lemma ex4_setEi_nonempty i: inc i I -> nonempty(ex4_setEi i).

José Grimm

Lemma ex4_modify_r_r x i: inc x ex4_F -> ex4_fct_r (ex4_modify_r x i) = i. (* 4 *)

If i is the new value to insert, we take for j the first index such that i ≤ a j . It exists when i ≤ r (x). This is the correct way. We now define f αβ . In the special case α = β we have j = n -1. This means that the restriction is a no-op. Moreover the modification is trivial as well. So f i i is the identity function. In order to prove (LP I ), we consider i ≤ j ≤ k, and x with r (x) = k, truncate to length b, modify with j , truncate to length c, modify with i ; we can also directly truncate to truncate to length a, and modify with i . It is rather easy to show a = c, hence the conclusion. In order to show that f αβ is surjective, we take y ∈ E α and c such that β < c. Extend y so that x i = y i for i < n and x n = (β, c). Then f αβ (y) = x. Assume a ≤ c, b ≤ c, z ∈ F c , x = f ab (z) and y = f bc (z). This means that x and y are obtained by restricting z to size j and j and modifying r . If x and y have the same length, then j = j . As s is not modified, we have s(x) = s(y). This shows (b). Inria Take x ∈ lim ← --E, and S the set of all s(x i ) for i ∈ I. If i ∈ I, we have i = r (x i ) < s(x i ). So, S is cofinal in I. Let S n be the set of all elements t of S such that t = s(x i ) and x i has length n. By (b), S n has at most one element; so is finite, thus countable. Thus, S, being a countable union of countable sets is countable. This shows (c). Point (d) becomes trivial. Let S the system described in Example 2, where F = {0}. The projective limit is the diagonal of a given set; it is non-empty. For u i we take the constant function zero. Now lim ← --u i is a function whose source is empty and target is non-empty. It cannot be surjective. This terminates the proof. Exercise 5. « Let I be a directed set and let (E α ) α∈I be a family of lattices such that each E α , endowed with the opposite ordering is Noetherian ( §6, no. 5). For each pair (α, β) of indices in I such that α ≤ β let f αβ : E β → E α be an increasing mapping, and suppose that (E α , f αβ ) is an inverse system of sets relative to I. For each α ∈ I let G α be a non-empty subset of E α such that (i) no two distinct elements of G α are comparable, (ii)

. Under these conditions the inverse limit of the inverse system of subsets (G α ) is not empty. The proof runs as follows:

(a) Let J be a finite subset of I. A family (x α ) α∈J , where x α ∈ G α for all α ∈ J, is said to be coherent if it satisfies the following two conditions: (i) if α ∈ J, β ∈ J, α ≤ β, then x α = f αβ (x β ); (ii) for each upper bound γ of J in I there exists x γ ∈ G γ such that x α = f αγ (x γ ) for all α ∈ J. Show that for each upper bound γ of J in I, the set α∈J f -1 αγ (x α ) has a greatest element equal to inf α∈J (M αγ (x α )); furthermore the intersection of G γ and α∈J f -1 αγ (x α ) is the set (non-empty

José Grimm

by hypothesis) of all y γ ∈ G γ such that

(use condition (i)).

(b) Let J be any subset of I. A family x J = (x α ) α∈J where x α ∈ G α for all α ∈ J, is said to be coherent if every finite subfamily of x J is coherent. If J = I and if β ∈ I-J, show that there exists x β ∈ G β such that the family x J∪{β} = (x α ) α∈J∪{β} is coherent. (Using (a) and condition (iv), show that for every finite subset F of J, if γ is an upper bound of F ∪ {β}, then f βγ (G γ ∩ α∈F f -1 αγ (x α )) is the (non-empty) set of all y β ∈ G β which are ≤ f βγ (inf α∈F (M αγ (x α ))). Using the fact that E β endowed with the opposite ordering is Noetherian, show next that there exists a finite subset F 0 of J and an upper bound γ 0 of F 0 ∪{β} such that for each finite subset F of J and each upper bound γ of F ∪ {β} we have

Prove then that every element x β ∈ F β which is ≤ f βγ 0 (inf α∈F 0 (M αγ 0 (x α )) satisfies the required conditions.

(c) Finally, complete the proof by showing that there exists a coherent family whose index set is the whole of I. (Order the set of coherent families x J by the relation "x J is a subfamily of x K ", and apply (b) and Zorn's lemma.) » We consider a context, formed of a projective system S, two sets representing the family of lattices (L i ), and the family of sets (G i ). Both families are indexed by I, the index set of S. In what follows, we shall denote by ≤ i the order relation of L i ; the substrate is E i and whenever x and y belong to E i , the quantities max(x, y) and min(x, y) are defined as the maximum and minimum of x and y for ≤ i . We shall also assume that every non-empty subset of E i has a minimal element. If i ≤ j (where ≤ is the ordering of S), then f i j is a function E j → E i ; we assume it increasing for the order relations ≤ j and ≤ i .

Section Exercise5.

Variable S: projective_system. Variable Er Gf: Set.

Hypothesis rdr: right_directed_prop (psr S). Hypothesis fgEr: fgraph Er. Hypothesis dEr: domain Er = psI S. Hypothesis lEr: forall i, inc i (psI S) -> lattice (Vg Er i). Hypothesis sEr: forall i, inc i (psI S) -> substrate (Vg Er i) = Vg (psE S) i. Hypothesis sen: forall i X, inc i (psI S) -> sub X (Vg (psE S) i) -> nonempty X -> exists a, minimal (induced_order (Vg Er i) X) a. Hypothesis fm: forall p, inc p (psr S) -> increasing_fun (Vg (psf S) p) (Vg Er (Q p)) (Vg Er (P p)).

We introduce 8 assumptions G 1 , G 2 , G 3 , G 4 , G 5 , G 6 , G 7 , and G 8 . Assumptions G 1 , G 2 , G 4 and G 6 say that the family (G i ) can be considered as a projective system S of subsets of the E i , the objective is to show lim ← --S = . Assumption G 3 says that no G i is empty (which is obviously necessary). Assumption G 5 says that no two elements of G i are comparable (for ≤ i ). Assumption G 7 is condition (iii) and assumption G 8 is condition (iv).

Hypothesis ex5_G1: fgraph Gf. Hypothesis ex5_G2: domain Gf = psI S. Hypothesis ex5_G3: forall i, inc i (psI S) -> nonempty (Vg Gf i). Hypothesis ex5_G4: forall i, inc i (psI S) -> sub (Vg Gf i) (Vg (psE S) i). Hypothesis ex5_G5: forall i x y, inc i (psI S) -> inc x (Vg Gf i) -> inc y (Vg Gf i) -> x <> y -> ~(ocomparable (Vg Er i) x y). Hypothesis ex5_G6: forall i j, gle (psr S) i j -> Vfs (ex5_f i j) (Vg Gf j) = Vg Gf i. Hypothesis ex5_G7:forall i j x, gle (psr S) i j -> inc x (Vg Gf i) -> has_greatest (induced_order (Vg Er j) (Vfi1 (ex5_f i j) x)). Hypothesis ex5_G8: forall i j h x, gle (psr S) i j -> inc h (Vg (psE S) j) -> (exists2 y, inc y (Vg Gf j) & gle (Vg Er j) y h) -> inc x (Vg Gf i) -> gle (Vg Er i) x (Vf (ex5_f i j) h) -> exists x', [/\ inc x' (Vg Gf j), gle (Vg Er j) x' h & x = Vf (ex5_f i j) x'].

Lemma ex5_Gsubfams: prl_subfam_hyp S Gf.

Definition ex5_S' :=projective_system_subsets (ex5_Gsubfams).

Let X i j (x) = f -1 i j (x) be the set of all t such that f i j (t ) = x. If i ≤ j this is a subset of E j . Assumption G 7 says that, if x ∈ G i , X has a greatest element M i j (x).

Definition ex5_X i j x := Vfi1 (ex5_f i j) x. Definition ex5_M i j x := the_greatest (induced_order (Vg Er j) (ex5_X i j x)).

Lemma ex5_Gij_prop1 i j x: gle (psr S) i j -> inc x (Vg Gf j) -> (* 4 *) inc (Vf (ex5_f i j) x) (Vg Gf i). Lemma ex5_Gij_prop2 i j y: gle (psr S) i j -> inc y (Vg Gf i) -> (* 4 *) exists2 x, inc x (Vg Gf j) & y = Vf (ex5_f i j) x. Lemma ex5_Xij_pr i j x: gle (psr S) i j -> forall t, inc t (ex5_X i j x) <-> (inc t (Vg (psE S) j) /\ x = Vf (ex5_f i j) t). Lemma ex5_Xij_pr2 i j x: gle (psr S) i j -> sub (ex5_X i j x) (Vg (psE S) j). Lemma ex5_Mij_pr1 i j x (M:= ex5_M i j x): gle (psr S) i j -> inc x (Vg Gf i) -> inc M (ex5_X i j x) /\ forall t, inc t (ex5_X i j x) -> gle (Vg Er j) t M. (* 7 *) Lemma ex5_Mij_pr2 i j x (M:= ex5_M i j x): (* 3 *) gle (psr S) i j -> inc x (Vg Gf i) -> Vf (ex5_f i j) M = x /\ forall t, inc t (Vg (psE S) j) -> Vf (ex6_f i j) t = x -> gle (Vg Er j) t M.

We introduce

We assume that k is an upper bound of J in I. We have Y Jk (x) ⊂ E k . If J is non-empty then Y Jk (x) is the set of all t ∈ E k such that x i = f i k (t ) whenever i ∈ J.

Definition ex5_Y J k x := intersectionf J (fun i => ex5_X i k (Vg x i)). Definition ex5_inY J k x t :=

José Grimm

forall i, inc i J -> Vg x i = Vf (ex5_f i k) t. Definition ex5_upper_bd J k := inc k (psI S) /\ (forall i, inc i J -> gle (psr S) i k).

Lemma ex5_Y_prop1 J k x: ex5_upper_bd J k -> sub (ex5_Y J k x) (Vg (psE S) k). (* 5 *) Lemma ex5_Y_prop2 J k x: nonempty J -> ex5_upper_bd J k -> (* 5 *) forall t, inc t (ex5_Y J k x) <-> (inc t (Vg (psE S) k) /\ ex5_inY J k x t).

We introduce now

Assume that J is a non-empty finite subset of I, k an upper bound of J and x ∈ J G i , in other terms, x is a functional graph, with domain J, and i ∈ J implies

Since the number of terms in the inf is finite and E k is a lattice, it follows that m is effectively

Section Exercise5_prop_m.

Variables J k x: Set. Hypothesis (mp1: ex5_fneI J) (mp2: ex5_upper_bd J k)(mp3: ex5_prodG J x). We say that x is J-coherent if (C 1 ): J is a non-empty finite subset of I; (C 2 ): x ∈ i ∈J G j (in particular, this says that J is the domain of x); (C 3 ): x i = f i j (x j ) whenever i ≤ j in J; and C 4 : for every upper bound k of J, G k ∩ Y Jk (x) is non-empty.

Let x be J-coherent, k an upper bound of J. We pretend that m Jk (x) = max Y Jk (x). Obviously y ∈ Y implies y ≤ k m, so that it suffices to show m ∈ Y. Take i ∈ J. By definition of m,

Obviously, the LHS is a subset of the RHS. So, assume t

We say that x is coherent if x ∈ J G i and, whenever K is a finite non-empty subset of the domain of x, the restriction of x to K is K-coherent.

The objective here is to show that, if j ∈ J, there is an extension of x to J ∪ { j } that makes it coherent. We first consider the case J = . The problem simplifies to: there is t ∈ G j , such that, whenever j ≤ k, there is t

Definition ex5_extend x j a := (x +s1 (J j a)). Definition ex5_extend_prop x j x':= ex5_coherent2 (ex5_extend x j x').

Lemma ex5_res2 x j: ex5_coherent2 x -> inc j (psI S) -> domain x = emptyset -> exists x', ex5_extend_prop x j x'. (* 29 *)

The general case being non-trivial, we consider a section where x and j are fixed, J is the non-empty domain of x, x is coherent, j ∈ I -J. Section Exercise5b. Variables j x: Set. Let J' := domain x. Hypothesis coh2: ex5_coherent2 x. Hypothesis jJ : inc j (psI S) /\ ~(inc j J'). Hypothesis Jne: nonempty J'.

We denote by H(F, k) the property that F is a non-empty finite subset of J, k an upper bound of F and j ≤ k. We have (3.37)

Write the equation as f j k 〈A〉 = B, and note that A satisfies (3.36), it is the non-empty set of all t ∈ G k such that t ≤ k m. Assume y ∈ B. Apply condition G 8 with h β = m (for y β we can take any element of A). From y ≤ j f j k (m) we get: there is t ∈ A such that y = f j k (t ). Conversely, if y = f j k (t ) and t ≤ k m, we get f j k (t ) ≤ j f j k (m) and y ∈ B.

This allows us to define the set T of all coherent graphs, and order it by inclusion. Let X be a totally ordered subset of T, and x = X. Each t ∈ X is a functional graph, so that x is a graph. Assume a ∈ x, b ∈ x, a and b have the same first projections. Assume a ∈ t a , b ∈ t b . Since X is totally ordered, we have t a ⊂ t b or t b ⊂ t a . In the first case, a and b are in the functional graph t b , so that a = b. The same holds in the second case; so that x is a functional graph. Assume a ∈ t , t ∈ X, and let i be the first component of a. We have x(i ) = t (i ). Note that every i in the domain of x has this form. In particular x(i ) ∈ G i . This shows x ∈ G i . Consider now a non-empty finite subset K of the domain of x. By finite induction there is t ∈ X such that K is a subset of the domain of t (assume K = {a, b}, a is in the domain of t a , b is in the domain of t b ; one of t a and t b is the greatest for inclusion, let's says it is t a ; then K is a subset of t a ). The restriction of x to K is K-coherent since this is the restriction of t to K. It follows x ∈ X. By a corollary of Zorn's lemma, T has a maximal element x. The previous result shows that x can be extended when the domain is not I. So x has domain I and this concludes the proof.

Lemma ex5_result: nonempty (projective_limit ex5_S'). (* 80 *) Exercise 6. « Let I be a directed set, and let (J λ ) λ∈L be a family of subsets of I satisfying the conditions of Exercise 1. Let (E α , f βα ) be a direct system of sets indexed by I, let E = lim --→ E α , and for each λ ∈ L let F λ be the direct limit of the direct system obtained from (E α , f βα ) by restricting the index set to J λ . Whenever λ ≤ µ, let g µλ be the canonical mapping of F λ into F µ (no. 6). Show that (F λ , g µλ ) is a direct system of sets relative to L and define a canonical bijection of E onto F = lim --→ F λ . » Assumptions are as in Exercise 1, except that we need J i to be right directed for j ∈ L.

Section Exercise6.

Variables I rI L rL Jf: Set. Variable S: inductive_system.

Hypothesis rS: (isr S = rI). Hypotheses (HIs: substrate rI = I). Hypotheses (HLp :preorder rL) (HLs: substrate rL = L) (HLd:right_directed_on rL L). Hypothesis (HJg: fgraph Jf) (HJd: domain Jf = L) (HJI: unionb Jf = I) (HJm: forall i j, gle rL i j -> sub (Vg Jf i) (Vg Jf j)) (HJrd: forall j, inc j L -> right_directed_on rI (Vg Jf j)).

Some trivial properties. In particular, if i ∈ L, then J i ⊂ I; moreover, J i is right directed, so that we can define S i ; we generalize the definition by using the axiom of choice. We define F i = lim --→ S i . We give a lemma that explicits the fields of S i , in case i ∈ L. Assume i ≤ L j ; from J i ⊂ J j we deduce that J i is a right directed subset of the substrate of the order of S j . The system formed from S j by restricting the index set to J i has the same data as S i . Lemma ex6_prop1 i: inc i L -> sub (Vg Jf i) I. Lemma ex6_prop2 i j: gle rL i j -> inc i L /\ inc j L. inl_equiv (ex6_systemi i) = inl_equiv (inl_restr (ex6_prop4 H)). Lemma ex6_prop6b i j (H:gle rL i j): inl_equiv (ex6_systemi i) = inl_equiv (inl_restr (ex6_prop5c H)). Lemma ex6_res1 i j (H: gle rL i j): ex6_Fl i = (inductive_limit (inl_restr (ex6_prop5b H))).

José Grimm

We define here g j i as some inductive map. Assume i ≤ L j , so that i and j belong to L. Then g j i is the canonical function S i → S j . It is the identity function when i = j . Moreover, it satisfies (LI I ) so that one can define an inductive system with the F i and g i j , let's call it S .

Lemma ex6_gij_prop1 i j (H:gle rL i j): ex6_gij (J i j) = inl_restr_cf (ex6_prop5c H).

Lemma ex6_res2 i j: gle rL i j -> function_prop (ex6_gij (J i j)) (ex6_Fl i) (ex6_Fl j). (* 2 *) Lemma ex6_res3 i: inc i L -> ex6_gij (J i i) = identity (ex6_Fl i). Lemma ex6_res4 i j k: gle rL i j -> gle rL j k -> ex6_gij (J j k) \co ex6_gij (J i j) = ex6_gij (J i k).

Definition ex6_F: inductive_system. Lemma ex6_F_prop: inductive_system_on ex6_F (Lg L ex6_Fl) L rL (Lg rL ex6_gij).

Let's define a canonical injection f : lim --→ S → lim --→ S. If x ∈ lim --→ S , there exists j ∈ J, i ∈ J j and y ∈ E i such that x = C S (C S j (y, i ), j ). Write this as x = W(y, i , j ). Note that the value of Inria W does not change if j is replaced by j when j ≤ L j . So we can define f (x) = C S (y, i ). This belongs to lim --→ S since i ∈ I. Assume f (x) = f (x ) so C S (y, i ) = C S (y , i ). There is i such that f i i (y) = f i i (y ). This implies C S k (y, i ) = C S k (y , i ), whenever k is big enough (there is j such that i ∈ J j ; we need i ≤ L k). One deduces W(y, i , k) = W(y , i , k). If moreover i ≤ L k and i ≤ L k, one deduces x = x so that f is injective.

Consider now an element of lim --→ S, say y = C S (z, i ). Since i ∈ I, there is j such that i ∈ J j ; take x = W(z, i , j ). Obviously x ∈ lim --→ S . We pretend f (x) = y. Recall that x = W(z , i , j ) and f (x) = C S (z , i ), so our objective becomes C S (z, i ) = C S (z , i ), where i , j , z , are defined by the axiom of choice. Write x 1 = C S j (y, i ) so that x = C S (x 1 , j ). We also have x = C S (x 1 , j ). This says that there is j such that j ≤ L j , j ≤ L j and g j j (x 1 ) = g j j (x 1 ). By definition of g , and rewriting x 1 , x 1 , this is C S (z, i ) = C S (z , i ), where S should be replaced by S j ; but, given the definition of S j , we may omit the index and conclude. Lemma ex6_F_prop2 y i j j': (* 15 *) inc i (Vg Jf j) -> inc y (Vg (isE S) i) -> gle rL j j' -> ex6_F_val y i j = ex6_F_val y i j'.

Lemma ex6_fct_ax: lf_axiom ex6_fct (inductive_limit ex6_F) (inductive_limit S). (* 3 *) Lemma ex6_fct_fi: injection ex6_iso. (* 23 *) Lemma ex6_fct_fs: surjection ex6_iso. (* 40 *) mma ex6_fct_bp: bijection_prop ex6_iso (inductive_limit ex6_F) (inductive_limit S). End Exercise6.

Exercise 7. « Let I be a directed set and let (E α , f βα ) be a direct system of sets relative to I. For each α ∈ I, let f α : E α → E = lim --→ E α be the canonical mapping. In each E α , let R α be the equivalence relation f α (x) = f α (y). Show that, whenever α ≤ β, the mapping f βα is compatible with the equivalence relations R α and R β . Let E α = E α /R α , and let f βα be the mapping of E α into E β induced by f βα on passing to the quotients. Show that f βα is injective and that (E α , f βα ) is a direct system of sets, and define a canonical bijection of E onto lim --→ E α . » Obviously R i is an equivalence relation on E i . Write x ≡ i y when x and y are related by R i . This is the same as C S (x, i ) = C S (y, i ). It clearly implies f j i (x) ≡ j f j i (y). This is the compatibility property.

José Grimm

Section Exercise7. Variable S : inductive_system. Definition ex7_eqv i := equivalence_associated (inl_can_fun S i). Lemma ex7_eqv_prop1 i: inc i (isI S) -> equivalence_on (ex7_eqv i) (Vg (isE S) i). (* 3 *) Lemma ex7_eqv_prop2 i: inc i (isI S) -> forall x y, (* 7 *) related (ex7_eqv i) x y <-> [/\ inc x (Vg (isE S) i), inc y (Vg (isE S) i) & class (inl_equiv S) (J x i) = class (inl_equiv S) (J y i)]. Lemma ex7_eqv_prop3 i j: gle (isr S) i j -> compatible_with_equivs (Vg (isf S) (J i j)) (ex7_eqv i)(ex7_eqv j). (* 12 *)

We define here E i the quotient and f j i , the functions on the quotients. We denote by C i (x) the class of R i , so that f j i (x) = C j ( f j i (R(x)), where R(x) is a representative of x (an element of E i whose class is x). If i = j we have f j i (x) = C i (R(x)) so that f i j is the identity function. If f j i (x) = f j i (y) then C j ( f j i (R(x))) = C j ( f j i (R(y))). This gives C S ( f j i (R(x)), j ) = C S ( f j i (R(y)), j ), then C S (R(x), i ) = C S (R(y), i ) and C i (R(x)) = C i (R(y)). This says x = y and f j i is injective.

Definition ex7_Ei i := quotient (ex7_eqv i). Definition ex7_fij ij:= fun_on_quotients (ex7_eqv (P ij)) (ex7_eqv (Q ij)) (Vg (isf S) ij).

Lemma ex7_fij_prop1 i j: gle (isr S) i j -> function_prop (ex7_fij i j) (ex7_Ei i) (ex7_Ei j). (* 8 *) Lemma ex7_fij_ev i j x: gle (isr S) i j -> inc x (ex7_Ei i) -> (* 4 *)

Vf (ex7_fij i j) x = class (ex7_eqv j) (Vf (Vg (isf S) (J i j)) (rep x)). Lemma ex7_fij_ev_bis i j x: gle (isr S) i j -> inc x (Vg (isE S) i) -> Vf (ex7_fij i j) (class (ex7_eqv i) x) = class (ex7_eqv j) (Vf (Vg (isf S) (J i j)) x). (* 12 *) Lemma ex7_fij_prop2 i: inc i (isI S) -> (* 7 *) (ex7_fij i i) = identity (ex7_Ei i). Lemma ex7_fij_prop3 i j k: gle (isr S) i j -> gle (isr S) j k -> (* 28 *) ex7_fij j k \co ex7_fij i j = ex7_fij i k. Lemma ex7_fij_prop4 i j : gle (isr S) i j -> injection (ex7_fij i j). (* 16 *)

We can define an inductive system with f j i and E i . Let's call it S . Assume x ∈ lim --→ S , so that x = C S (z, i ), where z ∈ E i ; we have z = C i (z ), where z = R(z) ∈ E i . Then x → C S (z , i ) is a canonical bijection lim --→ S → lim --→ S. Inria Definition ex7_iso := Lf ex7_fct (inductive_limit ex7_system) (inductive_limit S).

Lemma ex7_can_val_bj : (* 53 *) bijection_prop ex7_iso (inductive_limit ex7_system) (inductive_limit S).

End Exercise7.

Exercise 8. « Let (E α , f βα ) and (F α , g βα ) be two direct systems of sets, both indexed by the same directed set I. For each α ∈ I, let u α be a mapping of E α into F α such that the u α form a direct system of mappings. Let G α ⊂ E α × F α be the graph of u α . Show that (G α ) is a direct system of subsets of E α × F α and that its direct limit may be canonically identified with the graph of u = lim --→ u α .»

The first claim is easy (same proof as Exercise 3). Assume that t is an element of the graph of u. So that is i ∈ I, x ∈ E i such that x = C S (x , i ), y = C S (u i (x ), i ) and t = (x, y). This means that (x , u i (x )) ∈ G i .

Section Exercise8.

Variables S S': inductive_system. Variable (u:Set). Hypothesis same_I: (inl_same_index S S'). Hypothesis (Hu: inl_map2_compat S S' u).

José Grimm

Exercise 9. « Let I be an arbitrary preordered set, and let (E α ) α∈I be a family of sets indexed by I. For each pair of indices (α, β) such that α ≤ β, let f βα be a mapping of E α into E β , and suppose that these mappings satisfy conditions (LI I ) and (LI II ). Let G be the set which is the sum of the family E α and (with the notations of no. 5) let Räx, yä be the relation "λ(x) = α ≤ λ(y) = β and y = f βα (x)" between two elements x, y of G. Let R be the equivalence relation on G whose graph is the smallest of the graphs of equivalence relations which contain the graph of R (Chapter II, §6, Exercise 10). The set E = G/R is called the direct limit of the family E α with respect to the family of mappings ( f βα ), and we write E = lim --→ E α . When the index set I is directed, show that the definition agrees with that given in no. 5. In the general case, the restriction to E α of the canonical mapping of G into E α is called the canonical mapping of E α into E and is denoted by f α . Suppose we are given, for each α ∈ I, a mapping u α of E α into F such that u β • f βα = u α whenever α ≤ β; show that there exists a unique mapping u of E into F such that u = u α • f α for each α ∈ I. » The context will be the following: Section Exercise9.

Variables (E I r f: Set). Hypothesis (or: preorder r) (sr: substrate r = I) (fgE:fgraph E) (dE: domain E = I) (fgf: fgraph f) (df: domain f = r) (function_f: forall p, inc p r -> function_prop (Vg f p) (Vg E (P p)) (Vg E (Q p))) (compose_f: forall i j k, gle r i j -> gle r j k -> Vg f (J j k) \co Vg f (J i j) = Vg f (J i k)) (identity_f: forall i, inc i I -> Vg f (J i i) = identity (Vg E i)).

We consider a set G and two relations R and R . The first relation is proposed by Bourbaki, the second relation is the equivalence of an inductive system. Obviously, R implies R . We consider the least equivalence relation s on G such that R(x, y) implies s(x, y). Note that R is reflexive on G, but not symmetric, so that we replace the relation by "x and y are in G, R(x, y) or R(y, x)"; this does not change s. Exercise 10 of Chapter 2, implemented in the main text gives an explicit form for s (See part I of this report). In particular, R (x, y) implies s(x, y). Assume I right directed; we can consider the inductive system defined by I, r , E, f and all the axioms; it follows that R is an equivalence relation on G. In this case, s is equal to the graph of R on G. Let's consider the quotient of G by s. In the special case where I is right directed, and S is the inductive system mentioned above, this quotient is lim --→ S. In the general case, we can define the canonical function. Assume now that we have a family of functions u i : E i → F, satisfying some properties. If x = (x , i ) and y = (y , j ) then R(x, y) implies u i (x ) = u j (y ). Write this as R(x, y) =⇒ r (x, y). Note that r is an equivalence relation, so that, if s is the least equivalence that extends R, we have s(x, y) =⇒ r (x, y). Let X be an equivalence class of s, and (x , i ) an element of the class; then u i (x ) depends only of X. We denote it by u(X). This defines a function u such that that u i = u • f i . Conversely, if this holds, then u(C s (x, i )) = u i (x) whenever i ∈ I and x ∈ E i . This implies uniqueness.

Variables (u F: Set).

Hypotheses

(fgu:fgraph u) (du: domain u = I) (function_u: forall i, inc i I -> function_prop (Vg u i) (Vg E i) F) (compose_u: forall i j, gle r i j -> (Vg u j) \co Vg f (J i j) = Vg u i).

Definition ex9_map_property g:= function_prop g ex9_quo F /\ forall i, inc i I -> (Vg u i) = g \co (ex9_can_fun i).

José Grimm

Inria