Transporting divisor class groups along a reindexing of points

Let S be an order system on points X with functions G, and T an order system on points Y with functions H. An equivalence e : X ≃ Y reindexes Weil divisors by Finsupp.domCongr e. Suppose that, for an additive equivalence φ : G ≃+ H, reindexing carries the principal divisor of every g : G to the principal divisor of φ g. Then reindexing carries the principal divisors of S onto those of T, so it descends to an isomorphism of divisor class groups S.ClassGroup ≃+ T.ClassGroup. If weights v on X and w on Y correspond under e, the isomorphism preserves weighted degrees and restricts to an isomorphism of the degree-zero parts S.picZero v ≃+ T.picZero w.

This is the mechanism for comparing divisor class groups of two models of one curve: for instance, the codimension-one points of a curve and the places of its function field, or the places of two isomorphic function fields.

Main declarations

• WeilDivisor.OrderSystem.classGroupCongr: the induced isomorphism of divisor class groups;
• WeilDivisor.OrderSystem.picZeroCongr: its restriction to the degree-zero parts.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.map_domCongr_principalSubgroup {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) : AddSubgroup.map (Finsupp.domCongr e).toAddMonoidHom S.principalSubgroup = T.principalSubgroup

Reindexing along e carries the principal divisors of S onto those of T, when it carries the principal divisor of each g to that of φ g.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupCongr {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) : S.ClassGroup ≃+ T.ClassGroup

Transport of divisor class groups. If reindexing Weil divisors along e : X ≃ Y carries the principal divisor of every g to the principal divisor of φ g, it induces an isomorphism S.ClassGroup ≃+ T.ClassGroup.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupCongr_divisorClass {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) (D : WeilDivisor X) : (classGroupCongr e φ h) (S.divisorClass D) = T.divisorClass ((Finsupp.domCongr e) D)

classGroupCongr sends the class of D to the class of its reindexing.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.classGroupCongr_symm_divisorClass {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) (D : WeilDivisor Y) : (classGroupCongr e φ h).symm (T.divisorClass D) = S.divisorClass ((Finsupp.domCongr e).symm D)

The inverse of classGroupCongr sends the class of D to the class of its reindexing along e.symm.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.weightedDegreeClass_classGroupCongr {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) {v : X → ℤ} {w : Y → ℤ} (hv : S.IsWeightedDegreeZero v) (hw : T.IsWeightedDegreeZero w) (hvw : ∀ (x : X), w (e x) = v x) (c : S.ClassGroup) : (weightedDegreeClass w hw) ((classGroupCongr e φ h) c) = (weightedDegreeClass v hv) c

classGroupCongr preserves the weighted degree of divisor classes, for weights that correspond under e.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.map_picZero_classGroupCongr {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) {v : X → ℤ} {w : Y → ℤ} (hv : S.IsWeightedDegreeZero v) (hw : T.IsWeightedDegreeZero w) (hvw : ∀ (x : X), w (e x) = v x) : AddSubgroup.map (classGroupCongr e φ h).toAddMonoidHom (picZero v hv) = picZero w hw

classGroupCongr carries the degree-zero part of S onto that of T.

noncomputable def TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.picZeroCongr {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) {v : X → ℤ} {w : Y → ℤ} (hv : S.IsWeightedDegreeZero v) (hw : T.IsWeightedDegreeZero w) (hvw : ∀ (x : X), w (e x) = v x) : ↥(picZero v hv) ≃+ ↥(picZero w hw)

Transport of the degree-zero part of the class group. The isomorphism classGroupCongr restricts to an isomorphism S.picZero v ≃+ T.picZero w for weights that correspond under e.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_picZeroCongr_apply {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) {v : X → ℤ} {w : Y → ℤ} (hv : S.IsWeightedDegreeZero v) (hw : T.IsWeightedDegreeZero w) (hvw : ∀ (x : X), w (e x) = v x) (c : ↥(picZero v hv)) : ↑((picZeroCongr e φ h hv hw hvw) c) = (classGroupCongr e φ h) ↑c

picZeroCongr is the restriction of classGroupCongr.

@[simp]

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.coe_picZeroCongr_symm_apply {X : Type u_1} {Y : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] {S : OrderSystem X G} {T : OrderSystem Y H} (e : X ≃ Y) (φ : G ≃+ H) (h : ∀ (g : G), (Finsupp.domCongr e) (S.principalDivisor g) = T.principalDivisor (φ g)) {v : X → ℤ} {w : Y → ℤ} (hv : S.IsWeightedDegreeZero v) (hw : T.IsWeightedDegreeZero w) (hvw : ∀ (x : X), w (e x) = v x) (c : ↥(picZero w hw)) : ↑((picZeroCongr e φ h hv hw hvw).symm c) = (classGroupCongr e φ h).symm ↑c

The inverse of picZeroCongr is the restriction of the inverse of classGroupCongr.