Documentation

TauCeti.AlgebraicGeometry.WeilDivisor.Action

Monoid and group actions on Weil divisors #

A monoid G acting on a type of points X acts on the formal divisors WeilDivisor X by pushing point coefficients forward: g • ∑ n_x [x] = ∑ n_x [g • x]. This file registers that action and records how it interacts with the divisor vocabulary — coefficients, point divisors, the order, effectivity, and the (weighted) degree.

The underlying scalar multiplication is Mathlib's Finsupp.comapSMul, the action on the domain of a finitely supported function; Mathlib keeps it out of the instance graph because on a general α →₀ M it competes with the action on the values M. The same overlap exists here whenever G also acts on ℤ (for instance ℕ acting on WeilDivisor ℕ), so the domain action is only a scoped instance, available after open scoped TauCeti.AlgebraicGeometry.WeilDivisor; TauCeti.AlgebraicGeometry.WeilDivisor.smul_def identifies it with the formal pushforward. Concrete settings where no competing action exists, such as automorphisms of a function field acting on its divisors, register it globally.

Main results #

source
@[instance_reducible]
noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.instDistribMulAction {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] :
DistribMulAction G (WeilDivisor X)

A monoid acting on the points acts on the divisors by pushing point coefficients forward. This is Mathlib's Finsupp.comapSMul, the action on the domain of a finitely supported function. It is scoped because it overlaps with the coefficientwise action whenever G also acts on ℤ.

Equations
Instances For
    source
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.smul_def {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] (g : G) (D : WeilDivisor X) :
    g • D = (pushforward fun (x : X) => g • x) D

    The action is the formal pushforward along the action on points.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.smul_ofPoint {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] (g : G) (x : X) :
    g • ofPoint x = ofPoint (g • x)

    The action carries the point divisor at x to the point divisor at g • x.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.degree_smul {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] (g : G) (D : WeilDivisor X) :
    degree (g • D) = degree D

    A monoid action on the points preserves the unweighted degree.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.weightedDegree_smul {G : Type u_1} {X : Type u_2} [Monoid G] [MulAction G X] (g : G) (w : X → ℤ) (D : WeilDivisor X) :
    (weightedDegree w) (g • D) = (weightedDegree fun (x : X) => w (g • x)) D

    A monoid action on the points transports a weighted degree into the weighted degree against the weight composed with the action.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.coeff_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (g : G) (D : WeilDivisor X) (x : X) :
    (g • D).coeff x = D.coeff (g⁻¹ • x)

    The coefficient of x in g • D is the coefficient of g⁻¹ • x in D.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.smul_le_smul_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (g : G) {D E : WeilDivisor X} :
    g • D ≤ g • E ↔ D ≤ E

    The action preserves the coefficientwise order on Weil divisors.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.WeilDivisor.isEffective_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (g : G) {D : WeilDivisor X} :
    (g • D).IsEffective ↔ D.IsEffective

    The action preserves effectivity of Weil divisors.