Divisor classes and line bundles

This file provides checked interfaces between three existing notions:

• Tau Ceti's locally free rank-one InvertibleSheaf;
• AINTLIB's tensor-unit definition of the Picard group of a scheme;
• Tau Ceti's Weil-divisor class group.

The scheme-level bridge is stated relative to the exact comparison between local rank-one freeness and tensor-invertibility that it needs. Given a principal-trivial divisor-to-Picard homomorphism, the universal property of the divisor class group then supplies the descent. If the kernel is exactly the principal divisors and the map is surjective, the descent is an equivalence.

At the scheme level, a full invertible-sheaf/Picard comparison together with a divisor-class equivalence constructs the entire dictionary: chosen line bundles come from skeleton representatives, their tensor-additivity holds up to isomorphism, and exactness supplies principal triviality. Conversely, every exact dictionary forces precisely those two global outputs. Thus the remaining global Challenge has a checked irreducible characterization rather than hiding additional localization assumptions.

Unconditionally, the current dependency graph supports the standard-sign class-level dictionary for an affine Dedekind curve, tensor-additive chosen invertible-module representatives, and tilde line bundles whose isomorphism classes detect linear equivalence exactly. The checked representative formula below sends the divisor of a fractional ideal to the inverse of that ideal's Picard class. The affine localization bridge is also unconditional: restriction of tilde to a principal open is identified through localized global sections, and a finite basic-open cover proves that tilde of every invertible module is an invertible sheaf. The further comparison with AINTLIB's scheme Picard group is now canonical in the forward direction: the localized tensor comparison assembles to a tilde tensor-product isomorphism, hence an injective homomorphism from the module Picard group to the scheme Picard group. Consequently the affine divisor map has exactly the principal divisors as its kernel, and divisor classes are unconditionally equivalent to their canonical image in scheme Picard. Surjectivity of that map is proved equivalent to the reverse tensor-unit/local-rank-one comparison. The forward comparison is reduced to the precise missing localization reflection from invertibility of tilde back to invertibility of the module. Thus the full affine comparison is exactly forward tensor-invertibility plus canonical Picard surjectivity, and the affine Dedekind dictionary exists exactly when that comparison does.

@[instance_reducible]

noncomputable def MazurTorsion.AlgebraicGeometry.schemeModulesMonoidal (X : AlgebraicGeometry.Scheme) : CategoryTheory.MonoidalCategory X.Modules

The AINTLIB monoidal structure used locally to inspect representatives of Scheme.Pic.

Equations

• MazurTorsion.AlgebraicGeometry.schemeModulesMonoidal X = AlgebraicGeometry.Scheme.Modules.monoidalCategory X

@[instance_reducible]

noncomputable def MazurTorsion.AlgebraicGeometry.schemeModulesSymmetric (X : AlgebraicGeometry.Scheme) : CategoryTheory.SymmetricCategory X.Modules

The AINTLIB symmetric structure used locally for the commutative Picard group.

Equations

• MazurTorsion.AlgebraicGeometry.schemeModulesSymmetric X = AlgebraicGeometry.Scheme.Modules.symmetricCategory X

@[reducible, inline]

abbrev MazurTorsion.AlgebraicGeometry.PicardGroup (X : AlgebraicGeometry.Scheme) : Type (u + 1)

The additive form of the scheme Picard group, used by divisor homomorphisms.

Equations

• MazurTorsion.AlgebraicGeometry.PicardGroup X = Additive X.Pic

def MazurTorsion.AlgebraicGeometry.IsTensorInvertible (X : AlgebraicGeometry.Scheme) (M : X.Modules) : Prop

Categorical tensor-invertibility of a sheaf of modules.

Equations

• MazurTorsion.AlgebraicGeometry.IsTensorInvertible X M = IsUnit (CategoryTheory.toSkeleton M)

def MazurTorsion.AlgebraicGeometry.TensorInverseComparison (X : AlgebraicGeometry.Scheme) : Prop

The exact forward comparison needed to attach a Picard class to a locally free rank-one sheaf: such a sheaf admits a tensor inverse.

Equations

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

def MazurTorsion.AlgebraicGeometry.TensorUnitLocalTriviality (X : AlgebraicGeometry.Scheme) : Prop

The reverse comparison: every tensor-unit class has a locally free rank-one representative.

Equations

• MazurTorsion.AlgebraicGeometry.TensorUnitLocalTriviality X = ∀ (M : X.Modules), MazurTorsion.AlgebraicGeometry.IsTensorInvertible X M → TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M

def MazurTorsion.AlgebraicGeometry.PicardComparison (X : AlgebraicGeometry.Scheme) : Prop

The comparison between locally free rank-one sheaves and tensor units.

Equations

• MazurTorsion.AlgebraicGeometry.PicardComparison X = ∀ (M : X.Modules), TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M ↔ MazurTorsion.AlgebraicGeometry.IsTensorInvertible X M

theorem MazurTorsion.AlgebraicGeometry.TensorInverseComparison.isTensorInvertible {X : AlgebraicGeometry.Scheme} (hX : TensorInverseComparison X) {M : X.Modules} (hM : TauCeti.AlgebraicGeometry.SheafOfModules.isInvertible X M) : IsTensorInvertible X M

A chosen tensor inverse makes the skeleton class of a locally free rank-one sheaf a unit.

noncomputable def MazurTorsion.AlgebraicGeometry.TensorInverseComparison.toPic {X : AlgebraicGeometry.Scheme} (hX : TensorInverseComparison X) (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) : X.Pic

The Picard class represented by an invertible sheaf, using only the forward tensor-inverse comparison.

Equations

• hX.toPic L = IsUnit.unit ⋯

@[simp]

theorem MazurTorsion.AlgebraicGeometry.TensorInverseComparison.toPic_val {X : AlgebraicGeometry.Scheme} (hX : TensorInverseComparison X) (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) : ↑(hX.toPic L) = CategoryTheory.toSkeleton L.obj

noncomputable def MazurTorsion.AlgebraicGeometry.TensorInverseComparison.trivialIsoTensorUnit {X : AlgebraicGeometry.Scheme} : (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules

The globally free rank-one sheaf is the tensor unit for AINTLIB's localized monoidal structure on sheaves of modules. The first isomorphism identifies the singleton coproduct with Mathlib's ordinary unit sheaf; the adjunction counit then identifies that sheaf with the sheafified monoidal unit.

Equations

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

@[simp]

theorem MazurTorsion.AlgebraicGeometry.TensorInverseComparison.toPic_trivial {X : AlgebraicGeometry.Scheme} (hX : TensorInverseComparison X) : hX.toPic (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X) = 1

The globally trivial invertible sheaf represents the identity of the scheme Picard group.

theorem MazurTorsion.AlgebraicGeometry.IsTensorInvertible.exists_tensorInverse {X : AlgebraicGeometry.Scheme} {M : X.Modules} (hM : IsTensorInvertible X M) : ∃ (N : X.Modules), Nonempty (CategoryTheory.MonoidalCategoryStruct.tensorObj M N ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

A tensor-unit class has a chosen sheaf representative of its inverse.

def MazurTorsion.AlgebraicGeometry.TildeInvertibility (R : Type u) [CommRing R] : Prop

The affine localization input saying that the sheaf associated to an invertible module is locally free of rank one.

Equations

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

def MazurTorsion.AlgebraicGeometry.UniversalTildeInvertibility : Prop

The tilde-localization comparison, uniformly for commutative rings in one universe.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTensorEquivOfIsLocalization (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) (A : Type u) [CommRing A] [Algebra R A] [IsLocalization S A] : TensorProduct A (LocalizedModule S M) (LocalizedModule S N) ≃ₗ[A] LocalizedModule S (TensorProduct R M N)

Tensor product commutes with localization of both modules, for an arbitrary chosen localization ring.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTensorEquivOfIsLocalization_mk_one (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) (A : Type u) [CommRing A] [Algebra R A] [IsLocalization S A] (m : M) (n : N) : (localizedTensorEquivOfIsLocalization R M N S A) (LocalizedModule.mk m 1 ⊗ₜ[A] LocalizedModule.mk n 1) = LocalizedModule.mk (m ⊗ₜ[R] n) 1

The tensor-localization equivalence sends the tensor of two denominator-one fractions to the denominator-one fraction of their tensor.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTensorEquivOfIsLocalization_mk (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) (A : Type u) [CommRing A] [Algebra R A] [IsLocalization S A] (m : M) (n : N) (s t : ↥S) : (localizedTensorEquivOfIsLocalization R M N S A) (LocalizedModule.mk m s ⊗ₜ[A] LocalizedModule.mk n t) = LocalizedModule.mk (m ⊗ₜ[R] n) (s * t)

The tensor-localization equivalence multiplies denominators on arbitrary pure fractions.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTensorEquiv (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) : TensorProduct (Localization S) (LocalizedModule S M) (LocalizedModule S N) ≃ₗ[Localization S] LocalizedModule S (TensorProduct R M N)

Tensor product commutes with localization, using Mathlib's canonical module structures on LocalizedModule. This specialization can therefore be applied directly to stalk elements.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTensorEquiv_mk (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Submonoid R) (m : M) (n : N) (s t : ↥S) : (localizedTensorEquiv R M N S) (LocalizedModule.mk m s ⊗ₜ[Localization S] LocalizedModule.mk n t) = LocalizedModule.mk (m ⊗ₜ[R] n) (s * t)

The canonical localization tensor equivalence multiplies the denominators of pure fractions.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorPure (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (a : (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op U)) (b : (AlgebraicGeometry.structureSheafInType R N).obj.obj (Opposite.op U)) : (AlgebraicGeometry.structureSheafInType R (TensorProduct R M N)).obj.obj (Opposite.op U)

Pointwise tensor multiplication of locally fractional sections. The local-fraction proof intersects the two witnessing neighborhoods and multiplies their denominators.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorMap (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) : (CategoryTheory.MonoidalCategoryStruct.tensorObj (AlgebraicGeometry.moduleStructurePresheaf R M) (AlgebraicGeometry.moduleStructurePresheaf R N)).obj (Opposite.op U) ⟶ (AlgebraicGeometry.moduleStructurePresheaf R (TensorProduct R M N)).obj (Opposite.op U)

The sectionwise bilinear pairing from the pointwise tensor of tilde presheaves to the tilde presheaf of the module tensor product.

Equations

• MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorMap R M N U = ModuleCat.MonoidalCategory.tensorLift (MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorPure R M N U) ⋯ ⋯ ⋯ ⋯

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.tensorToTildePresheaf (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : CategoryTheory.MonoidalCategoryStruct.tensorObj (AlgebraicGeometry.moduleStructurePresheaf R M) (AlgebraicGeometry.moduleStructurePresheaf R N) ⟶ AlgebraicGeometry.moduleStructurePresheaf R (TensorProduct R M N)

The natural presheaf morphism underlying the tensor-product comparison for tilde.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.basicOpenTensorEquiv (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : R) : TensorProduct ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))) ((AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))) ((AlgebraicGeometry.structureSheafInType R N).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))) ≃ₗ[(AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))] (AlgebraicGeometry.structureSheafInType R (TensorProduct R M N)).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))

On a principal open, the sectionwise tensor pairing is the standard equivalence between the tensor of two localized modules and the localization of their tensor.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.basicOpenTensorEquiv_tmul_toOpen (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : R) (m : M) (n : N) : (basicOpenTensorEquiv R M N f) ((AlgebraicGeometry.StructureSheaf.toOpenₗ R M (PrimeSpectrum.basicOpen f)) m ⊗ₜ[(AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))] (AlgebraicGeometry.StructureSheaf.toOpenₗ R N (PrimeSpectrum.basicOpen f)) n) = (AlgebraicGeometry.StructureSheaf.toOpenₗ R (TensorProduct R M N) (PrimeSpectrum.basicOpen f)) (m ⊗ₜ[R] n)

The principal-open equivalence sends a tensor of denominator-one sections to the denominator-one section of the tensor.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorMap_tmul_toOpen (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : R) (m : M) (n : N) : sectionsTensorPure R M N (PrimeSpectrum.basicOpen f) ((AlgebraicGeometry.StructureSheaf.toOpenₗ R M (PrimeSpectrum.basicOpen f)) m) ((AlgebraicGeometry.StructureSheaf.toOpenₗ R N (PrimeSpectrum.basicOpen f)) n) = (AlgebraicGeometry.StructureSheaf.toOpenₗ R (TensorProduct R M N) (PrimeSpectrum.basicOpen f)) (m ⊗ₜ[R] n)

On denominator-one sections, the section pairing has the expected pure-tensor formula.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorMap_basicOpen (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : R) : sectionsTensorMap R M N (PrimeSpectrum.basicOpen f) = ModuleCat.ofHom ↑(basicOpenTensorEquiv R M N f)

The section pairing on a principal open agrees with the localization equivalence after reducing arbitrary fractions to scalar multiples of denominator-one sections.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.sectionsTensorMap_basicOpen_bijective (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : R) : Function.Bijective ⇑(ModuleCat.Hom.hom (sectionsTensorMap R M N (PrimeSpectrum.basicOpen f)))

Every principal-open component of the tilde tensor presheaf morphism is bijective.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.sheafifyValIso (R : Type u) [CommRing R] (P : (AlgebraicGeometry.Spec (CommRingCat.of R)).Modules) : (MazurTorsion.AlgebraicGeometry.AffineTilde.affineSheafification✝ R).obj P.val ≅ P

Sheafifying the underlying presheaf of a sheaf of modules returns that sheaf. This is the reflective sheafification counit, specialized to an affine scheme.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.tensorAsSheafification (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : CategoryTheory.MonoidalCategoryStruct.tensorObj (AlgebraicGeometry.tilde (ModuleCat.of R M)) (AlgebraicGeometry.tilde (ModuleCat.of R N)) ≅ (MazurTorsion.AlgebraicGeometry.AffineTilde.affineSheafification✝ R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (MazurTorsion.AlgebraicGeometry.AffineTilde.underlyingAffineModule✝ R (AlgebraicGeometry.tilde (ModuleCat.of R M))) (MazurTorsion.AlgebraicGeometry.AffineTilde.underlyingAffineModule✝ R (AlgebraicGeometry.tilde (ModuleCat.of R N))))

The localized monoidal structure identifies the tensor of two tilde sheaves with the sheafification of the pointwise tensor of their underlying presheaves.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.tildeTensorUnderlyingHom (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : CategoryTheory.MonoidalCategoryStruct.tensorObj (MazurTorsion.AlgebraicGeometry.AffineTilde.underlyingAffineModule✝ R (AlgebraicGeometry.tilde (ModuleCat.of R M))) (MazurTorsion.AlgebraicGeometry.AffineTilde.underlyingAffineModule✝ R (AlgebraicGeometry.tilde (ModuleCat.of R N))) ⟶ MazurTorsion.AlgebraicGeometry.AffineTilde.underlyingAffineModule✝ R (AlgebraicGeometry.tilde (ModuleCat.of R (TensorProduct R M N)))

The locally bijective presheaf morphism used to compare the sheaf tensor with tilde of the module tensor product.

Equations

• MazurTorsion.AlgebraicGeometry.AffineTilde.tildeTensorUnderlyingHom R M N = MazurTorsion.AlgebraicGeometry.AffineTilde.tensorToTildePresheaf R M N

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.tildeTensorUnderlyingHom_memW (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : MazurTorsion.AlgebraicGeometry.AffineTilde.affineSheafificationW✝ R (tildeTensorUnderlyingHom R M N)

The presheaf tensor comparison is inverted by sheafification because its components are bijective on the basis of principal opens.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.tildeTensorIso (R : Type u) [CommRing R] (M N : Type u) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : CategoryTheory.MonoidalCategoryStruct.tensorObj (AlgebraicGeometry.tilde (ModuleCat.of R M)) (AlgebraicGeometry.tilde (ModuleCat.of R N)) ≅ AlgebraicGeometry.tilde (ModuleCat.of R (TensorProduct R M N))

On an affine scheme, the sheaf tensor product of two tilde objects agrees with tilde of the module tensor product.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.tildeTensorInverseIso (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] [Module.Invertible R M] : CategoryTheory.MonoidalCategoryStruct.tensorObj (AlgebraicGeometry.tilde (ModuleCat.of R M)) (AlgebraicGeometry.tilde (ModuleCat.of R (Module.Dual R M))) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgebraicGeometry.Spec (CommRingCat.of R)).Modules

The tilde sheaf of an invertible module has the tilde sheaf of its dual as an explicit tensor inverse.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.tilde_isTensorInvertible (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] [Module.Invertible R M] : IsTensorInvertible (AlgebraicGeometry.Spec (CommRingCat.of R)) (AlgebraicGeometry.tilde (ModuleCat.of R M))

Tilde sends every invertible module to a tensor-invertible sheaf. This proves the forward Picard comparison for the affine tilde representatives used below, without assuming a global comparison for arbitrary sheaves.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicClass (R : Type u) [CommRing R] (I : CommRing.Pic R) : (AlgebraicGeometry.Spec (CommRingCat.of R)).Pic

The scheme Picard class represented by the tilde sheaf of a module Picard-class representative.

Equations

• MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicClass R I = IsUnit.unit ⋯

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicClass_val (R : Type u) [CommRing R] (I : CommRing.Pic R) : ↑(modulePicToSchemePicClass R I) = CategoryTheory.toSkeleton (AlgebraicGeometry.tilde (ModuleCat.of R I.AsModule))

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicClass_one (R : Type u) [CommRing R] : modulePicToSchemePicClass R 1 = 1

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicClass_mul (R : Type u) [CommRing R] (I J : CommRing.Pic R) : modulePicToSchemePicClass R (I * J) = modulePicToSchemePicClass R I * modulePicToSchemePicClass R J

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePic (R : Type u) [CommRing R] : CommRing.Pic R →* (AlgebraicGeometry.Spec (CommRingCat.of R)).Pic

The canonical comparison from the module Picard group of a ring to the scheme Picard group of its spectrum, induced by tilde.

Equations

• MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePic R = { toFun := MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicClass R, map_one' := ⋯, map_mul' := ⋯ }

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePic_injective (R : Type u) [CommRing R] : Function.Injective ⇑(modulePicToSchemePic R)

The tilde comparison from module Picard classes to scheme Picard classes is injective. Equality in the scheme skeleton gives an isomorphism of tilde sheaves, and full faithfulness of tilde recovers a linear equivalence of the module representatives.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicAdd (R : Type u) [CommRing R] : Additive (CommRing.Pic R) →+ PicardGroup (AlgebraicGeometry.Spec (CommRingCat.of R))

The additive form of the canonical comparison from module Picard classes to scheme Picard classes.

Equations

• MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicAdd R = MonoidHom.toAdditive (MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePic R)

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePicAdd_injective (R : Type u) [CommRing R] : Function.Injective ⇑(modulePicToSchemePicAdd R)

The additive tilde comparison is injective.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePic_surjective_of_tensorUnitLocalTriviality (R : Type u) [CommRing R] (hreverse : TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))) : Function.Surjective ⇑(modulePicToSchemePic R)

If every tensor-unit sheaf on an affine scheme is locally free of rank one, then every scheme Picard class is represented by tilde of an invertible module.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicEquivSchemePicOfTensorUnitLocalTriviality (R : Type u) [CommRing R] (hreverse : TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))) : Additive (CommRing.Pic R) ≃+ PicardGroup (AlgebraicGeometry.Spec (CommRingCat.of R))

Under the exact reverse Picard comparison, tilde gives an additive equivalence from module Picard classes to affine-scheme Picard classes.

Equations

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

def MazurTorsion.AlgebraicGeometry.AffineTilde.TildeReflectsInvertibility (R : Type u) [CommRing R] : Prop

The precise missing affine localization reflection: if tilde of a module is locally free of rank one, then the module is invertible. The converse is tildeInvertibility below.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.tensorInverseComparison_of_tildeReflectsInvertibility (R : Type u) [CommRing R] (hreflect : TildeReflectsInvertibility R) : TensorInverseComparison (AlgebraicGeometry.Spec (CommRingCat.of R))

Reflection of rank-one local freeness through tilde supplies the forward tensor-inverse comparison for every invertible sheaf on an affine scheme.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTildeRestrictIso {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) : AlgebraicGeometry.tilde (ModuleCat.of (MazurTorsion.AlgebraicGeometry.AffineTilde.awayRing✝ f) (LocalizedModule.Away f ↑M)) ≅ (AlgebraicGeometry.tilde M).restrict (MazurTorsion.AlgebraicGeometry.AffineTilde.awaySpecMap✝ f)

Tilde commutes with localization to a principal open: the tilde of the localized module is isomorphic to the restriction of the original tilde sheaf along Spec R[1/f] ⟶ Spec R.

Equations

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

@[reducible, inline]

noncomputable abbrev MazurTorsion.AlgebraicGeometry.specBasicOpen (R : CommRingCat) (r : ↑R) : (AlgebraicGeometry.Spec R).Opens

The basic open of Spec R associated to r, expressed in the scheme's own type of opens. This avoids hiding the comparison between the scheme topology and the raw prime spectrum.

Equations

• MazurTorsion.AlgebraicGeometry.specBasicOpen R r = PrimeSpectrum.basicOpen r

def MazurTorsion.AlgebraicGeometry.BasicOpenTildeTriviality (R : CommRingCat) (M : ModuleCat ↑R) : Prop

The precise affine localization input: whenever Mₙ is free on D(r), the restriction of tilde M to that basic open is the free rank-one sheaf.

Equations

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

def MazurTorsion.AlgebraicGeometry.UniversalBasicOpenTildeTriviality : Prop

The basic-open tilde comparison, uniformly for rings and modules in one universe.

Equations

• MazurTorsion.AlgebraicGeometry.UniversalBasicOpenTildeTriviality = ∀ (R : CommRingCat) (M : ModuleCat ↑R), MazurTorsion.AlgebraicGeometry.BasicOpenTildeTriviality R M

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.localizedTildeFreeIso {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) [Module.Invertible ↑R ↑M] [Module.Free (Localization.Away f) (LocalizedModule.Away f ↑M)] : SheafOfModules.free PUnit.{u + 1} ≅ (AlgebraicGeometry.tilde M).restrict (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

If the localization of an invertible module at f is free, its tilde sheaf on Spec R[1/f] is the free rank-one sheaf and hence trivializes the restricted original sheaf.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineTilde.basicOpenTrivialization {R : CommRingCat} (M : ModuleCat ↑R) (f : ↑R) [Module.Invertible ↑R ↑M] [Module.Free (Localization.Away f) (LocalizedModule.Away f ↑M)] : SheafOfModules.free PUnit.{u + 1} ≅ SheafOfModules.over (AlgebraicGeometry.tilde M) (specBasicOpen R f)

The checked basic-open trivialization required by Tau Ceti's local definition of an invertible sheaf.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.universalBasicOpenTildeTriviality : UniversalBasicOpenTildeTriviality

The pinned Mathlib and Tau Ceti APIs prove the universal basic-open tilde comparison.

theorem MazurTorsion.AlgebraicGeometry.tilde_isInvertible_of_basicOpenTriviality (R : CommRingCat) (M : ModuleCat ↑R) [Module.Invertible ↑R ↑M] (h : BasicOpenTildeTriviality R M) : TauCeti.SheafOfModules.IsInvertible (AlgebraicGeometry.tilde M)

Finite basic-open freeness of an invertible module and the exact local restriction comparison imply that its tilde sheaf is invertible.

theorem MazurTorsion.AlgebraicGeometry.UniversalBasicOpenTildeTriviality.toUniversalTildeInvertibility (h : UniversalBasicOpenTildeTriviality) : UniversalTildeInvertibility

The exact basic-open localization theorem entails the formerly bundled global tilde invertibility statement.

theorem MazurTorsion.AlgebraicGeometry.universalTildeInvertibility : UniversalTildeInvertibility

Tilde of every invertible module is an invertible sheaf. This is now unconditional in the pinned dependency graph.

theorem MazurTorsion.AlgebraicGeometry.tildeInvertibility (R : Type u) [CommRing R] : TildeInvertibility R

The universe-local form of unconditional tilde invertibility.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.tensorUnitLocalTriviality_of_modulePicToSchemePic_surjective (R : Type u) [CommRing R] (hsurjective : Function.Surjective ⇑(modulePicToSchemePic R)) : TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))

Conversely, surjectivity of the canonical affine tilde map forces every tensor-unit sheaf to be locally free of rank one.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.modulePicToSchemePic_surjective_iff_tensorUnitLocalTriviality (R : Type u) [CommRing R] : Function.Surjective ⇑(modulePicToSchemePic R) ↔ TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))

Surjectivity of the canonical affine module-Picard comparison is exactly the reverse tensor-unit/local-rank-one comparison.

theorem MazurTorsion.AlgebraicGeometry.PicardComparison.tensorInverseComparison {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) : TensorInverseComparison X

The full comparison contains the exact forward tensor-inverse comparison.

theorem MazurTorsion.AlgebraicGeometry.PicardComparison.tensorUnitLocalTriviality {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) : TensorUnitLocalTriviality X

The full comparison contains the reverse local-triviality comparison.

noncomputable def MazurTorsion.AlgebraicGeometry.PicardComparison.toPic {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) : X.Pic

The Picard class represented by an invertible sheaf.

Equations

• hX.toPic L = IsUnit.unit ⋯

@[simp]

theorem MazurTorsion.AlgebraicGeometry.PicardComparison.toPic_val {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) : ↑(hX.toPic L) = CategoryTheory.toSkeleton L.obj

noncomputable def MazurTorsion.AlgebraicGeometry.PicardComparison.representative {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) (p : X.Pic) : TauCeti.AlgebraicGeometry.InvertibleSheaf X

A chosen invertible-sheaf representative of a Picard class.

Equations

• hX.representative p = { obj := (CategoryTheory.fromSkeleton X.Modules).obj ↑p, property := ⋯ }

@[simp]

theorem MazurTorsion.AlgebraicGeometry.PicardComparison.toPic_representative {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) (p : X.Pic) : hX.toPic (hX.representative p) = p

theorem MazurTorsion.AlgebraicGeometry.PicardComparison.nonempty_representative_toPic_iso {X : AlgebraicGeometry.Scheme} (hX : PicardComparison X) (L : TauCeti.AlgebraicGeometry.InvertibleSheaf X) : Nonempty ((hX.representative (hX.toPic L)).obj ≅ L.obj)

Recovering a representative from the Picard class of a line bundle changes it only by isomorphism.

theorem MazurTorsion.AlgebraicGeometry.picardComparison_of_components {X : AlgebraicGeometry.Scheme} (hforward : TensorInverseComparison X) (hreverse : TensorUnitLocalTriviality X) : PicardComparison X

The full Picard comparison is exactly its forward tensor-inverse component together with the reverse local-triviality component.

theorem MazurTorsion.AlgebraicGeometry.AffineTilde.picardComparison_iff_tensorInverseComparison_and_modulePic_surjective (R : Type u) [CommRing R] : PicardComparison (AlgebraicGeometry.Spec (CommRingCat.of R)) ↔ TensorInverseComparison (AlgebraicGeometry.Spec (CommRingCat.of R)) ∧ Function.Surjective ⇑(modulePicToSchemePic R)

The exact full affine Picard boundary: the forward tensor-inverse construction together with surjectivity of the canonical tilde map is necessary and sufficient.

@[reducible, inline]

abbrev MazurTorsion.AlgebraicGeometry.DivisorPicard.ClassEquivalence {Y : Type u_1} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (X : AlgebraicGeometry.Scheme) : Type (max (u + 1) u_1)

The type of additive identifications between divisor classes and scheme Picard classes.

Equations

• MazurTorsion.AlgebraicGeometry.DivisorPicard.ClassEquivalence S X = (S.ClassGroup ≃+ MazurTorsion.AlgebraicGeometry.PicardGroup X)

def MazurTorsion.AlgebraicGeometry.DivisorPicard.PrincipalTrivial {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) : Prop

A divisor-to-Picard homomorphism sends every principal divisor to the identity.

Equations

• MazurTorsion.AlgebraicGeometry.DivisorPicard.PrincipalTrivial S toPic = ∀ (g : G), toPic (S.principalDivisor g) = 0

noncomputable def MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hprincipal : PrincipalTrivial S toPic) : S.ClassGroup →+ PicardGroup X

Descend a principal-trivial divisor-to-Picard construction to divisor classes.

Equations

• MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic S toPic hprincipal = TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ClassGroup.lift S toPic hprincipal

@[simp]

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic_divisorClass {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hprincipal : PrincipalTrivial S toPic) (D : TauCeti.AlgebraicGeometry.WeilDivisor Y) : (classToPic S toPic hprincipal) (S.divisorClass D) = toPic D

def MazurTorsion.AlgebraicGeometry.DivisorPicard.HasPrincipalKernel {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) : Prop

Exactness at divisors: the only divisors with trivial Picard class are principal.

Equations

• MazurTorsion.AlgebraicGeometry.DivisorPicard.HasPrincipalKernel S toPic = (toPic.ker = S.principalSubgroup)

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.principalTrivial_of_principalKernel {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hker : HasPrincipalKernel S toPic) : PrincipalTrivial S toPic

Exactness at divisors already proves that every principal divisor has trivial Picard class.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic_injective {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hprincipal : PrincipalTrivial S toPic) (hker : HasPrincipalKernel S toPic) : Function.Injective ⇑(classToPic S toPic hprincipal)

noncomputable def MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicardRange {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hker : HasPrincipalKernel S toPic) : S.ClassGroup ≃+ ↥(classToPic S toPic ⋯).range

With exact principal kernel, divisor classes are additively equivalent to the range of their Picard realization. This is the strongest codomain statement available from exactness without assuming that every scheme Picard class comes from a divisor.

Equations

• MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicardRange S toPic hker = AddEquiv.ofBijective (MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic S toPic ⋯).rangeRestrict ⋯

@[simp]

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicardRange_apply_val {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hker : HasPrincipalKernel S toPic) (c : S.ClassGroup) : ↑((classEquivPicardRange S toPic hker) c) = (classToPic S toPic ⋯) c

The range equivalence has the descended divisor-class map as its underlying Picard value.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic_surjective {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hprincipal : PrincipalTrivial S toPic) (hsurjective : Function.Surjective ⇑toPic) : Function.Surjective ⇑(classToPic S toPic hprincipal)

noncomputable def MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicard {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hker : HasPrincipalKernel S toPic) (hsurjective : Function.Surjective ⇑toPic) : ClassEquivalence S X

The strongest general divisor-class/Picard equivalence: a homomorphism with exactly principal kernel and hitting every Picard class descends to an equivalence. Principal triviality is a consequence of the kernel equality, not an additional assumption.

Equations

• MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicard S toPic hker hsurjective = AddEquiv.ofBijective (MazurTorsion.AlgebraicGeometry.DivisorPicard.classToPic S toPic ⋯) ⋯

@[simp]

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicard_divisorClass {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (toPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X) (hker : HasPrincipalKernel S toPic) (hsurjective : Function.Surjective ⇑toPic) (D : TauCeti.AlgebraicGeometry.WeilDivisor Y) : (classEquivPicard S toPic hker hsurjective) (S.divisorClass D) = toPic D

structure MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary {Y : Type u_1} {G : Type v} [AddCommGroup G] (S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G) (X : AlgebraicGeometry.Scheme) : Type (max (u + 1) u_1)

An exact scheme-level divisor-class/Picard dictionary for an order system. Besides the class map and its exactness, it records chosen invertible-sheaf representatives and the comparison between Tau Ceti's local rank-one predicate and AINTLIB's tensor-unit Picard group. The data does not assert a particular affine-chart normalization of the chosen correspondence.

• comparison : TensorInverseComparison X

  Every locally free rank-one sheaf has a tensor inverse and hence a Picard class.

• divisorToPic : TauCeti.AlgebraicGeometry.WeilDivisor Y →+ PicardGroup X

  The additive Picard class associated to a Weil divisor.

• lineBundle : TauCeti.AlgebraicGeometry.WeilDivisor Y → TauCeti.AlgebraicGeometry.InvertibleSheaf X

  An invertible-sheaf representative of the line bundle associated to a divisor.

• lineBundle_toPic (D : TauCeti.AlgebraicGeometry.WeilDivisor Y) : Additive.ofMul (⋯.toPic (self.lineBundle D)) = self.divisorToPic D

  The chosen line bundle represents the specified divisor Picard class.

• principalKernel : HasPrincipalKernel S self.divisorToPic

  Only principal divisors have trivial Picard class.

• surjective : Function.Surjective ⇑self.divisorToPic

  Every scheme Picard class is represented by a divisor.

noncomputable def MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.ofClassEquivalence {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (hX : PicardComparison X) (e : ClassEquivalence S X) : Dictionary S X

A full Picard comparison and a divisor-class/Picard equivalence canonically supply all data of an exact dictionary. The line bundle of D is the chosen invertible-sheaf representative of the image of [D]; exactness and surjectivity are inherited from the quotient equivalence.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.principalTrivial {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) : PrincipalTrivial S d.divisorToPic

Principal divisors have trivial Picard class, as a checked consequence of exactness at the divisor term.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.lineBundle_principal_iso_trivial {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) (g : G) : Nonempty ((d.lineBundle (S.principalDivisor g)).obj ≅ (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj)

The line bundle attached by an exact dictionary to a principal divisor is isomorphic to the globally trivial line bundle. This follows from exactness, compatibility with the Picard class, and the fact that equality in the skeleton is precisely existence of an isomorphism.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.lineBundle_add_iso {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) (D E : TauCeti.AlgebraicGeometry.WeilDivisor Y) : Nonempty ((d.lineBundle (D + E)).obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (d.lineBundle D).obj (d.lineBundle E).obj)

Divisor addition is represented by tensor product of the chosen line bundles, up to the isomorphism appropriate for chosen representatives.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.lineBundle_iso_of_linearlyEquivalent {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) {D E : TauCeti.AlgebraicGeometry.WeilDivisor Y} (h : S.LinearlyEquivalent D E) : Nonempty ((d.lineBundle D).obj ≅ (d.lineBundle E).obj)

The chosen line bundles of linearly equivalent divisors are isomorphic.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.nonempty_lineBundle_iso_iff_linearlyEquivalent {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) (D E : TauCeti.AlgebraicGeometry.WeilDivisor Y) : Nonempty ((d.lineBundle D).obj ≅ (d.lineBundle E).obj) ↔ S.LinearlyEquivalent D E

The exact dictionary detects linear equivalence on the chosen divisor line bundles: two such bundles are isomorphic precisely when their divisors differ by a principal divisor.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.tensorUnitLocalTriviality {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) : TensorUnitLocalTriviality X

Surjectivity of the divisor map and the chosen line-bundle representatives force the reverse Picard comparison: every tensor-unit sheaf is locally free of rank one. Thus a global dictionary need not store that comparison as an independent hypothesis.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.picardComparison {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) : PicardComparison X

An exact divisor-line-bundle dictionary supplies the full equivalence between Tau Ceti's local rank-one predicate and AINTLIB's tensor-unit predicate.

noncomputable def MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.classEquivalence {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) : ClassEquivalence S X

The divisor-class/Picard equivalence supplied by an exact dictionary.

Equations

• d.classEquivalence = MazurTorsion.AlgebraicGeometry.DivisorPicard.classEquivPicard S d.divisorToPic ⋯ ⋯

@[simp]

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.classEquivalence_divisorClass {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (d : Dictionary S X) (D : TauCeti.AlgebraicGeometry.WeilDivisor Y) : d.classEquivalence (S.divisorClass D) = d.divisorToPic D

@[simp]

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.classEquivalence_ofClassEquivalence {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} (hX : PicardComparison X) (e : ClassEquivalence S X) : (ofClassEquivalence hX e).classEquivalence = e

The divisor-class equivalence recovered from the dictionary constructed by ofClassEquivalence is the original equivalence.

theorem MazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.nonempty_iff_picardComparison_and_classEquivalence {Y : Type u_1} {X : AlgebraicGeometry.Scheme} {G : Type v} [AddCommGroup G] {S : TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem Y G} : Nonempty (Dictionary S X) ↔ PicardComparison X ∧ Nonempty (ClassEquivalence S X)

Existence of an exact dictionary is equivalent to precisely its two irreducible global outputs: the full invertible-sheaf/Picard comparison and an equivalence from divisor classes to the scheme Picard group. All chosen divisor line bundles and their compatibility are then constructed by ofClassEquivalence.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.classEquivPicard (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).ClassGroup ≃+ Additive (CommRing.Pic R)

The standard-sign affine Dedekind divisor-class/Picard equivalence. Tau Ceti's fractional ideal divisor sends an ideal to its positive valuation divisor, while O(D) is represented by the inverse ideal, hence the final negation.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.classToSchemePic (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).ClassGroup →+ PicardGroup (AlgebraicGeometry.Spec (CommRingCat.of R))

The canonical tilde-induced homomorphism from affine Dedekind divisor classes to AINTLIB's scheme Picard group.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.classToSchemePic_injective (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Function.Injective ⇑(classToSchemePic R K)

Affine Dedekind divisor classes inject canonically into the scheme Picard group.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.classEquivSchemePicRange (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).ClassGroup ≃+ ↥(classToSchemePic R K).range

The strongest unconditional affine divisor-class/scheme-Picard equivalence currently available: divisor classes are equivalent to the range of their canonical tilde realization.

Equations

• MazurTorsion.AlgebraicGeometry.AffineDedekind.classEquivSchemePicRange R K = AddEquiv.ofBijective (MazurTorsion.AlgebraicGeometry.AffineDedekind.classToSchemePic R K).rangeRestrict ⋯

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.classToSchemePic_surjective_of_tensorUnitLocalTriviality (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (hreverse : TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))) : Function.Surjective ⇑(classToSchemePic R K)

Under the reverse tensor-unit/local-rank-one comparison, every affine Dedekind divisor class is represented by the canonical tilde construction.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.classEquivSchemePicOfTensorUnitLocalTriviality (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (hreverse : TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))) : (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).ClassGroup ≃+ PicardGroup (AlgebraicGeometry.Spec (CommRingCat.of R))

The full affine divisor-class/scheme-Picard equivalence under precisely the reverse Picard comparison that makes the canonical tilde map surjective.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToPic (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R) →+ Additive (CommRing.Pic R)

The Picard class of the invertible module O(D) associated to an affine Dedekind divisor.

Equations

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

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToSchemePic (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R) →+ PicardGroup (AlgebraicGeometry.Spec (CommRingCat.of R))

The canonical affine Dedekind divisor-to-scheme-Picard homomorphism. It is the descent-ready scheme-level realization of the module line-bundle class.

Equations

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

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToSchemePic_apply (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : (divisorToSchemePic R K) D = (AffineTilde.modulePicToSchemePicAdd R) ((divisorToPic R K) D)

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.classEquivSchemePicOfTensorUnitLocalTriviality_divisorClass (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (hreverse : TensorUnitLocalTriviality (AlgebraicGeometry.Spec (CommRingCat.of R))) (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : (classEquivSchemePicOfTensorUnitLocalTriviality R K hreverse) ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).divisorClass D) = (divisorToSchemePic R K) D

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToPic_principalDivisor (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : Additive Kˣ) : (divisorToPic R K) ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).principalDivisor g) = 0

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToSchemePic_principalDivisor (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : Additive Kˣ) : (divisorToSchemePic R K) ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).principalDivisor g) = 0

Principal divisors give the zero scheme-Picard class.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToSchemePic_kernel (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : (divisorToSchemePic R K).ker = (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).principalSubgroup

The kernel of the canonical divisor-to-scheme-Picard map consists exactly of principal divisors. Thus its factorization through classToSchemePic is an honest descent to divisor classes, with no unproved surjectivity claim.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleClass (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : CommRing.Pic R

The multiplicative Picard class underlying divisorToPic.

Equations

• MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleClass R K D = Additive.toMul ((MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToPic R K) D)

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleClass_fractionalIdealDivisor (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ) : lineBundleClass R K ((TauCeti.AlgebraicGeometry.WeilDivisor.fractionalIdealDivisor R K) (Additive.ofMul I)) = ((ClassGroup.equivPic R) ((ClassGroup.mk K) I))⁻¹

On the divisor of an invertible fractional ideal I, the standard line-bundle class is the inverse of the Picard class represented by I.

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.classEquivPicard_divisorClass (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : (classEquivPicard R K) ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).divisorClass D) = Additive.ofMul (lineBundleClass R K D)

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleClass_principalDivisor (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : Additive Kˣ) : lineBundleClass R K ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).principalDivisor g) = 1

@[reducible, inline]

abbrev MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleModule (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : Type u

A chosen invertible-module representative of the affine line-bundle class O(D).

Equations

• MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleModule R K D = (MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleClass R K D).AsModule

@[simp]

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundleModule_picClass (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : CommRing.Pic.mk R (lineBundleModule R K D) = lineBundleClass R K D

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_lineBundleModule_add_equiv (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D E : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : Nonempty (lineBundleModule R K (D + E) ≃ₗ[R] TensorProduct R (lineBundleModule R K D) (lineBundleModule R K E))

The chosen affine line-bundle module carries divisor addition to tensor product, up to linear equivalence.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_lineBundleModule_equiv_iff_linearlyEquivalent (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D E : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : Nonempty (lineBundleModule R K D ≃ₗ[R] lineBundleModule R K E) ↔ (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).LinearlyEquivalent D E

Two chosen affine line-bundle modules are linearly equivalent exactly when the underlying divisors are linearly equivalent.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_lineBundleModule_principal_equiv (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : Additive Kˣ) : Nonempty (lineBundleModule R K ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).principalDivisor g) ≃ₗ[R] R)

A principal divisor has a trivial affine line-bundle module.

noncomputable def MazurTorsion.AlgebraicGeometry.AffineDedekind.lineBundle (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : TauCeti.AlgebraicGeometry.InvertibleSheaf (AlgebraicGeometry.Spec (CommRingCat.of R))

The line bundle O(D) on the affine Dedekind scheme.

Equations

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

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.divisorToSchemePic_val (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : ↑(Additive.toMul ((divisorToSchemePic R K) D)) = CategoryTheory.toSkeleton (lineBundle R K D).obj

The canonical scheme-Picard class of O(D) is represented by the actual tilde line bundle constructed above.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_lineBundle_add_iso (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D E : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : Nonempty ((lineBundle R K (D + E)).obj ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (lineBundle R K D).obj (lineBundle R K E).obj)

Divisor addition is carried to the actual sheaf tensor product by the chosen affine line bundles. This strengthens the module-level formula to a checked line-bundle isomorphism.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_lineBundle_principal_iso_trivial (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (g : Additive Kˣ) : Nonempty ((lineBundle R K ((TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).principalDivisor g)).obj ≅ (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial (AlgebraicGeometry.Spec (CommRingCat.of R))).obj)

The line bundle of a principal divisor is isomorphic to the trivial line bundle.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_lineBundle_iso_iff_linearlyEquivalent (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (D E : TauCeti.AlgebraicGeometry.WeilDivisor (IsDedekindDomain.HeightOneSpectrum R)) : Nonempty ((lineBundle R K D).obj ≅ (lineBundle R K E).obj) ↔ (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K).LinearlyEquivalent D E

Isomorphism of the chosen affine tilde line bundles detects linear equivalence exactly. The reverse implication uses full faithfulness of Mathlib's tilde functor.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_dictionary_iff_picardComparison_and_modulePicardEquivalence (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Nonempty (DivisorPicard.Dictionary (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K) (AlgebraicGeometry.Spec (CommRingCat.of R))) ↔ PicardComparison (AlgebraicGeometry.Spec (CommRingCat.of R)) ∧ Nonempty (Additive (CommRing.Pic R) ≃+ PicardGroup (AlgebraicGeometry.Spec (CommRingCat.of R)))

Rewriting the general dictionary boundary through the affine Dedekind class/module-Picard equivalence gives this abstract two-input form. The next theorem removes the second input: the reverse half of the full Picard comparison makes the canonical tilde map an equivalence.

theorem MazurTorsion.AlgebraicGeometry.AffineDedekind.nonempty_dictionary_iff_picardComparison (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] : Nonempty (DivisorPicard.Dictionary (TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.ofDedekindDomain R K) (AlgebraicGeometry.Spec (CommRingCat.of R))) ↔ PicardComparison (AlgebraicGeometry.Spec (CommRingCat.of R))

For an affine Dedekind scheme, the remaining exact dictionary boundary is just the full local-rank-one/tensor-unit comparison. Its reverse half makes the canonical tilde map surjective, so the divisor-class/Picard equivalence no longer needs to be supplied separately.