The over-X core of the mixed-pair transition #
The mixed-pair transition (CoproductMixedTransition.lean) identifies the parts over a common
base open P of the local resolutions of two padded pieces E₁⁺ = E₁.padAlong σ₁,
E₂⁺ = E₂.padAlong σ₂ through the common admissible input T₀ on the shear's domain
N₀ = Sp(𝕊⁺.G)|W₁' (the pieces restricted to O' ⊆ V₁ ∩ V₂, padded: 𝕊⁺, 𝕋⁺) and its two
open embeddings u = ι₁⁺ ∘ ι_{W₁'}, v = ι₂⁺ ∘ ι_{W₂'} ∘ g into the two padded ambients. Its
over-X clause reduces (through the maps of the local resolutions to the closed subspaces of the
ambients, localResolutionHomOn_comp_map) to the statement of THIS module: the two read-down
maps of Sp(T₀.I|W₀) to X — along u into Sp(E₁⁺.I|W) and then pieceOverHom, along v
into Sp(E₂⁺.I|W') and then pieceOverHom — agree. The proof is the shear's morphism
identity hmor ([Kol07, Lemma 39]; the shear of exists_padded_equivalence_hom_point) conjugated
by the squares of QuotientHomSquares.lean: homOfPullbackEq along a composite is the composite
(functoriality), the inverse embedding of a padded restricted piece is carried to the inverse
embedding of the padded piece over the inclusion of the pieces, and restrictIncl ≫ ofRestrict.
Two bookkeeping lemmas open the module: the congruence of homOfPullbackEq in the function, and
the composite form of homOfPullbackEq_comp with the composite function given by name. A generic
category lemma (comp_leg_eq) does the associativity bookkeeping of one leg. Not in the sources
beyond Lemma 39; bookkeeping.
The associativity bookkeeping of one leg of the over-X identity, in any category — a map H
followed by three maps, rewritten through five identities into ρ ≫ (r₀ ≫ e₀) ≫ o₀.
homOfPullbackEq depends on the function only — two equal functions give the same morphism
(the proofs are irrelevant).
homOfPullbackEq_comp with the composite function given by name — f₂ ∘ f₁ = f₁₂ as
functions, the three pull-back identities as stated.
The ambient of a piece restricted to V' and padded along σ (named: a local notation cannot
carry the universe).
Equations
- E.padRestrictAmbient hV' hsub σ = Hironaka.Manifold.pieceAmbient 𝕜 ((E.restrictPiece hV' hsub).padAlong σ).G
Instances For
The padded inclusion of ambients Sp((E|V')⁺.G) → Sp(E⁺.G).
Equations
- E.padRestrictIncl hV' hsub σ = Hironaka.Manifold.pieceAmbientIncl ⋯
Instances For
The shear's domain N₀ = Sp((E|V')⁺.G)|W₁'.
Equations
- E.shearDomain hV' hsub σ W₁' = (E.padRestrictAmbient hV' hsub σ).restrict W₁'
Instances For
The common admissible input T₀ on the shear's domain — the padded restricted piece's ambient
triple pulled back along the inclusion of W₁'.
Equations
- E.shearInput hV' hsub σ W₁' = ((E.restrictPiece hV' hsub).padAlong σ).ambientTriple.pullback ((E.padRestrictAmbient hV' hsub σ).inclusion W₁') ⋯
Instances For
The common input T₀ is the pull-back of the first padded piece's ambient triple along
ι₁⁺ ∘ ι_{W₁'} (isPullbackOf_ambientTriple_padAlong_restrictPiece of PadRestrict.lean composed
with the restriction).
Through the shear g with its ideal identity hI, the common input T₀ is the pull-back of
the second padded piece's ambient triple along ι₂⁺ ∘ ι_{W₂'} ∘ g (the boundary families are
empty on both sides).
The two read-down maps of the common closed subspace agree (the uniqueness step of
[Kol07, Theorem 36, proof], through the automorphism of [Kol07, Lemma 39]) — Sp(T₀.I|W₀) mapped
into the first padded piece's closed subspace along ι₁⁺ ∘ ι_{W₁'} and then to X by
pieceOverHom, or into the second's along ι₂⁺ ∘ ι_{W₂'} ∘ g and then to X, is the same
morphism. The shear's hmor conjugated by the squares of QuotientHomSquares.lean.