ModuleRingCover.lean
Nyll.SchemeTheory.FiniteEtale.RingCover
3 declarations indexed from sourceView source ↗ Module documentation
Field Arithmetic, Definition 7.1.3: ring covers
The book's condition S = R[z] is recorded by the existence of a power basis. The Galois condition is stated for the induced extension of fraction fields.
Imports4
- Mathlib.FieldTheory.Galois.Basic
- Mathlib.RingTheory.Discriminant
- Mathlib.RingTheory.Localization.FractionRing
- Mathlib.RingTheory.PowerBasis
Imported by1
Declarations
FieldArithmetic.Chapter07.IsRingCover
DocumentationThe algebraic part of the ring-cover condition in Fried--Jarden, Definition 7.1.3. The ambient hypotheses that R and S are integrally closed domains are supplied where this predicate is used.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace FieldArithmetic
namespace Chapter07
universe u v
variable (R : Type u) (S : Type v)
variable [CommRing R] [CommRing S]
variable [Algebra R S]
FieldArithmetic.Chapter07.FractionExtensionIsGalois
DocumentationThe extension of fraction fields induced by R → S is Galois.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace FieldArithmetic
namespace Chapter07
universe u v
variable (R : Type u) (S : Type v)
variable [CommRing R] [CommRing S]
variable [Algebra R S]
FieldArithmetic.Chapter07.IsGaloisRingCover
DocumentationThe algebraic part of the Galois ring-cover condition in Definition 7.1.3.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace FieldArithmetic
namespace Chapter07
universe u v
variable (R : Type u) (S : Type v)
variable [CommRing R] [CommRing S]
variable [Algebra R S]