Heterogeneous equalities for the truncation and the concatenation of blow-up sequences

The embedded desingularization sequence (Hironaka.Resolution.Algebraic.Wlo05.Embedded) reads the absorbing stage through the truncation run.take n at its last index, whose end result is only propositionally the run's stage n, and glues the truncation to the restarted run by concat, whose end result is only propositionally the restarted run's. The facts about the loop are proved in the index form of the run's stages and at the restarted run's end. This module holds the bookkeeping that carries data across the two casts: an ideal sheaf equal to the pullback of another along eqToHom h is heterogeneously equal to it (heq_of_eq_comap_eqToHom), and heterogeneous equality is compatible with the constructions the loop uses (colon, product, the vanishing ideal of a union of supports, the image of a finite set, composition with a morphism, the strict, marked and total transforms along a concatenation). Nothing here is mathematics; every proof is subst and a rewrite. The lemmas are used by the analysis of the loop (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP6Loop, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedStep).

theorem Hironaka.Resolution.heq_of_eq_comap_eqToHom {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {a : Y.IdealSheafData} {b : Y'.IdealSheafData} (hab : a = b.comap (CategoryTheory.eqToHom h)) : a ≍ b

An ideal sheaf equal to the pull-back of another along the cast eqToHom h is heterogeneously equal to it.

theorem Hironaka.Resolution.heq_of_eq_comap_eqToHom_divisorFamily {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {E : Y.DivisorFamily} {E' : Y'.DivisorFamily} (hE : E = E'.comap (CategoryTheory.eqToHom h)) : E ≍ E'

heq_of_eq_comap_eqToHom for divisor families.

theorem Hironaka.Resolution.heq_colon {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {a b : Y.IdealSheafData} {a' b' : Y'.IdealSheafData} (ha : a ≍ a') (hb : b ≍ b') : a.colon b ≍ a'.colon b'

Heterogeneous equality is compatible with the colon.

theorem Hironaka.Resolution.heq_mul {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {a b : Y.IdealSheafData} {a' b' : Y'.IdealSheafData} (ha : a ≍ a') (hb : b ≍ b') : a * b ≍ a' * b'

Heterogeneous equality is compatible with the product.

theorem Hironaka.Resolution.heq_vanishingIdeal_biSup_support {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {ι : Type v} (A : Finset ι) {g : ι → Y.IdealSheafData} {g' : ι → Y'.IdealSheafData} (hg : ∀ (c : ι), g c ≍ g' c) : AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (⨆ c ∈ A, (g c).support) ≍ AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (⨆ c ∈ A, (g' c).support)

Heterogeneous equality is compatible with the vanishing ideal of a finite union of supports.

theorem Hironaka.Resolution.heq_finset_image {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {ι : Type v} (A : Finset ι) {g : ι → Y.IdealSheafData} {g' : ι → Y'.IdealSheafData} (hg : ∀ (c : ι), g c ≍ g' c) : Finset.image g A ≍ Finset.image g' A

Heterogeneous equality is compatible with the image of a finite set.

theorem Hironaka.Resolution.heq_comap {Y Y' Z : AlgebraicGeometry.Scheme} (h : Y = Y') {f : Y ⟶ Z} {f' : Y' ⟶ Z} (hf : f ≍ f') (I : Z.IdealSheafData) : I.comap f ≍ I.comap f'

Heterogeneous equality is compatible with the pull-back of an ideal sheaf.

theorem Hironaka.Resolution.heq_finset_prod {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {ι : Type v} (A : Finset ι) {g : ι → Y.IdealSheafData} {g' : ι → Y'.IdealSheafData} (hg : ∀ (c : ι), g c ≍ g' c) : ∏ c ∈ A, g c ≍ ∏ c ∈ A, g' c

Heterogeneous equality is compatible with a finite product.

theorem Hironaka.Resolution.heq_pi {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {α : Sort v} {f : α → Y.IdealSheafData} {g : α → Y'.IdealSheafData} (hfg : ∀ (a : α), f a ≍ g a) : f ≍ g

Pointwise heterogeneously equal families of ideal sheaves are heterogeneously equal.

theorem Hironaka.Resolution.eq_of_heq_of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {a b : Y.IdealSheafData} {a' b' : Y'.IdealSheafData} (ha : a ≍ a') (hb : b ≍ b') (hab : a' = b') : a = b

An equation of ideal sheaves transports across a cast.

theorem Hironaka.Resolution.strictTransformSeq_concat_last_heq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (D : X.IdealSheafData) : (S.concat T).strictTransformSeq D (Fin.last (S.concat T).length) ≍ T.strictTransformSeq (S.strictTransformSeq D (Fin.last S.length)) (Fin.last T.length)

The strict transform along a concatenation, heterogeneously: the iterated strict transform.

theorem Hironaka.Resolution.markedTransformSeq_concat_last_heq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) (m : ℕ) : (S.concat T).markedTransformSeq I m (Fin.last (S.concat T).length) ≍ T.markedTransformSeq (S.markedTransformSeq I m (Fin.last S.length)) m (Fin.last T.length)

The marked transform along a concatenation, heterogeneously.

theorem Hironaka.Resolution.totalTransformSeq_concat_last_heq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (E : X.DivisorFamily) : (S.concat T).totalTransformSeq E (Fin.last (S.concat T).length) ≍ T.totalTransformSeq (S.totalTransformSeq E (Fin.last S.length)) (Fin.last T.length)

The total transform along a concatenation, heterogeneously.

theorem Hironaka.Resolution.comap_composite_concat_heq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (I : X.IdealSheafData) : I.comap (S.concat T).composite ≍ (I.comap S.composite).comap T.composite

The pull-back along the composite of a concatenation, heterogeneously.