Pulling a local cover back along a smooth morphism

[Kol07, 34]: "the claimed isomorphism is unique, and hence the existence is a local question". The functoriality of the globalised functor BO_{n,m} is checked after pulling a local cover of the target back to the source. This module supplies that pull-back: for a local cover g : TU → T (an M-cover into the local class in the sense of [Kol07, Theorem 105], IsLocalCover) and a smooth h : T' → T along which T' carries the pull-back data of T, the fibre product W = TU ×_T T' is a local cover of T' along the second projection (an open-immersion coproduct, surjective), carries the pull-back data of TU along the first projection (smooth, and surjective when h is), and lies in the local class: BOClass along the open-immersion leg, the hypersurface of maximal contact pulled back along the smooth leg (isSmoothDivisor_comap_of_smooth, isMaximalContact_comap_of_smooth). The construction is exists_fibreTriple of Hironaka/Resolution/Algebraic/Kol07/GlobalizeDescent.lean with one leg smooth instead of an open-immersion coproduct; the triple on W is Triple.pullback along the open-immersion leg. It is used in Hironaka/Resolution/Algebraic/OrderReduction/Step3Clauses.lean.

theorem Hironaka.BO.exists_localCover_pullback {k : Type u} [Field k] [CharZero k] {n m : ℕ} {T T' TU : AlgebraicGeometry.Triple k} {h : T'.X.left ⟶ T.X.left} [AlgebraicGeometry.Smooth h] (hpb : T'.IsPullbackOf T h) {g : TU.X.left ⟶ T.X.left} (hc : AlgebraicGeometry.Triple.IsLocalCover AlgebraicGeometry.openImmersionCoprods (AlgebraicGeometry.Triple.BOClass n m) (localClass n m) T TU g) (hT' : AlgebraicGeometry.Triple.BOClass n m T') : ∃ (W : AlgebraicGeometry.Triple k) (h' : W.X.left ⟶ TU.X.left) (g' : W.X.left ⟶ T'.X.left), CategoryTheory.IsPullback h' g' g h ∧ W.IsPullbackOf TU h' ∧ AlgebraicGeometry.Triple.IsLocalCover AlgebraicGeometry.openImmersionCoprods (AlgebraicGeometry.Triple.BOClass n m) (localClass n m) T' W g' ∧ AlgebraicGeometry.Smooth h' ∧ (Function.Surjective ⇑h → Function.Surjective ⇑h')

The pull-back of a local cover along a smooth morphism carrying pull-back data: for hc : IsLocalCover … T TU g and h : T'.X.left ⟶ T.X.left smooth with T'.IsPullbackOf T h, the fibre product W = TU ×_T T' is a local cover of T' along the projection g' and carries the pull-back data of TU along the smooth projection h', which is surjective when h is.