### Remove Atomic. Add AtomicWarning.md with explanation.

Created by  finegeometer  on February 20, 2022
`VJZMBX6RE7BBINBTXKXER3W2C5WYGUBGFAPFU5MB2JUQMYBUSZHAC`
##### In channels main
##### Change contents
• ###### File deletion: atomic.v
BF:BFD[2.20] → [2.28491:28523]
BF:BFD[2.28523] → [2.28524:28524]
B:BD[2.28524] → [2.28525:29271]
``From Coq Require Import PropExtensionality FunctionalExtensionality ProofIrrelevance ssreflect.``Require Export isomorphism.``Class Atomic (O : Type) := {``    Amazing : Type -> Type;``    amaze : forall {A B}, ((O -> A) -> B) <--> (A -> Amazing B);``}.``Notation "{ 'amazing' O , X }" := (Amazing (O := O) X)``    (at level 0, format "{ 'amazing' O , X }") : type_scope.``    ``#[refine]``Global Instance iUnit : Atomic unit := {``    Amazing T := T;``    amaze _ _ := {|``        Forward f t := f (fun 'tt => t);``        Backward f t := f (t tt);``    |}``}.``Proof.``    - move=> f.``        apply: functional_extensionality => x.``        suff: x = fun 'tt => x tt by move=>->.``        apply: functional_extensionality.``        by move=>[].``    - done.``Qed.``
• ###### Replacement in theories/common.v at line 3 [2.12647]
B:BD[2.12796] → [2.12796:12879]
``Require Export isomorphism atomic weil_algebras axioms basic_infinitesimal_spaces.``
[2.12796]
[2.12879]
``Require Export isomorphism weil_algebras axioms basic_infinitesimal_spaces.``
• ###### Replacement in theories/basic_infinitesimal_spaces.v at line 2 [2.13912]
B:BD[2.13964] → [2.13964:14006]
``Require Import isomorphism axioms atomic.``
[2.13964]
[2.14006]
``Require Import isomorphism axioms.``
• ###### Deletion in theories/basic_infinitesimal_spaces.v at line 80 [2.13912]
B:BD[2.15889] → [2.15889:15934]
``    Axiom atomicD : forall {n}, Atomic 'D_n.``
• ###### Deletion in theories/basic_infinitesimal_spaces.v at line 148 [2.13912]
B:BD[2.17618] → [2.17618:17666]
``    Axiom atomicΔ : forall {n}, Atomic (Δ n).``
• ###### Deletion in theories/basic_infinitesimal_spaces.v at line 394 [2.13912]
B:BD[2.26326] → [2.26326:26533]
``    Definition atomicD {n} : Atomic 'D_n := {|``        Amazing X := { amazing Spec R (Weil (nilpotent_weil n)), X };``        amaze _ _ := iso_trans (iso_exp (iso_exp nilpotent_weil_iso)) amaze;``    |}.``    ``
• ###### Deletion in theories/basic_infinitesimal_spaces.v at line 395 [2.13912]
B:BD[2.26559] → [2.26559:26614]
``Global Instance atomicD {n} : Atomic 'D_n := atomicD.``
• ###### Deletion in theories/basic_infinitesimal_spaces.v at line 415 [2.13912]
B:BD[2.27334] → [2.27334:27393]
``    Admitted.``    Definition atomicΔ {n} : Atomic (Δ n).``
• ###### Deletion in theories/basic_infinitesimal_spaces.v at line 417 [2.13912]
B:BD[2.27426] → [2.27426:27633]
``Global Instance atomicΔ {n} : Atomic (Δ n) := atomicΔ.``(* Can this be done?``#[refine]``Global Instance atomicD_union : Atomic 'D_∞ := {|``    Amazing X := _;``    amaze _ _ := _;``|}.``Admitted.``*)``
• ###### Replacement in theories/axioms.v at line 2 [2.27667]
B:BD[2.27722] → [2.27722:27759]
``Require Import weil_algebras atomic.``
[2.27722]
[2.27759]
``Require Import weil_algebras.``
• ###### Deletion in theories/axioms.v at line 24 [2.27667]
B:BD[2.28300] → [2.28300:28401]
``(* Axiom 3, from *Synthetic Differential Geometry*. *)``Axiom atomicAxiom : Atomic (Spec R (Weil W)).``
• ###### Deletion in theories/axioms.v at line 25 [2.27667]
B:BD[2.28417] → [2.28417:28490]
``Global Instance iSpec {W} : Atomic (Spec R (Weil W)) := atomicAxiom W.``
• ###### Deletion in _CoqProject at line 2 [2.29308]
B:BD[2.29332] → [2.29332:29350]
``theories/atomic.v``
• ###### File addition: AtomicWarning.md (----------)
[3.1]
``An element J of a topos is *atomic* if the functor `(–)^J` has a right adjoint, called `(–)_J`.``In other words, morphisms `B^J -> C` uniquely correspond to morphisms `B -> C_J`.``But this does *not* mean that the objects `C^(B^J)` and `(C_J)^B` are isomorphic.``They only have the same global elements.``In fact:`````text``X -> (C_J)^B``= X * B -> C_J``= (X * B)^J -> C``= X^J * B^J -> C``= X^J -> C^(B^J)``≠ X -> C^(B^J)```````This issue does not happen for exponentials, because:`````text``X -> (B^J)^A``= X * A -> B^J``= (X * A) * J -> B``= X * (A * J) -> B``= X -> B^(A * J)```````