A finite flat module M is locally free if rankAtStalk M is constant #
theorem
Module.bijective_of_surjective_of_rankAtStalk_eq
{R : Type u_1}
[CommRing R]
{M : Type u_2}
{N : Type u_3}
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
[Flat R M]
[AddCommGroup N]
[Module R N]
[Module.Finite R N]
[Flat R N]
{φ : M →ₗ[R] N}
(hs : Function.Surjective ⇑φ)
(h :
∀ (m : Ideal R) [inst : m.IsMaximal],
rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk N { asIdeal := m, isPrime := ⋯ })
:
theorem
Module.Free.away_of_finite_of_flat_of_rankAtStalk_constant
{R : Type u_1}
[CommRing R]
(M : Type u_2)
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
[Flat R M]
(p : Ideal R)
[p.IsPrime]
(h :
∀ (m : Ideal R) [inst : m.IsMaximal],
rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ })
:
∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)
Let M be a finite flat R-module, p be a prime ideal of R. If rankAtStalk M is
constant, then there exists a ∉ p such that M is free after localization away from a.