Deleting empty blow-ups through a concatenation

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] compares two sequences up to that deletion. Here eraseEmpty deletes an empty blow-up by pulling the tail back along the inverse of its blow-up map (an isomorphism), so the last stage of the erased sequence is only isomorphic to the last stage of the sequence: eraseEmptyLastHom S : S.eraseEmpty.last ⟶ S.last is that isomorphism (the composite of the last-stage lifts of the inverses), defined by recursion. With it:

• eraseEmpty_concat: deleting the empty blow-ups of S.concat T is deleting them in S, then in T transported along eraseEmptyLastHom S; this is what the functoriality of a sequence assembled from rounds by concatenation needs;
• eraseEmpty_eq_nil: a sequence all of whose centers are empty erases to the empty sequence (the case of a pulled-back sequence whose ideal has order below the mark everywhere);
• eraseEmpty_concat_eraseEmpty: deleting the empty blow-ups of a concatenation whose second piece has already been cleaned is deleting them from the concatenation itself.

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.eraseEmptyLastHom {X : Scheme} (S : X.BlowUpSequence) : S.eraseEmpty.last ⟶ S.last

The isomorphism between the last stage of the erased sequence and the last stage of the sequence: on a trivial blow-up (D = ⊤) the last-stage lift of inv (D.blowUpπ), composed with the isomorphism for the tail; on a nontrivial one the isomorphism for the tail.

Equations

• One or more equations did not get rendered due to their size.
• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝).eraseEmptyLastHom = CategoryTheory.CategoryStruct.id x✝

theorem AlgebraicGeometry.eraseEmptyLastHom_nil {X : Scheme} : (Scheme.BlowUpSequence.nil X).eraseEmptyLastHom = CategoryTheory.CategoryStruct.id X

theorem AlgebraicGeometry.eraseEmptyLastHom_cons_of_eq_top {X : Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (h : D = ⊤) [CategoryTheory.IsIso D.blowUpπ] : (Scheme.BlowUpSequence.cons X D rest).eraseEmptyLastHom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (rest.eraseEmpty.pullbackLastHom (CategoryTheory.inv D.blowUpπ)) rest.eraseEmptyLastHom)

theorem AlgebraicGeometry.eraseEmptyLastHom_cons_of_ne_top {X : Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (h : ¬D = ⊤) : (Scheme.BlowUpSequence.cons X D rest).eraseEmptyLastHom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) rest.eraseEmptyLastHom

theorem AlgebraicGeometry.concat_pullback_eqToHom {X : Scheme} {S S' : X.BlowUpSequence} (e : S = S') (R : S'.last.BlowUpSequence) : S.concat (R.pullback (CategoryTheory.eqToHom ⋯)) = S'.concat R

Transport of the second argument of a concatenation along an equality of first arguments: the eqToHom of the last-stage identification is absorbed.

theorem AlgebraicGeometry.eraseEmpty_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) : (S.concat T).eraseEmpty = S.eraseEmpty.concat (T.eraseEmpty.pullback S.eraseEmptyLastHom)

Deleting the empty blow-ups of a concatenation is deleting them in the first sequence, then in the second transported along the last-stage isomorphism of the first [Kol07, 32].

theorem AlgebraicGeometry.eraseEmpty_eq_nil {X : Scheme} (S : X.BlowUpSequence) : (∀ (i : Fin S.length), S.center i = ⊤) → S.eraseEmpty = Scheme.BlowUpSequence.nil X

A sequence all of whose centers are empty erases to the empty sequence [Kol07, 32].

theorem AlgebraicGeometry.eraseEmpty_concat_eraseEmpty {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) : (S.concat T.eraseEmpty).eraseEmpty = (S.concat T).eraseEmpty

Deleting the empty blow-ups of a concatenation whose second piece has already been cleaned is deleting them from the concatenation itself (eraseEmpty_concat twice and eraseEmpty_eraseEmpty).