Pullback of divisors on Riemann surfaces

A finite holomorphic map f : X → Y pulls a divisor on Y back to X by multiplying the coefficient at f x by the local multiplicity of f at x. The resulting function on X has finite support because f has finite fibres. This file packages the construction as the additive homomorphism TauCeti.RiemannSurface.divisorPullback on the existing finite formal sums TauCeti.AlgebraicGeometry.WeilDivisor.

Pullback is contravariantly functorial. On a point divisor it is the sum of the points in the fibre, weighted by their local multiplicities, and therefore its divisor degree is the analytic degree of the map. More generally, pullback multiplies divisor degree by the degree of the finite holomorphic map. These formulas are the divisor-theoretic form of counting a fibre with multiplicity and are used to construct ramification divisors.

Main declarations

• TauCeti.RiemannSurface.divisorPullback: pullback of finite formal divisors by a finite holomorphic map.
• TauCeti.RiemannSurface.coeff_divisorPullback: the coefficient of the pullback at a point.
• TauCeti.RiemannSurface.divisorPullback_comp: pullback reverses composition.
• TauCeti.RiemannSurface.degree_divisorPullback: pullback multiplies divisor degree by the degree of the map.

References

• The coefficientwise construction and its API adapt the function-field conorm formalization in TauCeti.FieldTheory.FunctionField.Divisor.Conorm to finite holomorphic maps.
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Graduate Studies in Mathematics 5, American Mathematical Society, 1995, Chapter II §4.

noncomputable def TauCeti.RiemannSurface.divisorPullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : FiniteHolomorphicMap X Y) : AlgebraicGeometry.WeilDivisor Y →+ AlgebraicGeometry.WeilDivisor X

Pullback of a divisor by a finite holomorphic map. The coefficient at x is the coefficient at f x, multiplied by the local multiplicity of f at x.

Equations

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

@[simp]

theorem TauCeti.RiemannSurface.coeff_divisorPullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : FiniteHolomorphicMap X Y) (D : AlgebraicGeometry.WeilDivisor Y) (x : X) : ((divisorPullback f) D).coeff x = ↑(localMultiplicity (↑f) x) * D.coeff (↑f x)

The coefficient of a pulled-back divisor is the coefficient at the image point multiplied by the local multiplicity.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.IsEffective.divisorPullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {D : WeilDivisor Y} (hD : D.IsEffective) (f : RiemannSurface.FiniteHolomorphicMap X Y) : ((RiemannSurface.divisorPullback f) D).IsEffective

Pullback preserves effective divisors.

@[simp]

theorem TauCeti.RiemannSurface.divisorPullback_ofPoint {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : FiniteHolomorphicMap X Y) (y : Y) : (divisorPullback f) (AlgebraicGeometry.WeilDivisor.ofPoint y) = AlgebraicGeometry.WeilDivisor.ofFinsetWithMultiplicity ⋯.toFinset (localMultiplicity ↑f)

Pulling back a point divisor gives the fibre, with each point weighted by its local multiplicity.

@[simp]

theorem TauCeti.RiemannSurface.support_divisorPullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] (f : FiniteHolomorphicMap X Y) (D : AlgebraicGeometry.WeilDivisor Y) : ↑((divisorPullback f) D).support = ↑f ⁻¹' ↑D.support

The support of a pulled-back divisor is the preimage of the original support.

@[simp]

theorem TauCeti.RiemannSurface.divisorPullback_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : divisorPullback (g.comp f) = (divisorPullback f).comp (divisorPullback g)

Pullback of divisors reverses composition of finite holomorphic maps.

theorem TauCeti.RiemannSurface.degree_divisorPullback_ofPoint {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) (y : Y) : AlgebraicGeometry.WeilDivisor.degree ((divisorPullback f) (AlgebraicGeometry.WeilDivisor.ofPoint y)) = ↑(degree ↑f)

Pulling back a point divisor has divisor degree equal to the degree of the finite holomorphic map.

@[simp]

theorem TauCeti.RiemannSurface.degree_divisorPullback {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) (D : AlgebraicGeometry.WeilDivisor Y) : AlgebraicGeometry.WeilDivisor.degree ((divisorPullback f) D) = ↑(degree ↑f) * AlgebraicGeometry.WeilDivisor.degree D

Pullback multiplies the degree of a divisor by the degree of the finite holomorphic map.