NYLL
Module

FaithfullyFlatNormality.lean

Nyll.SchemeTheory.RingTheory.Descent.FaithfullyFlatNormality
1 declaration indexed from sourceView source ↗

Module documentation

Faithfully flat descent of integral closure

An integral domain is integrally closed when a faithfully flat domain extension is integrally closed. The proof descends an integral element through the original algebra map.

Imports3
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.Tactic.Ring.RingNF
Imported by1

Declarations

theorem

of_faithfullyFlat

L29 ↗
IsIntegrallyClosed.of_faithfullyFlat
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsIntegrallyClosed_of_faithfullyFlat
Lean source · statement
theorem _root_.IsIntegrallyClosed.of_faithfullyFlat (A B : Type*)
    [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
    [Algebra A B] [Module.FaithfullyFlat A B] [IsIntegrallyClosed B] : IsIntegrallyClosed A

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.