RingTheory.Sequence.IsWeaklyRegular is stable under flat base change #
Main results #
RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange: LetRbe a commutative ring,Mbe anR-module,Sbe a flatR-algebra,Nbe the base change ofMtoS. If[r₁, …, rₙ]is a weakly regularM-sequence, then its image inNis a weakly regularN-sequence.
theorem
RingTheory.Sequence.IsWeaklyRegular.of_flat_of_isBaseChange
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
[Module.Flat R S]
{f : M →ₗ[R] N}
(hf : IsBaseChange S f)
{rs : List R}
(reg : IsWeaklyRegular M rs)
:
IsWeaklyRegular N (List.map (⇑(algebraMap R S)) rs)
Let R be a commutative ring, M be an R-module, S be a flat R-algebra, N be the base
change of M to S. If [r₁, …, rₙ] is a weakly regular M-sequence, then its image in N is
a weakly regular N-sequence.
theorem
RingTheory.Sequence.IsWeaklyRegular.of_flat
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[Module.Flat R S]
{rs : List R}
(reg : IsWeaklyRegular R rs)
:
IsWeaklyRegular S (List.map (⇑(algebraMap R S)) rs)
theorem
RingTheory.Sequence.IsWeaklyRegular.of_isLocalizedModule
{R : Type u_1}
(S : Type u_2)
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
(T : Submonoid R)
[IsLocalization T S]
(f : M →ₗ[R] N)
[IsLocalizedModule T f]
{rs : List R}
(reg : IsWeaklyRegular M rs)
:
IsWeaklyRegular N (List.map (⇑(algebraMap R S)) rs)
theorem
RingTheory.Sequence.IsWeaklyRegular.of_isLocalization
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(T : Submonoid R)
[IsLocalization T S]
{rs : List R}
(reg : IsWeaklyRegular R rs)
:
IsWeaklyRegular S (List.map (⇑(algebraMap R S)) rs)
theorem
RingTheory.Sequence.IsWeaklyRegular.isRegular_of_isLocalizedModule_of_mem
{R : Type u_1}
(S : Type u_2)
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
(p : Ideal R)
[p.IsPrime]
[IsLocalization.AtPrime S p]
[Nontrivial N]
[Module.Finite S N]
(f : M →ₗ[R] N)
[IsLocalizedModule.AtPrime p f]
{rs : List R}
(reg : IsWeaklyRegular M rs)
(mem : ∀ r ∈ rs, r ∈ p)
:
IsRegular N (List.map (⇑(algebraMap R S)) rs)
theorem
RingTheory.Sequence.IsWeaklyRegular.isRegular_of_isLocalization_of_mem
{R : Type u_1}
(S : Type u_2)
[CommRing R]
[CommRing S]
[Algebra R S]
(p : Ideal R)
[p.IsPrime]
[IsLocalization.AtPrime S p]
{rs : List R}
(reg : IsWeaklyRegular R rs)
(mem : ∀ r ∈ rs, r ∈ p)
:
IsRegular S (List.map (⇑(algebraMap R S)) rs)
theorem
RingTheory.Sequence.IsRegular.of_faithfullyFlat_of_isBaseChange
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
[CommRing R]
[CommRing S]
[Algebra R S]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
[Module.FaithfullyFlat R S]
{f : M →ₗ[R] N}
(hf : IsBaseChange S f)
{rs : List R}
(reg : IsRegular M rs)
:
IsRegular N (List.map (⇑(algebraMap R S)) rs)
Let R be a commutative ring, M be an R-module, S be a faithfully flat R-algebra,
N be the base change of M to S. If [r₁, …, rₙ] is a regular M-sequence, then its image
in N is a regular N-sequence.
theorem
RingTheory.Sequence.IsRegular.of_faithfullyFlat
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[Module.FaithfullyFlat R S]
{rs : List R}
(reg : IsRegular R rs)
:
IsRegular S (List.map (⇑(algebraMap R S)) rs)