Almost-disconnected morphisms

This is the neutral scheme-morphism root of Definition B.1 in arXiv:2607.28411v1. A witness for p : X ⟶ Y consists of a finite filtration of 𝒪_X; each graded piece is the pushforward of the inverse of an invertible sheaf from a closed subscheme Xᵢ ↪ X whose composite with p is an isomorphism to Y.

The definition deliberately contains no stability-condition, moduli, or quotient-presentation data. It is a MorphismProperty, so generic behavior belongs at this root and downstream stability adapters can consume it without owning it.

The paper also proves flat-base-change and composition closure (Lemma B.2). The geometric part of composition is implemented here at the common SupportData root. The full closure theorems are not yet asserted: composition still needs line-bundle pullback and the tensor--pushforward projection formula, while base change needs the arbitrary cartesian comparison g^* i_* L ≅ i'_* g'^* L and an exact scheme-module pullback API. In particular, the repository's current exact flat-pullback theorem lives below DerivedCategory/Families, which this root must not import.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.AlmostDisconnected.structureSheaf (X : Scheme) : X.Modules

The structure sheaf, regarded as an object of the scheme's module category.

Equations

• AlgebraicGeometry.AlmostDisconnected.structureSheaf X = SheafOfModules.unit X.ringCatSheaf

structure AlgebraicGeometry.AlmostDisconnected.SupportData {X Y : Scheme} (p : X ⟶ Y) : Type (u + 1)

The geometric support carried by one graded piece of an almost-disconnected witness.

This is the common root of the graded-piece hierarchy: it owns only the closed subscheme and its identification with the base. Line bundles and quotient comparisons are attached by GradedPieceData, so composition of supports does not depend on any module-theoretic choices.

• support : Scheme

  The closed support of the graded piece.

• inclusion : self.support ⟶ X

  Its inclusion into the source.

• inclusion_isClosedImmersion : IsClosedImmersion self.inclusion

  The support is a closed subscheme of the source.

• baseIso : self.support ≅ Y

  The support identifies with the target.

• baseIso_hom : self.baseIso.hom = CategoryTheory.CategoryStruct.comp self.inclusion p

  The chosen identification is induced by the original morphism.

instance AlgebraicGeometry.AlmostDisconnected.SupportData.instIsClosedImmersionInclusion {X Y : Scheme} {p : X ⟶ Y} (D : SupportData p) : IsClosedImmersion D.inclusion

Install the closed-immersion certificate carried by a support datum.

def AlgebraicGeometry.AlmostDisconnected.SupportData.identity (X : Scheme) : SupportData (CategoryTheory.CategoryStruct.id X)

The tautological support datum for an identity morphism.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.AlmostDisconnected.SupportData.comp {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (D : SupportData p) (E : SupportData q) : SupportData (CategoryTheory.CategoryStruct.comp p q)

Compose two support data.

If S ⟶ X identifies S with Y, and T ⟶ Y identifies T with Z, then T embeds in X through T ⟶ Y ⟶ S ⟶ X and identifies with Z. This is the geometric part of the composition proof in Lemma B.2, independent of the later tensor and projection- formula comparison for the associated line bundles.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.AlmostDisconnected.SupportData.comp_support {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (D : SupportData p) (E : SupportData q) : (D.comp E).support = E.support

The first projection law for the geometric part of Lemma B.2.

@[simp]

theorem AlgebraicGeometry.AlmostDisconnected.SupportData.comp_inclusion {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (D : SupportData p) (E : SupportData q) : (D.comp E).inclusion = CategoryTheory.CategoryStruct.comp E.inclusion (CategoryTheory.CategoryStruct.comp D.baseIso.inv D.inclusion)

The factorization used later to compare composite pushforwards.

@[simp]

theorem AlgebraicGeometry.AlmostDisconnected.SupportData.comp_baseIso {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (D : SupportData p) (E : SupportData q) : (D.comp E).baseIso = E.baseIso

The final-base projection law for the geometric part of Lemma B.2.

structure AlgebraicGeometry.AlmostDisconnected.GradedPieceData {X Y : Scheme} (p : X ⟶ Y) (Q : X.Modules) extends AlgebraicGeometry.AlmostDisconnected.SupportData p : Type (u + 1)

One graded piece of an almost-disconnected witness.

The geometric support extends SupportData; the module-theoretic child adds the line bundle and the comparison with the relevant quotient. Keeping this inheritance explicit prevents future consumers from growing parallel support records with subtly different composition laws.

• support : Scheme
• inclusion : self.support ⟶ X
• inclusion_isClosedImmersion : IsClosedImmersion self.inclusion
• baseIso : self.support ≅ Y
• baseIso_hom : self.baseIso.hom = CategoryTheory.CategoryStruct.comp self.inclusion p
• lineBundle : Scheme.Modules.LineBundleData self.support

  The invertible sheaf whose inverse presents the quotient.

• gradedIso : Q ≅ (Scheme.Modules.pushforward self.inclusion).obj self.lineBundle.inverse

  The quotient is the pushforward of the inverse line bundle from its support.

structure AlgebraicGeometry.AlmostDisconnected.Witness {X Y : Scheme} (p : X ⟶ Y) : Type (u + 1)

Explicit data witnessing that a scheme morphism is almost disconnected.

This is Definition B.1 of arXiv:2607.28411v1, with equalities replaced by chosen isomorphisms. The line bundle stores both Lᵢ and its tensor inverse, so gradedIso can name Lᵢ⁻¹ without making a noncanonical choice.

• filtration : CategoryTheory.FiniteFiltration X.Modules (structureSheaf X)

  The filtration 0 = F₀ ⊂ ⋯ ⊂ Fₘ = 𝒪_X.

• piece (i : Fin self.filtration.length) : GradedPieceData p (self.filtration.graded i)

  The geometrically rooted data attached to each graded quotient.

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.support {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : Scheme

The closed support Xᵢ of a witness's ith graded piece.

Equations

• W.support i = (W.piece i).support

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.inclusion {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : W.support i ⟶ X

The inclusion ιᵢ : Xᵢ ⟶ X.

Equations

• W.inclusion i = (W.piece i).inclusion

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.inclusion_isClosedImmersion {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : IsClosedImmersion (W.inclusion i)

The closed-immersion certificate for the ith support.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.baseIso {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : W.support i ≅ Y

The identification of the ith support with the base.

Equations

• W.baseIso i = (W.piece i).baseIso

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.baseIso_hom {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : (W.baseIso i).hom = CategoryTheory.CategoryStruct.comp (W.inclusion i) p

The support identification is induced by the original morphism.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.lineBundle {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : Scheme.Modules.LineBundleData (W.support i)

The line bundle attached to the ith support.

Equations

• W.lineBundle i = (W.piece i).lineBundle

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.gradedIso {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : W.filtration.graded i ≅ (Scheme.Modules.pushforward (W.inclusion i)).obj (W.lineBundle i).inverse

The ith quotient is the pushforward of the inverse line bundle from its support.

Equations

• W.gradedIso i = (W.piece i).gradedIso

instance AlgebraicGeometry.AlmostDisconnected.Witness.instIsClosedImmersionInclusion {X Y : Scheme} {p : X ⟶ Y} (W : Witness p) (i : Fin W.filtration.length) : IsClosedImmersion (W.inclusion i)

Install the closed-immersion certificate carried by a witness.

@[reducible, inline]

abbrev AlgebraicGeometry.AlmostDisconnected.Witness.CompositionIndex {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (W : Witness p) (V : Witness q) : Type

The outer-major pair indexing the graded pieces in a composite witness.

Equations

• W.CompositionIndex V = (Fin W.filtration.length × Fin V.filtration.length)

def AlgebraicGeometry.AlmostDisconnected.Witness.compositionIndexEquiv {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (W : Witness p) (V : Witness q) : W.CompositionIndex V ≃ Fin (W.filtration.length * V.filtration.length)

Outer-major pairs are canonically the finite interval of product length.

Equations

• W.compositionIndexEquiv V = finProdFinEquiv

def AlgebraicGeometry.AlmostDisconnected.Witness.compositionSupportData {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (W : Witness p) (V : Witness q) (ij : W.CompositionIndex V) : SupportData (CategoryTheory.CategoryStruct.comp p q)

The composite geometric support attached to an outer/inner pair of graded pieces.

Equations

• W.compositionSupportData V ij = (W.piece ij.1).comp (V.piece ij.2).toSupportData

@[simp]

theorem AlgebraicGeometry.AlmostDisconnected.Witness.compositionSupportData_support {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (W : Witness p) (V : Witness q) (ij : W.CompositionIndex V) : (W.compositionSupportData V ij).support = V.support ij.2

Rewrite a product index to the inner support used by the eventual line-bundle lookup.

@[simp]

theorem AlgebraicGeometry.AlmostDisconnected.Witness.compositionSupportData_inclusion {X Y Z : Scheme} {p : X ⟶ Y} {q : Y ⟶ Z} (W : Witness p) (V : Witness q) (ij : W.CompositionIndex V) : (W.compositionSupportData V ij).inclusion = CategoryTheory.CategoryStruct.comp (V.inclusion ij.2) (CategoryTheory.CategoryStruct.comp (W.baseIso ij.1).inv (W.inclusion ij.1))

The composite pair's inclusion is the root SupportData.comp inclusion.

noncomputable def AlgebraicGeometry.AlmostDisconnected.identityWitness (X : Scheme) : Witness (CategoryTheory.CategoryStruct.id X)

Explicit almost-disconnected data for the identity morphism.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.IsAlmostDisconnected : CategoryTheory.MorphismProperty Scheme

The morphism property of admitting the filtration in Definition B.1 of arXiv:2607.28411v1.

Equations

• AlgebraicGeometry.IsAlmostDisconnected p = Nonempty (AlgebraicGeometry.AlmostDisconnected.Witness p)

theorem AlgebraicGeometry.IsAlmostDisconnected.id (X : Scheme) : IsAlmostDisconnected (CategoryTheory.CategoryStruct.id X)

The identity morphism is almost disconnected.

instance AlgebraicGeometry.IsAlmostDisconnected.instContainsIdentitiesScheme : IsAlmostDisconnected.ContainsIdentities