Disjoint unions of triples and the domain of a blow-up sequence functor

By [Kol07, Warning 38] the domain of a blow-up sequence functor must contain the disconnected schemes ∐ᵢ Uᵢ: a resolution functor on connected schemes extends to disconnected ones, a blow-up sequence functor does not, because the order of the blow-ups on different components is part of the output. This is expressed as a predicate on triples (Hironaka/Scheme/BlowUpSequence/FunctorVocabulary.lean): T.IsSigmaOf Ts ι says that the cofan ι i : (Ts i).X.left ⟶ T.X.left is a coproduct of schemes over Spec k along which the ideal and the divisor family of T restrict to those of the Ts i, and Triple.ClosedUnderSigma Dom says that the class Dom is closed under finite nonempty disjoint unions. This module proves the elementary facts about these predicates.

• isSigmaOf_single: a triple is the disjoint union of itself along the identity: the one-object cofan on an isomorphism is a colimit (Mathlib's Cofan.isColimitMkOfUnique), and comap along the identity is the identity on ideal sheaves (Mathlib) and on divisor families (DivisorFamily.comap_id, componentwise).
• isIso_sigmaDesc: a cofan is a colimit iff the induced morphism from the categorical coproduct ∐ᵢ (Ts i).X.left is an isomorphism (Mathlib's Cofan.nonempty_isColimit_iff_isIso_sigmaDesc).
• isOpenImmersion, iUnion_range, disjoint_range: the pieces are open, cover, and are pairwise disjoint. Each ι i factors as Sigma.ι _ i ≫ Sigma.desc ι, an open immersion (Mathlib's sigmaOpenCover) followed by an isomorphism; every point of ∐ is Sigma.ι _ i z for a unique ⟨i, z⟩ (Mathlib's homeomorphism sigmaMk with the disjoint union of the underlying spaces, and sigmaι_eq_iff), transported along the isomorphism.
• Closure of the classes that occur: affine underlying scheme (Mathlib's IsAffine (∐ g) for a finite family of affines, transported along the isomorphism; this is the domain of [Kol07, Proposition 37], whose proof uses that X' = ∐ Uᵢ is affine); max-ord I ≤ m (the domain of the order reduction functor of [Kol07, Theorem 68]: the order of I at a point ι i z is the order of I|_{Uᵢ} = (Ts i).I at z, since the order is invariant under open immersions); intersections of closed classes; and for marked triples the classes given by a condition on the underlying triple and the classes T.m = m of [Kol07, Theorem 69] (the marks of the pieces agree with the mark of the whole; a nonempty index type is needed here, which is why the nullary union is excluded from ClosedUnderSigma).

@[simp]

theorem AlgebraicGeometry.Scheme.DivisorFamily.comap_id {X : Scheme} (E : X.DivisorFamily) : E.comap (CategoryTheory.CategoryStruct.id X) = E

Pulling a divisor family back along the identity changes nothing.

theorem AlgebraicGeometry.Triple.isSigmaOf_single {k : Type u} [Field k] (T : Triple k) : T.IsSigmaOf (fun (x : PUnit.{u + 1}) => T) fun (x : PUnit.{u + 1}) => CategoryTheory.CategoryStruct.id T.X.left

A triple is the disjoint union of the one-member family consisting of itself, along the identity.

theorem AlgebraicGeometry.Triple.IsSigmaOf.isIso_sigmaDesc {k : Type u} [Field k] {σ : Type u} {T : Triple k} {Ts : σ → Triple k} {ι : (i : σ) → (Ts i).X.left ⟶ T.X.left} (h : T.IsSigmaOf Ts ι) : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc ι)

The canonical morphism from the coproduct scheme to a disjoint union is an isomorphism.

theorem AlgebraicGeometry.Triple.IsSigmaOf.isOpenImmersion {k : Type u} [Field k] {σ : Type u} {T : Triple k} {Ts : σ → Triple k} {ι : (i : σ) → (Ts i).X.left ⟶ T.X.left} (h : T.IsSigmaOf Ts ι) (i : σ) : IsOpenImmersion (ι i)

The pieces of a disjoint union are open subschemes.

theorem AlgebraicGeometry.Triple.IsSigmaOf.iUnion_range {k : Type u} [Field k] {σ : Type u} {T : Triple k} {Ts : σ → Triple k} {ι : (i : σ) → (Ts i).X.left ⟶ T.X.left} (h : T.IsSigmaOf Ts ι) : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ

The pieces of a disjoint union cover it.

theorem AlgebraicGeometry.Triple.IsSigmaOf.disjoint_range {k : Type u} [Field k] {σ : Type u} {T : Triple k} {Ts : σ → Triple k} {ι : (i : σ) → (Ts i).X.left ⟶ T.X.left} (h : T.IsSigmaOf Ts ι) {i j : σ} (hij : i ≠ j) : Disjoint (Set.range ⇑(ι i)) (Set.range ⇑(ι j))

Distinct pieces of a disjoint union are disjoint.

theorem AlgebraicGeometry.Triple.closedUnderSigma_isAffine {k : Type u} [Field k] : ClosedUnderSigma fun (T : Triple k) => IsAffine T.X.left

The class of triples with affine underlying scheme is closed under finite disjoint unions (the disjoint union X' = ∐ Uᵢ of the proof of [Kol07, Proposition 37] is affine).

theorem AlgebraicGeometry.Triple.closedUnderSigma_maxOrd_le {k : Type u} [Field k] (m : ℕ) : ClosedUnderSigma fun (T : Triple k) => T.I.maxOrd ≤ ↑m

The class of triples with max-ord I ≤ m, the domain of the order reduction functor of [Kol07, Theorem 68], is closed under finite disjoint unions.

theorem AlgebraicGeometry.Triple.ClosedUnderSigma.and {k : Type u} [Field k] {D₁ D₂ : Triple k → Prop} (h₁ : ClosedUnderSigma D₁) (h₂ : ClosedUnderSigma D₂) : ClosedUnderSigma fun (T : Triple k) => D₁ T ∧ D₂ T

The intersection of two classes closed under finite disjoint unions is closed.

theorem Hironaka.MarkedTriple.closedUnderSigma_of_triple {k : Type u} [Field k] {D : AlgebraicGeometry.Triple k → Prop} (h : AlgebraicGeometry.Triple.ClosedUnderSigma D) : ClosedUnderSigma fun (T : MarkedTriple k) => D T.toTriple

A class of marked triples given by a condition on the underlying triple is closed under finite disjoint unions when that condition is.

theorem Hironaka.MarkedTriple.closedUnderSigma_m_eq {k : Type u} [Field k] (m : ℕ) : ClosedUnderSigma fun (T : MarkedTriple k) => T.m = m

The class of marked triples with mark m (the domain of the marked order reduction functor of [Kol07, Theorem 69]) is closed under finite nonempty disjoint unions.

theorem Hironaka.MarkedTriple.ClosedUnderSigma.and {k : Type u} [Field k] {D₁ D₂ : MarkedTriple k → Prop} (h₁ : ClosedUnderSigma D₁) (h₂ : ClosedUnderSigma D₂) : ClosedUnderSigma fun (T : MarkedTriple k) => D₁ T ∧ D₂ T

The intersection of two classes of marked triples closed under finite disjoint unions is closed.