f97fa41e608c — Benedikt Fluhr <http://bfluhr.com> 7 years ago
Better Exposition of Proofs
3 files changed, 35 insertions(+), 29 deletions(-)

M 00_10_someEquivalences.md
M 00_11_negEnhJoinTrees.md
M 00_12_EqualityOfInterlDist.md
M 00_10_someEquivalences.md +1 -1
@@ 139,7 139,7 @@ Now that both
 are bijective, we also have that
 $\Lambda(j)$ is bijective.
 But $\Lambda(j)$ is just
-$(\eta^{\pi^2} \circ \mathcal{C} \circ \mathcal{E})_{f U}$
+$(\eta^{\pi^2} \circ \mathcal{C} \circ \mathcal{E})_{f ~ U}$
 and this implies the claim.
 Now let $g \colon Y \rightarrow \R$ be another continuous function.

M 00_11_negEnhJoinTrees.md +6 -2
@@ 58,10 58,14 @@ and
 And this defines the negative persistence-enhancement.
 (Again a bit of a cheat.)
-Now we observe that $\mathcal{R}$ is a $1$-homomorphism from
-$\mathbf{D}$ to $\mathbf{D}$ and that
+We note that we have the following
+(@pi2hom) **Lemma.**
+The endofunctor $\mathcal{R}$ is a $1$-homomorphism from
+$\mathbf{D}$ to $\mathbf{D}$ and
 $\pi \colon \id \Rightarrow \mathcal{R}$ is a
 In particular $\mathcal{S}$ and $\mathcal{R} \circ \tilde{\mathcal{E}}$
 form a negative persistence-enhancement of join trees.
 (This does not yield any new results about join trees,

M 00_12_EqualityOfInterlDist.md +28 -26
@@ 35,8 35,10 @@ is an isomorphism of precosheaves.
 Now $\mathbf{C}$ is closed under isomorphisms and thus also
 $\mathcal{C} \mathcal{R} \mathcal{E} f$ lies in $\mathbf{C}$.
 Now we consider the case of $r$ not necessarily being $0$.
-We note that for any continuous function
-$g \colon Y \rightarrow (-\infty, \infty]$ and
+To this end let $g \colon Y \rightarrow (-\infty, \infty]$
+be a continuous function,
+possibly an object of $\mathbf{D}$.
+We note that for any
 $r \in (-\infty, \infty]$ we have
 $r + g = \mathcal{S}((\infty, -r)) (g)$
 by definition of $\mathcal{S}$.

@@ 48,16 50,14 @@ and not just $\mathbf{D}$.
 With $\mathbf{D}$ being invariant under these endofunctors,
 lemma @imgC follows from the following
-* **Lemma.**
-For all $(a, b) \in -D$ we have
-$\mathcal{C} \circ \mathcal{S}((a, b)) =
- \mathcal{S}'((a, b)) \circ \mathcal{C}$.
+(@CSendoCompat) **Lemma.**
+For all $\mathbf{a} \in -D$ we have
+$(\mathcal{C} \circ \mathcal{S}(\mathbf{a}))_g =
+ (\mathcal{S}'(\mathbf{a}) \circ \mathcal{C})_g$.
 * *Proof.*
-Let $f \colon X \rightarrow \R$ be a continuous function
-(not necessarily a Reeb or epigraph) and $(a, b) \in -D$.
-Then we have
-$\Delta \circ \mathcal{S}((a, b))(f) = S^{(-b, -b)} \circ \Delta \circ f$
+For $(a, b) \in -D$ we have
+$\Delta \circ \mathcal{S}((a, b))(g) = S^{(-b, -b)} \circ \Delta \circ g$
 and this implies the claim.
 Next we show that $\mathcal{C}$ is compatible with the natural

@@ 93,10 93,10 @@ and let
  (p, t) \mapsto (p, t - a + b)$,
 $(\overline{\mathcal{S}}(\mathbf{a} \preceq \mathbf{b}) \circ
-  \pi^2_* \circ \mathcal{C} \circ \mathcal{E})_{f [-\infty, r)} = \Lambda(i)$
+  \pi^2_* \circ \mathcal{C} \circ \mathcal{E})_{f ~ [-\infty, r)} = \Lambda(i)$
 $(\pi^2_* \circ \mathcal{C} \circ \mathcal{S}(\mathbf{a} \preceq \mathbf{b})
-  \circ \mathcal{E})_{f [-\infty, r)} = \Lambda(\tau)$.
+  \circ \mathcal{E})_{f ~ [-\infty, r)} = \Lambda(\tau)$.
 Now let $(p, t) \in \epi f \cap X \times [-\infty, r + a)$,
 then $\{p\} \times [t, t - a + b]$ is contained in
 $\epi f \cap X \times [-\infty, r + b)$.

@@ 115,11 115,16 @@ We have
 This follows from $\pi^2_*$ being a $1$-homomorphism and
 being full and faithful on $\mathbf{C}$.
-Now $\pi$ is a $2$-homomorphism and $\mathcal{C}$ is compatible
-with the shifts or endomorphisms from the smoothing functors,
-hence also the composition $\mathcal{C} \circ \pi$
-is compatible with the endomorphisms from the smoothing functors.
-From this and the previous corollary we get the commutative diagram
+* **Corollary.**
+We have
+$(\mathcal{S}'(\mathbf{a} \preceq \mathbf{b}) \circ
+  \mathcal{C} \circ \mathcal{R} \circ \mathcal{E})_f =
+ (\mathcal{C} \circ \mathcal{S}(\mathbf{a} \preceq \mathbf{b})
+  \circ \mathcal{R} \circ \mathcal{E})_f$.
+* *Proof.*
+By the lemmata @pi2hom and @CSendoCompat and the previous corollary
+we have the commutative diagram
     \mathcal{S}'(\mathbf{a}) \mathcal{C} \mathcal{E} f

@@ 152,18 157,15 @@ and thus the naturality of $\mathcal{S}'
 implies that
 $(\mathcal{C} \circ \mathcal{S}(\mathbf{a} \preceq \mathbf{b})
   \circ \mathcal{R} \circ \mathcal{E})_f =
- (\mathcal{S}'(\mathbf{a} \circ \mathcal{C} \preceq \mathbf{b})
+ (\mathcal{S}'(\mathbf{a} \preceq \mathbf{b}) \circ \mathcal{C}
   \circ \mathcal{R} \circ \mathcal{E})_f$.
-So we finally have the
-* **Lemma.**
+Eventually the previous two corollaries and lemma @CSendoCompat imply the
+* **Proposition.**
 The functor $\mathcal{C}$ is a $1$-homomorphism from
 $\mathbf{D}$ to $\mathbf{C}$.
-* *Remark.*
-A posteriori also $\mathcal{C} \circ \pi$ is a
 Now let $g \colon Y \rightarrow \R$ be another bounded constructible
 Then we have the following

@@ 178,7 180,7 @@ with respect to $\mathcal{S}'$.
 * *Proof.*
 We observe that all join trees of bounded constructible $\R$-spaces
 lie in a $-D$-subcategory of $\mathbf{D}$.
-By the previous lemma $\mathcal{C}$ yields a $1$-homomorphism
+By the previous proposition $\mathcal{C}$ yields a $1$-homomorphism
 from this $-D$-category to $\mathbf{C}$.
 Moreover corollary @ReebFullFaithf implies that
 $\mathcal{C}$ is full and faithful on this category

@@ 192,7 194,7 @@ Now by lemma @CpiEIso these are isomorph
 $\mathcal{C} \mathcal{E} g$
 and this implies the claim.
-Now we can finally proof theorem @interEq
+Now we can finally proof theorem @interEq.
 To this end let
 $f \colon X \rightarrow \R$ and $g \colon Y \rightarrow \R$
 be continuous maps with $X$ and $Y$ smooth and compact manifolds.