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