NYLL
Module

ChosenFactorUniverse.lean

Nyll.SchemeTheory.FiniteEtale.Henselian.ChosenFactorUniverse
3 declarations indexed from sourceView source ↗

Module documentation

A uniquely chosen finite etale factor in a separate universe

The strict-Henselian chosen-factor argument does not depend on the base and factor carriers living in the same universe. This file records the universe-polymorphic form needed when the factor is a localization of an integral closure in a generic tensor component.

Imports1
Imported by2

Declarations

theorem

algebraMap_bijective_of_henselian_of_isSepClosed_residue_of_finiteEtale_local_universe

L28 ↗
EtaleFundamentalGroups.algebraMap_bijective_of_henselian_of_isSepClosed_residue_of_finiteEtale_local_universe
Documentation

A finite etale local algebra over a Henselian local ring with separably closed residue field is the base, with independent carrier universes.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe uR uS
Lean source · statement
theorem
    algebraMap_bijective_of_henselian_of_isSepClosed_residue_of_finiteEtale_local_universe
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [IsLocalRing S]
    [Module.Finite R S] [FaithfulSMul R S] [Algebra.Etale R S]
    [IsSepClosed (IsLocalRing.ResidueField R)] :
    Function.Bijective (algebraMap R S)
theorem

algebraMap_bijective_of_unique_prime_over_maximal_of_strictHenselian_universe

L131 ↗
EtaleFundamentalGroups.algebraMap_bijective_of_unique_prime_over_maximal_of_strictHenselian_universe
Documentation

A finite etale algebra with a unique prime over the closed point of a strictly Henselian local ring is the base, with independent carrier universes.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe uR uS
Lean source · statement
theorem
    algebraMap_bijective_of_unique_prime_over_maximal_of_strictHenselian_universe
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Module.Finite R S] [Algebra.Etale R S]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    Function.Bijective (algebraMap R S)
def

strictHenselianChosenFactorAlgEquiv_universe

L176 ↗
EtaleFundamentalGroups.strictHenselianChosenFactorAlgEquiv_universe
Documentation

The explicit strict-Henselian chosen-factor equivalence with independent base and factor universes.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Polynomial
universe uR uS
Lean source · statement
def strictHenselianChosenFactorAlgEquiv_universe
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [HenselianLocalRing R] [Module.Finite R S] [Algebra.Etale R S]
    [IsSepClosed (IsLocalRing.ResidueField R)]
    (q : Ideal S) [q.IsPrime]
    [q.LiesOver (IsLocalRing.maximalIdeal R)]
    (hunique : ∀ Q : Ideal S, Q.IsPrime →
      Q.LiesOver (IsLocalRing.maximalIdeal R) → Q = q) :
    R ≃ₐ[R] S

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