Module

Module_finrank_baseChange_eq_one_of_rankAtStalk_eq_one.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_finrank_baseChange_eq_one_of_rankAtStalk_eq_one

1 declaration indexed from sourceView source ↗

Module documentation

One-dimensional fibers after base change

Transfers rank one at every prime to dimension one over a field algebra.

Imports2

Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.LinearAlgebra.Dimension.Constructions

Imported by2

theorem

finrank_baseChange_eq_one_of_rankAtStalk_eq_one

L32 ↗

Module.finrank_baseChange_eq_one_of_rankAtStalk_eq_one

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_finrank_baseChange_eq_one_of_rankAtStalk_eq_one
universe u
open TensorProduct

Lean source · statement

theorem _root_.Module.finrank_baseChange_eq_one_of_rankAtStalk_eq_one
    {R : Type u} [CommRing R] (P : Type u) [AddCommGroup P] [Module R P]
    [Module.Finite R P] [Module.Flat R P]
    (h : ∀ 𝔭, Module.rankAtStalk (R := R) P 𝔭 = 1)
    (K : Type u) [Field K] [Algebra R K] :
    Module.finrank K (K ⊗[R] P) = 1

Module documentation

One-dimensional fibers after base change

Declarations

finrank_baseChange_eq_one_of_rankAtStalk_eq_one