The filtration property

Definition 3.19 of arXiv:2607.28411v1 describes a filtration of the diagonal kernel on X ×_Y X by graph sheaves. Lemma B.4 gives the neutral geometric characterization used here: for separated f : X ⟶ Y, the first projection is almost disconnected and every closed support occurring in its witness also maps isomorphically to X under the second projection.

This formulation is intentionally an independent consumer of IsAlmostDisconnected; graph sheaves and stability conditions do not enter the morphism root. The two support isomorphisms canonically recover the relative automorphisms appearing in Definition 3.19.

Lemma B.5 (flat-base-change stability) will follow from Lemma B.2 plus the standard comparison between base change of the relative self-product and the self-product after base change. It is not asserted until the missing neutral flat-pullback/pushforward comparison documented in AlmostDisconnected.lean exists.

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

Data for the filtration property, in the equivalent form of Lemma B.4 of arXiv:2607.28411v1.

• isSeparated : IsSeparated f

  Definition 3.19 assumes that f is separated.

• kernel : AlmostDisconnected.Witness (CategoryTheory.Limits.pullback.fst f f)

  The first projection X ×_Y X ⟶ X is almost disconnected.

• secondProjectionIso (i : Fin self.kernel.filtration.length) : self.kernel.support i ≅ X

  Every support in the kernel filtration maps isomorphically to X by p₂.

• secondProjectionIso_hom (i : Fin self.kernel.filtration.length) : (self.secondProjectionIso i).hom = CategoryTheory.CategoryStruct.comp (self.kernel.inclusion i) (CategoryTheory.Limits.pullback.snd f f)

  The second support isomorphism is induced by the second projection.

noncomputable def AlgebraicGeometry.FiltrationProperty.Witness.automorphism {X Y : Scheme} {f : X ⟶ Y} (W : Witness f) (i : Fin W.kernel.filtration.length) : X ≅ X

The relative automorphism of X recovered from the two support isomorphisms in Lemma B.4.

Equations

• W.automorphism i = (W.kernel.baseIso i).symm ≪≫ W.secondProjectionIso i

theorem AlgebraicGeometry.FiltrationProperty.Witness.automorphism_hom_over {X Y : Scheme} {f : X ⟶ Y} (W : Witness f) (i : Fin W.kernel.filtration.length) : CategoryTheory.CategoryStruct.comp (W.automorphism i).hom f = f

The recovered automorphism is a morphism over Y.

theorem AlgebraicGeometry.FiltrationProperty.Witness.automorphism_inv_over {X Y : Scheme} {f : X ⟶ Y} (W : Witness f) (i : Fin W.kernel.filtration.length) : CategoryTheory.CategoryStruct.comp (W.automorphism i).inv f = f

The inverse of the recovered automorphism is also a morphism over Y.

noncomputable def AlgebraicGeometry.FiltrationProperty.Witness.overAutomorphism {X Y : Scheme} {f : X ⟶ Y} (W : Witness f) (i : Fin W.kernel.filtration.length) : CategoryTheory.Over.mk f ≅ CategoryTheory.Over.mk f

The automorphism of X regarded intrinsically as an automorphism of the object X ⟶ Y in the over-category.

Equations

• W.overAutomorphism i = { hom := CategoryTheory.Over.homMk (W.automorphism i).hom ⋯, inv := CategoryTheory.Over.homMk (W.automorphism i).inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

def AlgebraicGeometry.HasFiltrationProperty : CategoryTheory.MorphismProperty Scheme

The filtration property of Definition 3.19, represented by the equivalent scheme-theoretic criterion of Lemma B.4 of arXiv:2607.28411v1.

Equations

• AlgebraicGeometry.HasFiltrationProperty f = Nonempty (AlgebraicGeometry.FiltrationProperty.Witness f)