Correspondences of boundary families across a map

A correspondence between two hypersurface families across a map g : B → A (the boundary correspondence of Functor/EraseEmptyBoundary.lean is the case of a diffeomorphism): an order embedding e₀ : GA.ι ↪o GB.ι such that the member e₀ k of GB is the inverse image of the member k of GA, the members of GB outside the range of e₀ are empty, and the original members are matched. It is the relation between the boundary families at the last stages of two disjoining lists related by a local analytic isomorphism, possibly with extra empty exceptional divisors (the padding by empty blow-ups; [Kol07, 34.1], [Kol07, 32]). This module proves that the relation passes to the collapsed families (collapse, the original members collapsed into one first member): the collapsed boundary of the one list is an empty extension of the inverse image of the collapsed boundary of the other (PullbackCorr.exists_isEmptyExtension_collapse) — the hypothesis of the input family's IndifferentToEmptyMembers. Used by DisjoinedNatural.lean for the independence of the shrinking open.

def Manifold.HypersurfaceFamily.PullbackCorr {A B : Type u} (g : B → A) (GA : HypersurfaceFamily A) (GB : HypersurfaceFamily B) {ι₀ : Type u} (oA : ι₀ → GA.ι) (oB : ι₀ → GB.ι) : Prop

A correspondence across a map g : B → A: an order embedding e₀ : GA.ι ↪o GB.ι matching the members through g (GB.hyp (e₀ k) = g⁻¹(GA.hyp k)), the members of GB outside its range empty, and the original members (indexed by ι₀) matched.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.HypersurfaceFamily.PullbackCorr.refl_comap {A B : Type u} (g : B → A) (GA : HypersurfaceFamily A) {ι₀ : Type u} (oA : ι₀ → GA.ι) : PullbackCorr g GA (comap g GA) oA oA

The identity correspondence between GA and its inverse image g⁻¹(GA).

theorem Manifold.HypersurfaceFamily.PullbackCorr.congr {A B : Type u} {g : B → A} {GA GA' : HypersurfaceFamily A} {GB GB' : HypersurfaceFamily B} {ι₀ : Type u} {oA : ι₀ → GA.ι} {oB : ι₀ → GB.ι} {oA' : ι₀ → GA'.ι} {oB' : ι₀ → GB'.ι} (hA : GA = GA') (hB : GB = GB') (hoA : ∀ (j : ι₀), oA j ≍ oA' j) (hoB : ∀ (j : ι₀), oB j ≍ oB' j) (h : PullbackCorr g GA GB oA oB) : PullbackCorr g GA' GB' oA' oB'

Transport along equalities of the families (heterogeneously for the original members).

theorem Manifold.HypersurfaceFamily.PullbackCorr.trans_isEmptyExtension {A B : Type u} {g : B → A} {GA : HypersurfaceFamily A} {GB GB' : HypersurfaceFamily B} {ι₀ : Type u} {oA : ι₀ → GA.ι} {oB : ι₀ → GB.ι} {oB' : ι₀ → GB'.ι} (h : PullbackCorr g GA GB oA oB) {e : GB.ι ↪o GB'.ι} (he : IsEmptyExtension e) (hoB : ∀ (j : ι₀), e (oB j) = oB' j) : PullbackCorr g GA GB' oA oB'

Composition with an empty extension (the same nonempty members plus extra empty ones) on the target side, the original members matched along it.

The collapsed families

def Manifold.HypersurfaceFamily.sumLexMapRightEmb {α : Type u_1} {γ : Type u_2} {δ : Type u_3} [LinearOrder α] [LinearOrder γ] [LinearOrder δ] (e : γ ↪o δ) : α ⊕ₗ γ ↪o α ⊕ₗ δ

The lift of an order embedding of the right summands to the lexicographic sums with a common left summand (Sum.map id e) — the index sets of the collapsed families, whose first member is the collapsed one.

Equations

• Manifold.HypersurfaceFamily.sumLexMapRightEmb e = OrderEmbedding.ofMapLEIff (fun (x : α ⊕ₗ γ) => toLex (Sum.map id (⇑e) (ofLex x))) ⋯

def Manifold.HypersurfaceFamily.notOriginalEmb {A B : Type u} {GA : HypersurfaceFamily A} {GB : HypersurfaceFamily B} (e₀ : GA.ι ↪o GB.ι) {pA : GA.ι → Prop} {pB : GB.ι → Prop} (hp : ∀ (k : GA.ι), ¬pA k → ¬pB (e₀ k)) : { k : GA.ι // ¬pA k } ↪o { k : GB.ι // ¬pB k }

An order embedding restricted to the members outside the originals.

Equations

• Manifold.HypersurfaceFamily.notOriginalEmb e₀ hp = OrderEmbedding.ofMapLEIff (fun (k : { k : GA.ι // ¬pA k }) => ⟨e₀ ↑k, ⋯⟩) ⋯

theorem Manifold.HypersurfaceFamily.PullbackCorr.exists_isEmptyExtension_collapse {A B : Type u} {g : B → A} {GA : HypersurfaceFamily A} {GB : HypersurfaceFamily B} {ι₀ : Type u} {oA : ι₀ → GA.ι} {oB : ι₀ → GB.ι} (h : PullbackCorr g GA GB oA oB) : ∃ (e : (comap g (GA.collapse fun (k : GA.ι) => k ∈ Set.range oA)).ι ↪o (GB.collapse fun (k : GB.ι) => k ∈ Set.range oB).ι), IsEmptyExtension e

The collapsed families of a correspondence: a correspondence across g with matched original members induces an empty extension of the inverse image of the collapsed family of GA into the collapsed family of GB, the collapsed members being the unions of the originals.