NYLL
Module

Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
3 declarations indexed from sourceView source ↗

Module documentation

Module exists forall is Unit surjective base Change of surjective base Change residue

Field

Imports4
Imported by1

Declarations

theorem

lTensor_surjective_of_subsingleton

L37 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField.K4FSurjSpread.lTensor_surjective_of_subsingleton
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
universe u
open TensorProduct
namespace K4FSurjSpread
variable {R : Type u} [CommRing R] {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N]
  [Module R N]
Lean source · statement
theorem lTensor_surjective_of_subsingleton (f : M →ₗ[R] N) (A : Type u) [AddCommGroup A] [Module R
  A]
    (h : Subsingleton (A ⊗[R] (N ⧸ LinearMap.range f))) : Function.Surjective (f.lTensor A)
theorem

subsingleton_tensor_of_smul_eq_zero

L45 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField.K4FSurjSpread.subsingleton_tensor_of_smul_eq_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
universe u
open TensorProduct
namespace K4FSurjSpread
variable {R : Type u} [CommRing R] {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N]
  [Module R N]
Lean source · statement
theorem subsingleton_tensor_of_smul_eq_zero (Q : Type u) [AddCommGroup Q] [Module R Q] (g : R)
    (hg : ∀ q : Q, g • q = 0) (A : Type u) [CommRing A] [Algebra R A] (hu : IsUnit (algebraMap R A
      g)) :
    Subsingleton (A ⊗[R] Q)
theorem

exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField

L63 ↗
Module.exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
universe u
open TensorProduct
open K4FSurjSpread in
Lean source · statement
theorem
  _root_.Module.exists_forall_isUnit_surjective_baseChange_of_surjective_baseChange_residueField
    {R : Type u} [CommRing R]
    {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module.Finite R N]
    (f : M →ₗ[R] N) (𝔭 : PrimeSpectrum R)
    (hf : Function.Surjective (f.baseChange 𝔭.asIdeal.ResidueField)) :
    ∃ g : R, g ∉ 𝔭.asIdeal ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A], IsUnit (algebraMap R A g) →
        Function.Surjective (f.baseChange A)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.