The induced data of an erased sequence

The empty blow-up convention [Kol07, 32] deletes the empty blow-ups of a sequence, and the second clause of functoriality for smooth morphisms [Kol07, 34.1] reindexes: this is eraseEmpty, and the last stage of S.eraseEmpty is only isomorphic to the last stage of S, through eraseEmptyLastHom (Hironaka/Scheme/BlowUpSequence/EraseEmptyConcat.lean). This module transports the induced data of [Kol07, Definition 66] along that isomorphism:

• eraseEmptyLastHom_comp_composite: the composite map of the erased sequence factors through the isomorphism and the composite map of the sequence;
• isIso_eraseEmptyLastHom: the isomorphism, as an instance;
• weakTransformSeq_eraseEmpty_last: for a smooth blow-up sequence of order m, the weak transform along the erased sequence is the inverse image of the weak transform along the sequence (the weak transform along an empty blow-up is the inverse image along its blow-up map, weakTransform_top_left, and weak transforms commute with the flat pull-back along the inverse of that map, weakTransformSeq_pullback_of_isOrderSeq);
• strictTransformSeq_eraseEmpty_last: the same for the strict transform of a divisor, with no order hypothesis (strictTransform_top_left, strictTransformSeq_pullback);
• markedTransformSeq_eraseEmpty_last (with markedTransformSeq_last_congr, markedTransformSeq_eq_idx): the marked analogue for a sequence of order ≥ m (markedTransform_top_left and markedTransformSeq_comap_pullbackStageHom_mk), and Hironaka.BMO.smooth_eraseEmptyLastHom', the smoothness of the isomorphism as a theorem.

The total transform needs more than an inverse image: the erased sequence's boundary has fewer members (the exceptional member of an empty blow-up is the unit ideal, exceptionalDivisor_top). That is the subject of Hironaka/Resolution/Algebraic/Kol07/EraseEmptyEmbedding.lean.

Transport along equalities of sequences and of stage indices

theorem Hironaka.Sequence.stageMap_last_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') : S.stageMap (Fin.last S.length) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S'.stageMap (Fin.last S'.length))

The composite map of two equal sequences, through the eqToHom of their last stages.

theorem Hironaka.Sequence.weakTransformSeq_last_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') (I : X.IdealSheafData) : S.weakTransformSeq I (Fin.last S.length) = (S'.weakTransformSeq I (Fin.last S'.length)).comap (CategoryTheory.eqToHom ⋯)

The weak transform at the last stage of two equal sequences.

theorem Hironaka.Sequence.strictTransformSeq_last_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') (J : X.IdealSheafData) : S.strictTransformSeq J (Fin.last S.length) = (S'.strictTransformSeq J (Fin.last S'.length)).comap (CategoryTheory.eqToHom ⋯)

The strict transform at the last stage of two equal sequences.

theorem Hironaka.Sequence.totalTransformSeq_last_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') (E : X.DivisorFamily) : S.totalTransformSeq E (Fin.last S.length) = (S'.totalTransformSeq E (Fin.last S'.length)).comap (CategoryTheory.eqToHom ⋯)

The total transform at the last stage of two equal sequences.

theorem Hironaka.Sequence.stageMap_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {i j : Fin (S.length + 1)} (e : i = j) : S.stageMap j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (S.stageMap i)

The stage map at two equal indices, through the eqToHom of the stages.

theorem Hironaka.Sequence.weakTransformSeq_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) {i j : Fin (S.length + 1)} (e : i = j) : S.weakTransformSeq I j = (S.weakTransformSeq I i).comap (CategoryTheory.eqToHom ⋯)

The weak transform at two equal indices, through the eqToHom of the stages.

theorem Hironaka.Sequence.strictTransformSeq_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) {i j : Fin (S.length + 1)} (e : i = j) : S.strictTransformSeq J j = (S.strictTransformSeq J i).comap (CategoryTheory.eqToHom ⋯)

The strict transform at two equal indices, through the eqToHom of the stages.

theorem Hironaka.Sequence.strictTransformSeq_pullback_last {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (J : X.IdealSheafData) : (S.pullback h).strictTransformSeq (J.comap h) (Fin.last (S.pullback h).length) = (S.strictTransformSeq J (Fin.last S.length)).comap (S.pullbackLastHom h)

strictTransformSeq_pullback at the last stage, along the last-stage lift.

theorem Hironaka.Sequence.totalTransformSeq_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) {i j : Fin (S.length + 1)} (e : i = j) : S.totalTransformSeq E j = (S.totalTransformSeq E i).comap (CategoryTheory.eqToHom ⋯)

The total transform at two equal indices, through the eqToHom of the stages.

theorem Hironaka.Sequence.pullbackLastHom_comp_composite {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) : CategoryTheory.CategoryStruct.comp (S.pullbackLastHom h) S.composite = CategoryTheory.CategoryStruct.comp (S.pullback h).composite h

The last-stage lift of h over the composite maps: h_r ≫ Π = Π' ≫ h (pullbackStageHom_stageMap at the last index).

theorem Hironaka.Sequence.composite_cons {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) : (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest).composite = CategoryTheory.CategoryStruct.comp rest.composite D.blowUpπ

The composite map of a cons (definitional).

theorem Hironaka.Sequence.composite_nil {X : AlgebraicGeometry.Scheme} : (AlgebraicGeometry.Scheme.BlowUpSequence.nil X).composite = CategoryTheory.CategoryStruct.id X

The composite map of the empty sequence (definitional).

The composite map and the isomorphism

theorem Hironaka.Sequence.composite_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') : S.composite = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) S'.composite

The composite map of the erased sequence is the composite map of the sequence through the last-stage isomorphism.

theorem Hironaka.Sequence.eraseEmptyLastHom_comp_composite {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : CategoryTheory.CategoryStruct.comp S.eraseEmptyLastHom S.composite = S.eraseEmpty.composite

theorem Hironaka.Sequence.isIso_eraseEmptyLastHom {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : CategoryTheory.IsIso S.eraseEmptyLastHom

The last stage of the erased sequence is isomorphic to the last stage of the sequence.

instance Hironaka.Sequence.instIsIsoSchemeEraseEmptyLastHom {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : CategoryTheory.IsIso S.eraseEmptyLastHom

instance Hironaka.Sequence.instIsOpenImmersionEraseEmptyLastHom {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : AlgebraicGeometry.IsOpenImmersion S.eraseEmptyLastHom

Weak and strict transforms along the erased sequence

theorem Hironaka.Sequence.comap_comap_inv {Z W : AlgebraicGeometry.Scheme} (π : Z ⟶ W) [CategoryTheory.IsIso π] (I : W.IdealSheafData) : (I.comap π).comap (CategoryTheory.inv π) = I

The inverse image along inv π of the inverse image along π is the identity.

theorem Hironaka.Sequence.comap_comap_comap_comap {A B C W Z : AlgebraicGeometry.Scheme} (I : Z.IdealSheafData) (e : A ⟶ B) (f : B ⟶ C) (g : C ⟶ W) (h : W ⟶ Z) : (((I.comap h).comap g).comap f).comap e = I.comap (CategoryTheory.CategoryStruct.comp e (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h))

Four inverse images, as one along the composite (the shape of the last-stage isomorphism of a cons on a trivial blow-up: eqToHom ≫ pullbackLastHom ≫ eraseEmptyLastHom).

theorem AlgebraicGeometry.Scheme.DivisorFamily.comap_comap_inv {Z W : Scheme} (π : Z ⟶ W) [CategoryTheory.IsIso π] (E : W.DivisorFamily) : (E.comap π).comap (CategoryTheory.inv π) = E

The same for divisor families.

theorem Hironaka.Sequence.weakTransformSeq_eraseEmpty_last {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (_hS : S.IsOrderSeq f I E m) : S.eraseEmpty.weakTransformSeq I (Fin.last S.eraseEmpty.length) = (S.weakTransformSeq I (Fin.last S.length)).comap S.eraseEmptyLastHom

For a smooth blow-up sequence of order m, the weak transform at the end of the erased sequence is the inverse image, along the last-stage isomorphism, of the weak transform at the end of the sequence [Kol07, 32 and Definition 66].

theorem Hironaka.Sequence.strictTransformSeq_eraseEmpty_last {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) : S.eraseEmpty.strictTransformSeq J (Fin.last S.eraseEmpty.length) = (S.strictTransformSeq J (Fin.last S.length)).comap S.eraseEmptyLastHom

The strict transform of a divisor at the end of the erased sequence is the inverse image, along the last-stage isomorphism, of the strict transform at the end of the sequence [Kol07, 32].

The marked transform along the erased sequence

theorem Hironaka.Sequence.markedTransformSeq_last_congr {X : AlgebraicGeometry.Scheme} {S S' : X.BlowUpSequence} (e : S = S') (I : X.IdealSheafData) (m : ℕ) : S.markedTransformSeq I m (Fin.last S.length) = (S'.markedTransformSeq I m (Fin.last S'.length)).comap (CategoryTheory.eqToHom ⋯)

The marked transform at the end of a sequence, transported along an equality of sequences (the marked analogue of weakTransformSeq_last_congr).

theorem Hironaka.Sequence.markedTransformSeq_eq_idx {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) {i j : Fin (S.length + 1)} (e : i = j) : S.markedTransformSeq I m j = (S.markedTransformSeq I m i).comap (CategoryTheory.eqToHom ⋯)

The marked transform at a stage, transported along an equality of stage indices (the marked analogue of weakTransformSeq_eq_idx).

theorem Hironaka.Sequence.markedTransformSeq_eraseEmpty_last {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (m : ℕ) (E : X.DivisorFamily) (_hS : S.IsOrderGeSeq f I m E) : S.eraseEmpty.markedTransformSeq I m (Fin.last S.eraseEmpty.length) = (S.markedTransformSeq I m (Fin.last S.length)).comap S.eraseEmptyLastHom

For a smooth blow-up sequence of order ≥ m, the marked transform at the end of the erased sequence is the inverse image, along the last-stage isomorphism, of the marked transform at the end of the sequence [Kol07, 32 and Definition 66]; the marked analogue of weakTransformSeq_eraseEmpty_last. The marked transform under an empty blow-up is the inverse image (markedTransform_top_left), and a marked transform along the pull-back by an isomorphism is the inverse image of the marked transform (markedTransformSeq_comap_pullbackStageHom_mk).

theorem Hironaka.BMO.smooth_eraseEmptyLastHom' {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : AlgebraicGeometry.Smooth S.eraseEmptyLastHom

The last-stage isomorphism of an erased sequence is smooth (an isomorphism, hence an open immersion); the form used by the marked order reduction.