Scheme realizations of weak-stability family probes

The neutral scheme-indexed triangulated family lives under AlgebraicGeometry/DerivedCategory/Families/. This file adds only the geometric realizations of weak-stability topological probes on the underlying Zariski space of an actual scheme. The declarations keep the namespace of the probe structures they extend so that dot notation such as ChargeProbe.ofScheme resolves; the file lives with the scheme because that is the object it is about.

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.ChargeProbe.ofScheme (X : AlgebraicGeometry.Scheme) {A : Type v} (value : ↥X → A) : ChargeProbe A

A charge probe on the underlying Zariski space of an actual scheme.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.ChargeProbe.ofScheme X value = { Point := ↥X, topology := inferInstance, value := value }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Families.ChargeProbe.ofScheme_isLocallyConstant_iff (X : AlgebraicGeometry.Scheme) {A : Type v} (value : ↥X → A) : (ofScheme X value).IsLocallyConstant ↔ _root_.IsLocallyConstant value

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.OpenLocusProbe.ofScheme (X : AlgebraicGeometry.Scheme) (locus : Set ↥X) : OpenLocusProbe

An openness probe on the underlying Zariski space of an actual scheme.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.Families.OpenLocusProbe.ofScheme X locus = { Point := ↥X, topology := inferInstance, locus := locus }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Families.OpenLocusProbe.ofScheme_isOpen_iff (X : AlgebraicGeometry.Scheme) (locus : Set ↥X) : (ofScheme X locus).IsOpen ↔ _root_.IsOpen locus

def CategoryTheory.Triangulated.WeakStabilityCondition.Families.GenericSemistabilityProbe.ofScheme (X : AlgebraicGeometry.Scheme) (genericPoint : ↥X) (semistableLocus : Set ↥X) : GenericSemistabilityProbe

A generic-semistability probe on the underlying Zariski space of an actual scheme.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.Families.GenericSemistabilityProbe.ofScheme_isGenericallyOpen_iff (X : AlgebraicGeometry.Scheme) (genericPoint : ↥X) (semistableLocus : Set ↥X) : (ofScheme X genericPoint semistableLocus).IsGenericallyOpen ↔ genericPoint ∈ semistableLocus → ∃ (U : Set ↥X), IsOpen U ∧ genericPoint ∈ U ∧ U ⊆ semistableLocus