EtaleFundamentalGroups.strictHenselianChosenFactorFractionFieldAlgEquiv_universe
The fraction field of the uniquely chosen finite etale factor over a strictly Henselian base is canonically the fraction field of the base.
The target Froot-algebra is the one already present on P; the two scalar tower assumptions say precisely that its restrictions are the canonical maps through B and through the chosen factor D.
Source context 15 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups
universe uB uD uF uP
variable {B : Type uB} {D : Type uD}
variable {Froot : Type uF} {P : Type uP}
variable [CommRing B] [CommRing D]
variable [Field Froot] [Field P]
variable [Algebra B D]
variable [Algebra B Froot] [IsFractionRing B Froot]
variable [Algebra D P] [IsFractionRing D P]
variable [Algebra B P] [IsScalarTower B D P]
variable [Algebra Froot P] [IsScalarTower B Froot P]
variable [HenselianLocalRing B]
variable [Module.Finite B D] [Algebra.Etale B D]
variable [IsSepClosed (IsLocalRing.ResidueField B)]Lean source · statement
def strictHenselianChosenFactorFractionFieldAlgEquiv_universe
(q : Ideal D) [q.IsPrime]
[q.LiesOver (IsLocalRing.maximalIdeal B)]
(hunique : ∀ Q : Ideal D, Q.IsPrime →
Q.LiesOver (IsLocalRing.maximalIdeal B) → Q = q) :
Froot ≃ₐ[Froot] P