Deleting a member of an ordered divisor family: E − E^j #
Kollár writes E − E^j for the divisor E = ∑_i E^i with its member E^j removed (the proof of
[Kol07, Lemma 102]: "E_S := (E − E^j)|_S"; Step 2.1 of [Kol07, 104] clears the members
E^1, E^2, … in index order). This module holds that operation on DivisorFamily:
DivisorFamily.erase E j— the family with the memberE^jdeleted, indexed by{i // i ≠ j}with the induced linear order (the boundary is an ordered set of divisors, [Kol07, Notation 64 (3)]); its members areE's (erase_component).eraseAppendSumEquiv,eraseAppendEquiv—(E − E^j) + E^jisEup to reindexing, the deleted member going to the appended last position (append_erase_component_eraseAppendEquiv_symm); hence(E − E^j) + E^jis snc whenEis (isSnc_erase_append).hasSncWith_component— a family with Definition 24's coordinates at every point has simple normal crossings with each of its own members (E^i = (z_{c(i)} = 0)).IsEraseOf F E σ j— "FisEwith the memberE^jdeleted, up to a reindexingσ", preserved by total transforms (IsEraseOf.isEraseOf_totalTransform), which is what carries "E − E^j" along a blow-up sequence; and the snc bookkeeping of the proof of Lemma 102: a centreZ ⊆ E^jwith simple normal crossings withE − E^jhas simple normal crossings withE(IsEraseOf.hasSncWith_of_le,hasSncWith_of_erase).
The family E − E^j — E with its member E^j deleted, indexed by {i // i ≠ j} with the
induced linear order (the proof of [Kol07, Lemma 102], "E_S := (E − E^j)|_S"; the order is the one
induced from the ordered set of divisors of [Kol07, Notation 64 (3)]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
(E − E^j) + E^j is E up to reindexing — the equivalence of the plain index sums, the deleted
member going to the appended position.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(E − E^j) + E^j is E up to reindexing — the equivalence of index sets, the deleted member
going to the appended last position.
Equations
- E.eraseAppendEquiv j = ofLex.trans (E.eraseAppendSumEquiv j)
Instances For
If E is snc, so is (E − E^j) + E^j (the reindexing lemma isSnc_of_equiv).
[Kol07, Definition 24 (4)] for the family's own members: a family with the snc coordinates of
Definition 24 at every point has simple normal crossings with each of its members
(E^i = (z_{c(i)} = 0)).
F is E with the member E^j deleted, up to the reindexing σ: σ is injective,
matches the members, and its range is exactly the indices other than j. E.erase j is the case
σ = Subtype.val; the relation is preserved by total transforms (the appended exceptional members
line up), which is what carries "E − E^j" along a blow-up sequence.
- injective : Function.Injective σ
σis injective. σmatches the members.The range of
σis the set of indices other thanj.
Instances For
E.erase j is E with E^j deleted, via Subtype.val.
The bookkeeping along a blow-up: if F is E with E^j deleted, then the total transform of
F is the total transform of E with the birational transform of E^j deleted — the exceptional
members line up.
The snc bookkeeping of the proof of [Kol07, Lemma 102] ([Kol07, Definition 24 (4)]): on a smooth
X over k, if F is E with E^j deleted and a centre Z ⊆ E^j has simple normal crossings
with F, then it has simple normal crossings with E — the exchange of coordinates
hasSncWith_append_of_le (through hasSncWith_iff_hasSncWith_append) applied to F + E^j, which
is E up to the reindexing.
The snc bookkeeping of the proof of [Kol07, Lemma 102]: on a smooth X over k, a centre
Z ⊆ E^j with simple normal crossings with E − E^j has simple normal crossings with E —
IsEraseOf.hasSncWith_of_le for E.erase j.