PicardUFD.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Picard triviality for the factorial affine charts

Algebraic support for bun:homotopy in §4 of the source. Over a GCD domain, all invertible modules are trivial; in particular this applies to the UFD localizations in the two charts and their polynomial extensions.

The statements below concern invertible modules, not just bijections of underlying sets. Invertible modules correspond to line bundles on an affine scheme.

theorem OAI.StableCoordinate.PicardSupport.invertibleModule_trivial_of_gcd line 26
Source documentation
An invertible module over a GCD domain admits a linear trivialization. There is no Noetherian hypothesis: Mathlib's class-group theorem is stronger than the particular source input.
```
theorem invertibleModule_trivial_of_gcd
    (A M : Type*) [CommRing A] [IsDomain A] [IsGCDMonoid A]
    [AddCommGroup M] [Module A M] [Module.Invertible A M] :
    Nonempty (M ≃ₗ[A] A) :=
…
```

theorem OAI.StableCoordinate.PicardSupport.invertibleModule_trivial_of_localization line 33

Source documentation

Triviality survives localization of a UFD at non-zero-divisors.

theorem invertibleModule_trivial_of_localization
    (A B M : Type*) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A]
    [CommRing B] [Algebra A B] (S : Submonoid A) [IsLocalization S B]
    (hS : S ≤ nonZeroDivisors A)
    [AddCommGroup M] [Module B M] [Module.Invertible B M] :
    Nonempty (M ≃ₗ[B] B) := by
…

theorem OAI.StableCoordinate.PicardSupport.invertibleModule_trivial_of_away line 45

Source documentation

In particular, every invertible module on a principal localization of a UFD at a nonzero element is trivial.

theorem invertibleModule_trivial_of_away
    (A B M : Type*) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A]
    [CommRing B] [Algebra A B] (a : A) [IsLocalization.Away a B] (ha : a ≠ 0)
    [AddCommGroup M] [Module B M] [Module.Invertible B M] :
    Nonempty (M ≃ₗ[B] B) :=
…

theorem OAI.StableCoordinate.PicardSupport.invertibleModule_polynomial_trivial line 55

Source documentation

The affine-line parameter used in the action-lift argument preserves triviality of invertible modules on a factorial affine chart.

theorem invertibleModule_polynomial_trivial
    (A M : Type*) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A]
    [AddCommGroup M] [Module (Polynomial A) M] [Module.Invertible (Polynomial A) M] :
    Nonempty (M ≃ₗ[(Polynomial A)] (Polynomial A)) :=
…

theorem OAI.StableCoordinate.PicardSupport.invertibleModule_away_polynomial_trivial line 62

Source documentation

Combined version for a principal affine chart and its affine-line extension.

theorem invertibleModule_away_polynomial_trivial
    (A B M : Type*) [CommRing A] [IsDomain A] [UniqueFactorizationMonoid A]
    [CommRing B] [Algebra A B] (a : A) [IsLocalization.Away a B] (ha : a ≠ 0)
    [AddCommGroup M] [Module (Polynomial B) M] [Module.Invertible (Polynomial B) M] :
    Nonempty (M ≃ₗ[(Polynomial B)] (Polynomial B)) := by
…