Properties satisfying faithfully flat descent for rings #
We show the following properties of ring homomorphisms descend under faithfully flat ring maps:
- injective
- surjective
- bijective
theorem
Module.FaithfullyFlat.injective_of_tensorProduct
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
{T : Type u_3}
[CommRing T]
[Algebra R T]
[FaithfullyFlat R S]
(H : Function.Injective ⇑(algebraMap S (TensorProduct R S T)))
:
Function.Injective ⇑(algebraMap R T)
theorem
Module.FaithfullyFlat.surjective_of_tensorProduct
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
{T : Type u_3}
[CommRing T]
[Algebra R T]
[FaithfullyFlat R S]
(H : Function.Surjective ⇑(algebraMap S (TensorProduct R S T)))
:
Function.Surjective ⇑(algebraMap R T)
theorem
Module.FaithfullyFlat.bijective_of_tensorProduct
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
{T : Type u_3}
[CommRing T]
[Algebra R T]
[FaithfullyFlat R S]
(H : Function.Bijective ⇑(algebraMap S (TensorProduct R S T)))
:
Function.Bijective ⇑(algebraMap R T)
theorem
RingHom.FaithfullyFlat.codescendsAlong_injective :
CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Injective ⇑f)
fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat
theorem
RingHom.FaithfullyFlat.codescendsAlong_surjective :
CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Surjective ⇑f)
fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat
theorem
RingHom.FaithfullyFlat.codescendsAlong_bijective :
CodescendsAlong (fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f)
fun {R S : Type u_1} [CommRing R] [CommRing S] => FaithfullyFlat