Module

AlgEquivZeroGroupCut.lean

Nyll.AlgebraicCurves.Geometry.Picard.AlgEquivZeroGroupCut

7 declarations indexed from sourceView source ↗

Module documentation

The group structure on algebraically trivial invertible modules

Algebraically trivial invertible modules are closed under tensor products, inverses and pullback, giving the associated sub-Picard group condition.

Imports8

Imported by70

theorem

fst_comp_of_field

L39 ↗

AlgebraicGeometry.GeometricallyIntegral.fst_comp_of_field

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry

Lean source · statement

theorem GeometricallyIntegral.fst_comp_of_field {k : Type u} [Field k] {T₁ T₂ : Scheme.{u}}
    (h₁ : T₁ ⟶ Spec (CommRingCat.of k)) (h₂ : T₂ ⟶ Spec (CommRingCat.of k))
    [GeometricallyIntegral h₁] [LocallyOfFiniteType h₁] [GeometricallyIntegral h₂]
        [LocallyOfFiniteType h₂] :
    GeometricallyIntegral (pullback.fst h₁ h₂ ≫ h₁)

theorem

tensor

L59 ↗

AlgebraicGeometry.RelPicard.IsAlgEquivZero.tensor

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard

Lean source · statement

theorem IsAlgEquivZero.tensor {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec
    (CommRingCat.of k)}
    {L M : A.Modules} (hL : IsAlgEquivZero a L) (hM : IsAlgEquivZero a M) : IsAlgEquivZero a (L
        ⊗ M)

theorem

of_tensor_iso_unit

L108 ↗

AlgebraicGeometry.RelPicard.IsAlgEquivZero.of_tensor_iso_unit

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard

Lean source · statement

theorem IsAlgEquivZero.of_tensor_iso_unit {k : Type u} [Field k] {A : Scheme.{u}} {a : A ⟶ Spec
    (CommRingCat.of k)}
    {L M : A.Modules} (hL : IsAlgEquivZero a L) (e : L ⊗ M ≅ 𝟙_ A.Modules) : IsAlgEquivZero a M

theorem

tensor

L138 ↗

AlgebraicGeometry.RelPicard.FibrewiseAlgEquivZero.tensor

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

theorem FibrewiseAlgEquivZero.tensor {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {L M : RigidifiedLineBundle c ε t} (hL : FibrewiseAlgEquivZero L) (hM :
        FibrewiseAlgEquivZero M) :
    FibrewiseAlgEquivZero (L.tensor M)

theorem

of_tensor_iso_unit

L146 ↗

AlgebraicGeometry.RelPicard.FibrewiseAlgEquivZero.of_tensor_iso_unit

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry.RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c}

Lean source · statement

theorem FibrewiseAlgEquivZero.of_tensor_iso_unit {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {L M : RigidifiedLineBundle c ε t}
    (e : Nonempty ((L.tensor M).L ≅ (RigidifiedLineBundle.unit (c := c) (ε := ε) t).L))
    (hL : FibrewiseAlgEquivZero L) : FibrewiseAlgEquivZero M

def