Module

RingHom_QuasiFinite_codescendsAlong_faithfullyFlat.lean

Nyll.AlgebraicCurves.Foundations.Algebra.RingHom_QuasiFinite_codescendsAlong_faithfullyFlat

3 declarations indexed from sourceView source ↗

Module documentation

Ring Hom Quasi Finite codescends Along faithfully Flat

Imports2

Mathlib.RingTheory.Finiteness.Descent
Mathlib.RingTheory.RingHom.QuasiFinite

Imported by2

theorem

of_quasiFinite_tensorProduct_of_faithfullyFlat

L31 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.RingHom_QuasiFinite_codescendsAlong_faithfullyFlat.QFDescent.of_quasiFinite_tensorProduct_of_faithfullyFlat

Source context 6 commands

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

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

Lean source · statement

theorem of_quasiFinite_tensorProduct_of_faithfullyFlat
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] (T : Type*) [CommRing T] [Algebra R T]
    [Module.FaithfullyFlat R T] [Algebra.QuasiFinite T (T ⊗[R] S)] : Algebra.QuasiFinite R S

theorem

codescendsAlong_faithfullyFlat'

L55 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.RingHom_QuasiFinite_codescendsAlong_faithfullyFlat.codescendsAlong_faithfullyFlat'

Source context 5 commands

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

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

Lean source · statement

theorem codescendsAlong_faithfullyFlat' :
    RingHom.CodescendsAlong RingHom.QuasiFinite RingHom.FaithfullyFlat

theorem

codescendsAlong_faithfullyFlat

L62 ↗

RingHom.QuasiFinite.codescendsAlong_faithfullyFlat

Source context 5 commands

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

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

Lean source · full declaration

theorem _root_.RingHom.QuasiFinite.codescendsAlong_faithfullyFlat :
    RingHom.CodescendsAlong (fun {R S : Type u} [CommRing R] [CommRing S] => @RingHom.QuasiFinite R
      S _ _)
      (fun {R S : Type u} [CommRing R] [CommRing S] => @RingHom.FaithfullyFlat R S _ _) :=
  codescendsAlong_faithfullyFlat'

Module documentation

Ring Hom Quasi Finite codescends Along faithfully Flat

Declarations

of_quasiFinite_tensorProduct_of_faithfullyFlat

codescendsAlong_faithfullyFlat'

codescendsAlong_faithfullyFlat