The blow-up of a center equal to the unit ideal

The facts about the empty blow-up are stated elsewhere for the center written as ⊤ (markedTransform_top_left, strictTransform_top_left, exceptionalDivisor_top, eraseEmpty_cons_top). The proof of clause (3) of [Kol07, Lemma 102] meets a center Z that is provably the unit ideal (Kollár's "Z_{-1} = ∅") but is not written as ⊤, and the schemes Z.blowUp in the types prevent a rewrite. This module restates the facts for a center Z with a proof hZ : Z = ⊤ (each by substitution), together with the identification of the total transform along the trivial blow-up with the pull-back of the family with an appended empty member ([Kol07, Definition 25]: the exceptional divisor of the unit ideal is the unit ideal), and a few congruence lemmas along an equality of sequences.

theorem AlgebraicGeometry.markedTransform_of_eq_top {X : Scheme} (I : X.IdealSheafData) (m : ℕ) {Z : X.IdealSheafData} (hZ : Z = ⊤) : I.markedTransform Z m = I.comap Z.blowUpπ

The marked transform along the blow-up of a center provably equal to the unit ideal is the pull-back of the ideal (markedTransform_top_left for such a center).

theorem AlgebraicGeometry.totalTransform_of_eq_top {X : Scheme} (F : X.DivisorFamily) {Z : X.IdealSheafData} (hZ : Z = ⊤) : F.totalTransform Z = (F.append ⊤).comap Z.blowUpπ

The total transform of [Kol07, Definition 25] along the trivial blow-up: the total transform of a family along the blow-up of the unit ideal is the pull-back of the family with an appended empty member (the strict transform of each member is its pull-back, the exceptional divisor is the unit ideal).

theorem AlgebraicGeometry.cons_nil_congr {X : Scheme} {Z Z' : X.IdealSheafData} (h : Z = Z') : Scheme.BlowUpSequence.cons X Z (Scheme.BlowUpSequence.nil Z.blowUp) = Scheme.BlowUpSequence.cons X Z' (Scheme.BlowUpSequence.nil Z'.blowUp)

Two one-step sequences with equal centers are equal.

theorem AlgebraicGeometry.strictTransformSeq_last_eq_top_of_eq_nil {X : Scheme} {S : X.BlowUpSequence} (hS : S = Scheme.BlowUpSequence.nil X) {D : X.IdealSheafData} (hD : D = ⊤) : S.strictTransformSeq D (Fin.last S.length) = ⊤

The last strict transform along a sequence equal to the empty one is the ideal itself.

theorem AlgebraicGeometry.strictTransformSeq_last_eq_top_of_eq_cons_nil {X : Scheme} {S : X.BlowUpSequence} {Z : X.IdealSheafData} (hS : S = Scheme.BlowUpSequence.cons X Z (Scheme.BlowUpSequence.nil Z.blowUp)) {D : X.IdealSheafData} (hD : D.strictTransform Z = ⊤) : S.strictTransformSeq D (Fin.last S.length) = ⊤

The last strict transform along a one-step sequence is the strict transform along its center.

theorem AlgebraicGeometry.disjoint_cosupp_congr {X : Scheme} {S S' : X.BlowUpSequence} (e : S = S') (I D : X.IdealSheafData) (m : ℕ) : Disjoint {x : ↥(S.stage (Fin.last S.length)) | ↑m ≤ (S.weakTransformSeq I (Fin.last S.length)).ord x} ↑(S.strictTransformSeq D (Fin.last S.length)).support ↔ Disjoint {x : ↥(S'.stage (Fin.last S'.length)) | ↑m ≤ (S'.weakTransformSeq I (Fin.last S'.length)).ord x} ↑(S'.strictTransformSeq D (Fin.last S'.length)).support

Congruence of the disjointness of [Kol07, Lemma 102, conclusion (1)] along an equality of sequences (the index Fin.last _ depends on the sequence, so this is stated once and used in place of rw).