The meet loci and the disjoining centers: lattice facts

meetLocus G m is the closed set of points on at least m members of the finite family G (Kollár's "subset where m of the E_i intersect" [Kol07, 72]), a finite union of finite intersections of supports; disjoinCenter G m = ∏_{|s| = m} ∑_{i ∈ s} G_i is the ideal sheaf of that union with the natural scheme structure on each m-fold intersection. This module proves the lattice-level facts about them, which need no smoothness or snc hypothesis:

• membership in the meet locus (mem_meetLocus_iff) and its antitonicity in m;
• DivisorFamily.singularLocus, the locus where two components meet, is the meet locus at multiplicity 2 (sing_eq_meetLocus_two);
• the support of the center is the meet locus (support_disjoinCenter): the support of a product is the union of the supports (support_finset_prod, Hironaka/Resolution/Algebraic/Snc/DictionaryBoundary.lean), the support of a sum the intersection;
• the loci and the centers commute with inverse images along any morphism (meetLocus_comap, disjoinCenter_comap): the inverse image ideal sheaf is multiplicative and commutes with sums (comap_finset_prod, Hironaka/Resolution/Algebraic/Tuning/Transform.lean), and supports pull back to preimages; this is the content of Kollár's remark that the Z_t are defined from E alone, on which the functoriality of the construction rests;
• the disjoining sequence has k − 1 steps (length_disjoinSeq).

theorem TopologicalSpace.Closeds.mem_finset_sup {α : Type u_1} [TopologicalSpace α] {σ : Type u_2} {f : σ → Closeds α} {s : Finset σ} {x : α} : x ∈ s.sup f ↔ ∃ i ∈ s, x ∈ f i

A point lies in a finite supremum of closed sets iff it lies in one of them.

theorem TopologicalSpace.Closeds.mem_biSup_finset {α : Type u_1} [TopologicalSpace α] {σ : Type u_2} {f : σ → Closeds α} {s : Finset σ} {x : α} : x ∈ ⨆ i ∈ s, f i ↔ ∃ i ∈ s, x ∈ f i

A point lies in a supremum of closed sets indexed by a finite set iff it lies in one of them.

theorem Hironaka.Sequence.mem_meetLocus_iff {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (m : ℕ) (x : ↥X) : x ∈ meetLocus G m ↔ ∃ (s : Finset ι), s.card = m ∧ ∀ i ∈ s, x ∈ (G i).support

x lies in the meet locus at multiplicity m iff it lies on at least m members of G.

theorem Hironaka.Sequence.meetLocus_antitone {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) : Antitone (meetLocus G)

Fewer members meet at higher multiplicity.

theorem Hironaka.Sequence.meetLocus_zero {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) : meetLocus G 0 = ⊤

The meet locus at multiplicity 0 is everything.

theorem Hironaka.Sequence.meetLocus_eq_bot_of_card_lt {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) {m : ℕ} (hm : Fintype.card ι < m) : meetLocus G m = ⊥

The meet locus is empty at a multiplicity exceeding the number of members.

theorem Hironaka.Sequence.sing_eq_meetLocus_two {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : E.singularLocus = meetLocus E.component 2

The locus DivisorFamily.singularLocus where two components meet is the meet locus at multiplicity 2; the components are disjoint iff it is empty [Kol07, 72].

theorem Hironaka.Sequence.support_disjoinCenter {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) (m : ℕ) : (disjoinCenter G m).support = meetLocus G m

The center of a disjoining step is supported on Kollár's subset Z_t [Kol07, 72].

theorem Hironaka.Sequence.meetLocus_comap {X Y : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (h : Y ⟶ X) (G : ι → X.IdealSheafData) (m : ℕ) : meetLocus (fun (i : ι) => (G i).comap h) m = (meetLocus G m).preimage ⋯

The meet loci commute with inverse images along any morphism: the loci Z_t are defined from E alone [Kol07, 72].

theorem Hironaka.Sequence.disjoinCenter_comap {X Y : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (h : Y ⟶ X) (G : ι → X.IdealSheafData) (m : ℕ) : disjoinCenter (fun (i : ι) => (G i).comap h) m = (disjoinCenter G m).comap h

The disjoining centers commute with inverse images along any morphism [Kol07, 72].

@[simp]

theorem Hironaka.Sequence.disjoinSeqAux_zero {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) : disjoinSeqAux 0 G = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

The disjoining steps: unfolding lemmas.

@[simp]

theorem Hironaka.Sequence.disjoinSeqAux_one {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (G : ι → X.IdealSheafData) : disjoinSeqAux 1 G = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

theorem Hironaka.Sequence.disjoinSeqAux_succ_succ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} [Fintype ι] (m : ℕ) (G : ι → X.IdealSheafData) : disjoinSeqAux (m + 2) G = AlgebraicGeometry.Scheme.BlowUpSequence.cons X (disjoinCenter G (m + 2)) (disjoinSeqAux (m + 1) fun (i : ι) => (G i).strictTransform (disjoinCenter G (m + 2)))

theorem Hironaka.Sequence.length_disjoinSeqAux {ι : Type u_1} [Fintype ι] (m : ℕ) {X : AlgebraicGeometry.Scheme} (G : ι → X.IdealSheafData) : (disjoinSeqAux m G).length = m - 1

The steps at multiplicities m, …, 2 number m − 1.

theorem Hironaka.Sequence.length_disjoinSeq {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : (disjoinSeq E).length = Fintype.card E.ι - 1

"We make the E_i disjoint in k − 1 steps" [Kol07, 72].