def AlgebraicEquivalence.CartierDivisorGroup (X : AlgebraicGeometry.Scheme) : Type u

A simplified placeholder model for the Cartier divisor group on X: integer-valued functions on the underlying points.

@[implicit_reducible]

instance AlgebraicEquivalence.CartierDivisorGroup.instAddCommGroup (X : AlgebraicGeometry.Scheme) : AddCommGroup (CartierDivisorGroup X)

Abelian group structure on CartierDivisorGroup, pointwise.

def AlgebraicEquivalence.CartierDivisorGroup.pullback {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : CartierDivisorGroup Y →+ CartierDivisorGroup X

Pullback of (model) Cartier divisors along a morphism f : X → Y: compose with the underlying continuous map.

def AlgebraicEquivalence.CartierDivisorGroup.isPrincipal {X : AlgebraicGeometry.Scheme} (_D : CartierDivisorGroup X) : Prop

Placeholder predicate: a (model) divisor is principal. Always True in this skeleton.

theorem AlgebraicEquivalence.CartierDivisorGroup.pullback_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (D : CartierDivisorGroup Z) : (pullback (CategoryTheory.CategoryStruct.comp f g)) D = (pullback f) ((pullback g) D)

Functoriality of divisor pullback: (f ∘ g)^* = f^* ∘ g^*.

theorem AlgebraicEquivalence.CartierDivisorGroup.pullback_id {X : AlgebraicGeometry.Scheme} (D : CartierDivisorGroup X) : (pullback (CategoryTheory.CategoryStruct.id X)) D = D

Pullback along the identity is the identity.

structure AlgebraicEquivalence.SPoint {S X : AlgebraicGeometry.Scheme} (p : X ⟶ S) : Type u

An S-point of a scheme X over S: a section of the structure morphism p : X → S.

• morphism : S ⟶ X
• isSection : CategoryTheory.CategoryStruct.comp self.morphism p = CategoryTheory.CategoryStruct.id S

structure AlgebraicEquivalence.ConnectedVariety (S : AlgebraicGeometry.Scheme) : Type (u + 1)

A connected variety over S: an integral, topologically connected scheme equipped with a structure morphism to S. Used to parametrize algebraic families.

• toScheme : AlgebraicGeometry.Scheme
• structureMorphism : self.toScheme ⟶ S
• isIntegral : AlgebraicGeometry.IsIntegral self.toScheme
• isConnected : ConnectedSpace ↥self.toScheme

def AlgebraicEquivalence.IsAlgebraicallyEquivalent {S X : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (D₁ D₂ : CartierDivisorGroup X) : Prop

Two divisors D₁, D₂ on X are algebraically equivalent if there is a connected parameter scheme T over S, a divisor 𝒟 on X ×_S T, and two S-points t₁, t₂ of T whose pullbacks of 𝒟 are D₁ and D₂.

def AlgebraicEquivalence.IsAlgEquivZero {S X : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (D : CartierDivisorGroup X) : Prop

A divisor is algebraically equivalent to zero if it is algebraically equivalent to the zero divisor. The subgroup of such divisors is the kernel of the map to the Néron-Severi group.

structure AlgebraicEquivalence.IrredCompleteCurve (S : AlgebraicGeometry.Scheme) : Type (u + 1)

An irreducible complete curve over S: an integral scheme together with a proper structure morphism to S.

• toScheme : AlgebraicGeometry.Scheme
• structureMorphism : self.toScheme ⟶ S
• isIntegral : AlgebraicGeometry.IsIntegral self.toScheme
• isProper : AlgebraicGeometry.IsProper self.structureMorphism

structure AlgebraicEquivalence.CurveMorphism {S : AlgebraicGeometry.Scheme} (X Y : IrredCompleteCurve S) : Type u

A morphism of S-curves: a scheme morphism over S.

• morphism : X.toScheme ⟶ Y.toScheme
• compatible : CategoryTheory.CategoryStruct.comp self.morphism Y.structureMorphism = X.structureMorphism

def AlgebraicEquivalence.CurveMorphism.IsConstant {S : AlgebraicGeometry.Scheme} {X Y : IrredCompleteCurve S} (f : CurveMorphism X Y) : Prop

A morphism of curves is constant if it is not dominant.

theorem AlgebraicEquivalence.normalization_exists {S : AlgebraicGeometry.Scheme} (Y : IrredCompleteCurve S) : ∃ (NorY : IrredCompleteCurve S) (norMap : CurveMorphism NorY Y), AlgebraicGeometry.IsFinite norMap.morphism

Every irreducible complete curve Y admits a normalization Ỹ → Y which is a finite morphism.

theorem AlgebraicEquivalence.factorization_through_normalization {S : AlgebraicGeometry.Scheme} {X Y : IrredCompleteCurve S} (f : CurveMorphism X Y) (hf : ¬f.IsConstant) (NorY : IrredCompleteCurve S) (norMap : CurveMorphism NorY Y) (hFin : AlgebraicGeometry.IsFinite norMap.morphism) : ∃ (g : X.toScheme ⟶ NorY.toScheme), CategoryTheory.IsIso g ∧ CategoryTheory.CategoryStruct.comp g norMap.morphism = f.morphism

Any non-constant morphism f : X → Y of curves with X smooth/normal factors uniquely through the normalization Ỹ → Y.