Module

ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field

4 declarations indexed from sourceView source ↗

Module documentation

Proj Space subsingleton HSucc twist of subsingleton HSucc twist base Change field

Imports9

Mathlib.LinearAlgebra.Basis.VectorSpace
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.RingTheory.MvPolynomial.Homogeneous
Mathlib.AlgebraicGeometry.Morphisms.Affine
Nyll.SchemeTheory.ProjectiveSpace.Basic
Nyll.SchemeTheory.ProjectiveSpace.Cover
Nyll.AlgebraicCurves.Geometry.Projective.ProjTwistDatum
Nyll.AlgebraicCurves.Cohomology.Sheaves.ProjSpace_exists_linearEquiv_baseChange_cochain_twist_of_isPullback

Imported by1

Nyll.AlgebraicCurves.Geometry.Projective.All

theorem

eq_zero_of_one_tmul_eq_zero

L45 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field.RM6aSol.eq_zero_of_one_tmul_eq_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace RM6aSol
section LinAlg
variable {k : Type u} [Field k] (K : Type u) [Field K] [Algebra k K] {V : Type u} [AddCommGroup V]
  [Module k V]

Lean source · statement

theorem eq_zero_of_one_tmul_eq_zero (v : V) (h : (1 : K) ⊗ₜ[k] v = 0) : v = 0

theorem

mem_of_one_tmul_mem_baseChange

L56 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field.RM6aSol.mem_of_one_tmul_mem_baseChange

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace RM6aSol
section LinAlg
variable {k : Type u} [Field k] (K : Type u) [Field K] [Algebra k K] {V : Type u} [AddCommGroup V]
  [Module k V]

Lean source · statement

theorem mem_of_one_tmul_mem_baseChange (W : Submodule k V) (v : V)
    (h : (1 : K) ⊗ₜ[k] v ∈ W.baseChange K) : v ∈ W

theorem

range_baseChange_le

L81 ↗

AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field.RM6aSol.range_baseChange_le

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace RM6aSol
variable {R : Type u} [CommRing R] (A : Type u) [CommRing A] [Algebra R A]
  {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]

Lean source · statement

theorem range_baseChange_le (f : M →ₗ[R] N) :
    LinearMap.range (f.baseChange A) ≤ (LinearMap.range f).baseChange A

theorem

subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field

L105 ↗

AlgebraicGeometry.ProjSpace.subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry
universe u
open CategoryTheory CategoryTheory.Limits MvPolynomial TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Projective.Proofs in
open ProjSpace_subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field in

Lean source · statement

theorem ProjSpace.subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field
    {k : Type u} [Field k] {n : ℕ} {Z : Scheme.{u}}
    (ι : Z ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) [IsAffineHom ι]
    (K : Type u) [Field K] [Algebra k K] {Z' : Scheme.{u}}
    (ι' : Z' ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) K)) [IsAffineHom ι']
    (e : Z' ⟶ Z)
    (hpb : IsPullback e (ι' ≫ ProjSpace.π K n) (ι ≫ ProjSpace.π k n) (Spec.map (CommRingCat.ofHom
      (algebraMap k K))))
    (hcomp : e ≫ ι = ι' ≫ ProjSpace.map k K n) (d i : ℕ)
    (hK : Subsingleton ((ProjSpace.twist (ι' ≫ ProjSpace.π K n) ι' d).HSucc
      (ProjSpace.stdCoverPullback ι') i)) :
    Subsingleton ((ProjSpace.twist (ι ≫ ProjSpace.π k n) ι d).HSucc (ProjSpace.stdCoverPullback ι)
      i)

Module documentation

Proj Space subsingleton HSucc twist of subsingleton HSucc twist base Change field

Declarations

eq_zero_of_one_tmul_eq_zero

mem_of_one_tmul_mem_baseChange

range_baseChange_le

subsingleton_HSucc_twist_of_subsingleton_HSucc_twist_baseChange_field