The value of a family functor at induced triples: the transport lemmas #
The transport identities for the value of a family read at the induced triple of a list
(InducedValue.lean, ChainTransportPrep.lean, ChainTransport.lean; the functoriality argument
in the proof of [Kol07, Lemma 102], the empty blow-up convention [Kol07, 32], its counterpart for
boundary members, and the second condition of [Kol07, 34.1]), restated for an arbitrary family
functor B : AnalyticFamilyFunctor ψ₀ Dom with the two naturality properties (CommutesWithLocalIsos, IndifferentToEmptyMembers), the
class proofs of the induced triples taken as hypotheses. The versions of those three modules are for
the family of one boundary member BDanFamData on the class BOClass s, whose class proofs come
from
boClass_induced; the descent of the rounds on the nonmonomial part reads the order reduction at
the nonmonomial triple of the induced triple (nonmonomialFunctor), whose class proof is the
invariant of the descent and not a closure property, hence the hypotheses.
seqOn_induced_pullback: the value at the induced triple of a pulled-back list is the value at the induced triple of the list, pulled back along the lift of the last stages and cleaned of empty blow-ups (induced_pullbackandcommutesWithLocalIsos);induced_eq_pullback_induced_eraseEmpty,isEmptyExtension_eraseEmptyIdx_induced: the induced triple of a list is the induced triple of the cleaned list pulled back alongeraseEmptyLast, up to the empty boundary members (markedTransformSeq_last_eraseEmpty,eraseEmptyIdx);seqOn_induced_eraseEmpty: hence the value at the induced triple of a list is the value at the induced triple of the cleaned list, transported (indifferentToEmptyMembers,commutesWithLocalIsos);seqOn_induced_pullback_liftRange,seqOn_induced_pullback_congr,inducedValue_rel: the forms on reading opens, and the comparison of the two appended values of one link of a chain (the heart oflinkValue_rel), forB.
The value identities are the proofs of the corresponding statements of InducedValue.lean and
ChainTransport.lean with the family replaced. The comparison of the two appended values is an
instance of the general transport of a link along a value functor (ValueTransport.lean):
inducedValue_rel is BlowUpSequence.valueTransport_rel with the naturality of the value functor
"B at the induced triple" supplied by seqOn_induced_eraseEmpty,
seqOn_induced_pullback_liftRange and seqOn_induced_pullback_congr.
A class of triples closed under pull-back along local analytic isomorphisms (the class of [Kol07, Lemma 102] has this property; here it is a hypothesis of the transport lemmas).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The induced triple of a cleaned list #
The induced triple of a list is the induced triple of the cleaned list pulled back along
eraseEmptyLast, up to the empty boundary members ([Kol07, 32] and its counterpart for boundary
members): the ideal by
markedTransformSeq_last_eraseEmpty, the boundary replaced by the pulled-back boundary of the
cleaned list (the triple form of fam_seqOn_induced_eraseEmpty).
The boundary of the induced triple is an empty extension of the pulled-back boundary of the
induced triple of the cleaned list, along eraseEmptyIdx ([Kol07, 32] and its counterpart for
boundary members).
Transport of the class proofs #
The class proof of an induced triple transports along an equality of lists (a substitution).
A class closed under pull-back contains the induced triple of a pulled-back list when it
contains the induced triple of the list (induced_pullback).
The two value identities #
The value at the induced triple of a pulled-back list is the value at the induced triple of
the list on the image, pulled back along the lift of the last stages (induced_pullback, the
functor's commutesWithLocalIsos); the functoriality argument in the proof of [Kol07, Lemma 102],
that pull-back and restriction commute. The form of fam_seqOn_induced_pullback for B.
The value at the induced triple of a list is the value at the induced triple of the cleaned
list, transported along eraseEmptyLast ([Kol07, 32] and its counterpart for boundary members;
the second condition of [Kol07, 34.1]):
induced_eq_pullback_induced_eraseEmpty, isEmptyExtension_eraseEmptyIdx_induced, the functor's
indifferentToEmptyMembers and commutesWithLocalIsos. The form of fam_seqOn_induced_eraseEmpty
for B.
The reading-open forms #
The value at the pulled-back list is the value at the list pulled back along the lift, on
the reading opens (seqOn_induced_pullback on the image open, then the compatibility of the value
to the reading open of ρ). The form of fam_seqOn_induced_pullback_liftRange for B.
Congruence of pulled-back induced values along equal lists (a substitution). The form of
fam_seqOn_induced_pullback_congr for B.
The comparison of the two appended values #
The comparison of the two appended values (the heart of the chain transport, the form of
linkValue_rel for B): for lists L₂ on N and L₁ on M whose cleaned forms agree after
pulling L₁ back along hW, the value at the induced triple of L₂ on the reading open of ρ'
and the value at the induced triple of L₁ on the reading open of ρ, both pulled back to the
common cleaned last stage of the restricted lists and cleaned, agree. Both are the value at the
induced triple of the common cleaned list: the general valueTransport_rel with the naturality of
the value functor seqOn_induced_eraseEmpty, seqOn_induced_pullback_liftRange (on the side of
L₁) and seqOn_induced_pullback_congr (the substitution along hrel). The class proofs: of the
induced triples of L₁, L₂ and of the cleaned L₂ (hypotheses), the others by the closure of the
class under pull-back (hDom) and along the equality of the cleaned lists.