-Algèbre
     - Topologie
     - Catégories
     - Théorie des faisceaux

Algèbre

    Ring_quotients.v : [Ring_facts,Ring_util,Ideal2]
          Anneaux quotients, et anneaux quotients commutatifs.
    Ideal2.v : [Parts4,Ideal]
           Sommes et intersection de sous-groupes. Sommes et intersections d'ideaux.
      Radicals.v : [Parts4,Singleton,Ideal]
            Définition du radical d'un ideal, et propriétés.
      Ideal3.v: [radicals, Rings_quotients,Ideal2]
            Ideaux premiers et maximaux. Caracterisation en termes d'anneau quotient.
 

Topologie

    Cribles.v :
            Définition. Crible-intersection de deux cribles. Crible 'complet'. Lemmes généraux.

    Topolo:[Parts4, Singleton, Classical_Pred_Type]
             Definition. Espace topologique.
             Topologie engendrée par une base d'ouverts, de fermes.
             Etre ouvert, fermé comme prédicat. Ouverts , fermés comme types.
             Lemmes de compatibilite, sur les unions et intersections.

    Topolo2: [Topolo]
             Adhérence, intérieurs, bords et recouvrements.
             Lemmes basiques.

    Topolo3: [Topolo4]
             Topologies séparées. Compacts.
              L'image d'un compact par une application continue est un compact. (A finir).

    Topolo4: [Topolo2]
              Continuité, en un point, sur un ensemble.
              Caracterisation par l'image inverse d'un ouvert, d'un ferme et par l'adhérence.
 

Catégories

     Catégories2:[Categories]
               Foncteurs , foncteurs contravariants.

     Equ_dependant : [Parts3]
              Egalité sur un sigma-type.
           Pour se donner une egalite 'significative' sur un sigma-type (a:A;b:(f a)), il suffit de se donner une application
               qui associe a toute preuve d'egalite pa:a=a' une application Fpa de (f a ) vers (f a'). Ainsi on peut poser
               (a:A,b:(f a))=(a':A,b':(f a')) si il existe un preuve pa de a=a' telle que Fpa(b)=b'.
 

Faisceaux

     Top_cat:[Topolo2]
               Définition de la catégorie de départ des préfaisceaux, pour un espace
                topologique X donné.
             Les objets sont les  ouverts de X et les morphismes entre deux objets U et V sont les
                 preuves (toutes egales) que U est inclus dans V.

     Sheaves:[Top_cat ; Topolo2]
              Definition des préfaisceaux d'anneaux commutatifs. Lemmes sur les restrictions.
               Données de recollement. Définition des faisceaux d'anneaux commutatifs.
            Ces notions ne peuvent etre generalisee a toute categories : on a besoin de la notion d'egalite
               sur les objets de celles-ci. Un 'Replace All' de CRING par une categorie C dont  les objets peuvent
               etre coerces vers les setoides est cependant la seule modification a faire pour obtenir les notions
               correspondantes.

     Sheaves_plus:[Sheaves]
                Juste un lemme de plus pour les faisceaux dont les objets de la catégorie d'arrivée
                peuvent être vus comme des monoides.

     Sheaves2:[Sheaves]
                Definition des germes, fibres et morphismes de préfaisceaux.
                Structure d'anneaux sur les fibres. Isomorphismes de préfaisceaux.

    Sheaves_toolkit:[Sheaves2;Sheaves_plus]
                Quelques lemmes tres généraux sur les faisceaux et restrictions. Lourds à gérer mais
                augmentent de beaucoup  la puissance de Auto.

    Sheaves3:[Sheaves2 Sheaves_plus]
                 Morphisme induit sur les fibres par un morphisme de préfaisceau.
                 Projection sur les fibres. Compatibilité entre ces deux notions.

     Prop1_1:[Sheaves4_part_one ;Sheaves4_part_two; Sheaves4_part_three; Sheaves3]
               Proposition 1.1 du Harstone : un morphisme de faisceau est un isomorphisme ssi
                 tous les morphismes induits sur les fibres le sont.

     Associated_sheaf :[Associated_sheaf_part_one; Associated_sheaf_part_two ; Associated_sheaf_part_three ;Sheaves3]
              Construction du faisceau associe selon la definition de R.Hartshorne.

      Asc.v: [asc1.v;asc2.v;asc3.v;crible.v]
              Construction du faisceau associe en utilisant la notion de crible.
              Un element de l'anneau en U du  faisceau associe au prefaisceau F est en fait la donne d'un crible sur U et
                  la donnee pour chaque element c du crible d'un element de F(c), satisfaisant a certaines hypotheses.,

Index par ordre alphabetique  :
 

Anneaux :

    -quotients : Ringquo :Rings_Quotients.v

Cribles :

    - cribles.v

 Continuité :

   - en un point, sur un ensemble : Topolo4.v

  Compacts :

     - Topolo3.v
     - image par une application continue d'un compact :Topolo3.v

Espace :

       - topologique  : et : Topolo

 Égalités dépendantes:

        - Equ_dep.v

Faisceaux :

        - d'anneaux commutatifs : CRSheaf : Sheaves
        - associe a un prefaisceau : associated_sheaf : associated_sheaf.v (formalisation a la 'hartshorne')
                                                              asc  : asc.v (formalisation a l'aide de la notion de crible)

 Fermés :

        - comme predicat : isclosed : Topolo
        - comme type : closed : Topolo
        - lemmes classiques sur les unions , intersections : Topolo

 Fibres :

        - comme anneau : Stalk : Sheaves2
        - morphisme induit sur les : Sheaves3
        - projection sur les : Sheaves3

 Foncteurs :

        - Categories2.v

Germes :

         - Sheaves2
         - lemmes basiques : Sheaves2, Sheaves_toolkit.v
 

   -premiers et caractérisation en termes d'anneau quotient:Ideal3.v
   -maximaux et caractérisation en termes d'anneau quotient: Ideal3.v
   -somme d' :Ideal2.v
   -intersection d' : Ideal2.v
   -radicaux d' :radicals.v

Morphismes :

       -de préfaisceaux : Sheaves2, 3 , et Prop1.1.v
       -induits dans les fibres d'un préfaisceau: Sheaves3.v, Prop1.1.v

Ouverts :

       - comme type : open :Topolo
       - comme predicat : isopen :Topolo
       - lemmes classiques sur les unions , intersections : Topolo

Recollement :

        - cf faisceaux : sticking_data : Sheaves.

      -Spectrum.v