Standard etale maps

Main definitions

• StandardEtalePair: A pair f g : R[X] such that f is monic and f' is invertible in R[X][1/g].

• StandardEtalePair: The standard etale algebra corresponding to a StandardEtalePair.

• StandardEtalePair.equivPolynomialQuotient : P.Ring ≃ R[X][Y]/⟨f, Yg-1⟩

• StandardEtalePair.equivAwayAdjoinRoot : P.Ring ≃ (R[X]/f)[1/g]

• StandardEtalePair.equivAwayQuotient : P.Ring ≃ R[X][1/g]/f

• StandardEtalePair.equivMvPolynomialQuotient : P.Ring ≃ R[X, Y]/⟨f, Yg-1⟩

• StandardEtalePair.homEquiv: Maps out of P.Ring corresponds to x such that f(x) = 0 and g(x) is invertible.

• We also provide the instance that P.Ring is etale over R.

• Algebra.IsStandardEtale: The class of standard etale algebras.

structure StandardEtalePair (R : Type u_1) [CommRing R] : Type u_1

A StandardEtalePair R is a pair f g : R[X] such that f is monic, and f' is invertible in R[X][1/g]/f.

• f : Polynomial R

  The monic polynomial to be quotiented out in a standard etale algebra.

• monic_f : self.f.Monic
• g : Polynomial R

  The polynomial to be localized away from in a standard etale algebra.

• cond : ∃ (p₁ : Polynomial R) (p₂ : Polynomial R) (n : ℕ), Polynomial.derivative self.f * p₁ + self.f * p₂ = self.g ^ n

def StandardEtalePair.Ring {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : Type u_1

The standard etale algebra R[X][Y]/⟨f, Yg-1⟩ associated to a StandardEtalePair R. Also see equivPolynomialQuotient : P.Ring ≃ R[X][Y]/⟨f, Yg-1⟩ equivAwayAdjoinRoot : P.Ring ≃ (R[X]/f)[1/g] equivAwayQuotient : P.Ring ≃ R[X][1/g]/f equivMvPolynomialQuotient : P.Ring ≃ R[X, Y]/⟨f, Yg-1⟩

Equations

• P.Ring = (Polynomial (Polynomial R) ⧸ Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})

instance StandardEtalePair.instCommRingRing {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : CommRing P.Ring

Equations

• P.instCommRingRing = Ideal.Quotient.commRing (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})

instance StandardEtalePair.instAlgebraRing {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : Algebra R P.Ring

Equations

• P.instAlgebraRing = Ideal.instAlgebraQuotient R (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})

def StandardEtalePair.X {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.Ring

The X in the standard etale algebra R[X][Y]/⟨f, Yg-1⟩.

Equations

• P.X = (Ideal.Quotient.mk (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})) (Polynomial.C Polynomial.X)

def StandardEtalePair.HasMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (x : S) : Prop

There is a map from a standard etale algebra R[X][Y]/⟨f, Yg-1⟩ to S sending X to x iff f(x) = 0 and g(x) is invertible. Also see StandardEtalePair.homEquiv.

Equations

• P.HasMap x = ((Polynomial.aeval x) P.f = 0 ∧ IsUnit ((Polynomial.aeval x) P.g))

def StandardEtalePair.lift {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (x : S) (h : P.HasMap x) : P.Ring →ₐ[R] S

The map R[X][Y]/⟨f, Yg-1⟩ →ₐ[R] S sending X to x, given P.HasMap x.

Equations

• P.lift x h = Ideal.Quotient.liftₐ (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1}) (Polynomial.aevalAeval x ↑⋯.unit⁻¹) ⋯

@[simp]

theorem StandardEtalePair.lift_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (x : S) (h : P.HasMap x) : (P.lift x h) P.X = x

theorem StandardEtalePair.HasMap.map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {P : StandardEtalePair R} {x : S} (h : P.HasMap x) (f : S →ₐ[R] T) : P.HasMap (f x)

theorem StandardEtalePair.HasMap.isUnit_derivative_f {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) {x : S} (h : P.HasMap x) : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P.f))

theorem StandardEtalePair.aeval_X_g_mul_mk_X {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : (Polynomial.aeval P.X) P.g * (Ideal.Quotient.mk (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})) Polynomial.X = 1

theorem StandardEtalePair.hasMap_X {R : Type u_1} [CommRing R] {P : StandardEtalePair R} : P.HasMap P.X

theorem StandardEtalePair.hom_ext {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : StandardEtalePair R} {f g : P.Ring →ₐ[R] S} (H : f P.X = g P.X) : f = g

theorem StandardEtalePair.hom_ext_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : StandardEtalePair R} {f g : P.Ring →ₐ[R] S} : f = g ↔ f P.X = g P.X

@[simp]

theorem StandardEtalePair.lift_X_left {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.lift P.X ⋯ = AlgHom.id R P.Ring

theorem StandardEtalePair.inv_aeval_X_g {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : ↑⋯.unit⁻¹ = (Ideal.Quotient.mk (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1})) Polynomial.X

def StandardEtalePair.homEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) : (P.Ring →ₐ[R] S) ≃ { x : S // P.HasMap x }

Maps out of R[X][Y]/⟨f, Yg-1⟩ corresponds bijectively with x such that f(x) = 0 and g(x) is invertible.

Equations

• P.homEquiv = { toFun := fun (f : P.Ring →ₐ[R] S) => ⟨f P.X, ⋯⟩, invFun := fun (x : { x : S // P.HasMap x }) => P.lift ↑x ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem StandardEtalePair.homEquiv_apply_coe {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (f : P.Ring →ₐ[R] S) : ↑(P.homEquiv f) = f P.X

@[simp]

theorem StandardEtalePair.homEquiv_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (x : { x : S // P.HasMap x }) : P.homEquiv.symm x = P.lift ↑x ⋯

theorem StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePair R) (I : Ideal S) (hI : I ^ 2 = ⊥) (x : S) (hx : P.HasMap ((Ideal.Quotient.mk I) x)) : ∃! ε : S, ε ∈ I ∧ P.HasMap (x + ε)

instance StandardEtalePair.instFormallyEtaleRing {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : Algebra.FormallyEtale R P.Ring

instance StandardEtalePair.instEtaleRing {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : Algebra.Etale R P.Ring

def StandardEtalePair.equivPolynomialQuotient {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.Ring ≃ₐ[R] Polynomial (Polynomial R) ⧸ Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1}

An AlgEquiv between P.Ring and R[X][Y]/⟨f, Yg-1⟩, to not abuse the defeq between the two.

Equations

• P.equivPolynomialQuotient = AlgEquiv.refl

def StandardEtalePair.equivAwayAdjoinRoot {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.Ring ≃ₐ[R] Localization.Away ((AdjoinRoot.mk P.f) P.g)

R[X][Y]/⟨f, Yg-1⟩ ≃ (R[X]/f)[1/g]

Equations

• P.equivAwayAdjoinRoot = AlgEquiv.ofAlgHom (P.lift ((algebraMap (AdjoinRoot P.f) (Localization.Away ((AdjoinRoot.mk P.f) P.g))) (AdjoinRoot.root P.f)) ⋯) (IsLocalization.liftAlgHom ⋯) ⋯ ⋯

def StandardEtalePair.equivAwayQuotient {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.Ring ≃ₐ[R] Localization.Away P.g ⧸ Ideal.span {(algebraMap (Polynomial R) (Localization.Away P.g)) P.f}

R[X][Y]/⟨f, Yg-1⟩ ≃ R[X][1/g]/f

Equations

• One or more equations did not get rendered due to their size.

def StandardEtalePair.equivMvPolynomialQuotient {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.Ring ≃ₐ[R] MvPolynomial (Fin 2) R ⧸ Ideal.span {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f), (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}

R[X][Y]/⟨f, Yg-1⟩ ≃ R[X, Y]/⟨f, Yg-1⟩

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem StandardEtalePair.equivMvPolynomialQuotient_symm_apply {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : P.equivMvPolynomialQuotient.symm ((Ideal.Quotient.mk (Ideal.span {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f), (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)})) (MvPolynomial.X 0)) = P.X

structure StandardEtalePresentation (R : Type u_4) (S : Type u_5) [CommRing R] [CommRing S] [Algebra R S] extends StandardEtalePair R : Type (max u_4 u_5)

An isomorphism to the standard etale algebra of a standard etale pair.

• f : Polynomial R
• monic_f : self.f.Monic
• g : Polynomial R
• cond : ∃ (p₁ : Polynomial R) (p₂ : Polynomial R) (n : ℕ), Polynomial.derivative self.f * p₁ + self.f * p₂ = self.g ^ n
• x : S

  The image of X in a StandardEtalePresentation.

• hasMap : self.HasMap self.x
• lift_bijective : Function.Bijective ⇑(self.lift self.x ⋯)

def StandardEtalePresentation.equivRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : S ≃ₐ[R] P.Ring

The isomorphism to the standard etale algebra given a StandardEtalePresentation.

Equations

• P.equivRing = (AlgEquiv.ofBijective (P.lift P.x ⋯) ⋯).symm

@[simp]

theorem StandardEtalePresentation.equivRing_symm_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : P.equivRing.symm P.X = P.x

@[simp]

theorem StandardEtalePresentation.equivRing_x {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : P.equivRing P.x = P.X

def StandardEtalePresentation.toPresentation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : Algebra.Presentation R S (Fin 2) (Fin 2)

The Algebra.Presentation associated to a standard etale presentation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem StandardEtalePresentation.toPresentation_relation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (a✝ : Fin (Nat.succ 1)) : P.toPresentation.relation a✝ = ![(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f), (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.g) * MvPolynomial.X 1 - 1] a✝

@[simp]

theorem StandardEtalePresentation.toPresentation_σ' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (x : S) : P.toPresentation.σ' x = ⋯.choose

@[simp]

theorem StandardEtalePresentation.toPresentation_algebra_algebraMap_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (p : MvPolynomial (Fin 2) R) : Algebra.algebraMap p = MvPolynomial.eval₂ (algebraMap R S) ((⇑(P.lift P.x ⋯) ∘ ⇑P.equivMvPolynomialQuotient.symm ∘ ⇑(Ideal.Quotient.mk (Ideal.span {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f), (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}))) ∘ MvPolynomial.X) p

@[simp]

theorem StandardEtalePresentation.toPresentation_val {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (a✝ : Fin 2) : P.toPresentation.val a✝ = (P.lift P.x ⋯) (P.equivMvPolynomialQuotient.symm ((Ideal.Quotient.mk (Ideal.span {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f), (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)})) (MvPolynomial.X a✝)))

@[simp]

theorem StandardEtalePresentation.toPresentation_algebra_smul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (c : MvPolynomial (Fin 2) R) (x : S) : SMul.smul c x = (MvPolynomial.aeval ((⇑(P.lift P.x ⋯) ∘ ⇑P.equivMvPolynomialQuotient.symm ∘ ⇑(Ideal.Quotient.mk (Ideal.span {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f), (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)}))) ∘ MvPolynomial.X)) c * x

@[simp]

theorem StandardEtalePresentation.aeval_val_equivMvPolynomial {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (p : Polynomial R) : (MvPolynomial.aeval P.toPresentation.val) ((Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C p)) = (Polynomial.aeval P.x) p

def StandardEtalePresentation.toSubmersivePresentation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : Algebra.SubmersivePresentation R S (Fin 2) (Fin 2)

The Algebra.SubmersivePresentation associated to a standard etale presentation.

Equations

• P.toSubmersivePresentation = { toPresentation := P.toPresentation, map := id, map_inj := StandardEtalePresentation.toSubmersivePresentation._proof_2, jacobian_isUnit := ⋯ }

@[simp]

theorem StandardEtalePresentation.toSubmersivePresentation_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (a : Fin 2) : P.toSubmersivePresentation.map a = id a

@[simp]

theorem StandardEtalePresentation.toSubmersivePresentation_toPreSubmersivePresentation_toPresentation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : P.toSubmersivePresentation.toPresentation = P.toPresentation

theorem StandardEtalePresentation.toSubmersivePresentation_jacobian {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) : P.toSubmersivePresentation.jacobian = (Polynomial.aeval P.x) (Polynomial.derivative P.f) * (Polynomial.aeval P.x) P.g

theorem StandardEtalePresentation.exists_mul_aeval_x_g_pow_eq_aeval_x {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : StandardEtalePresentation R S) (x : S) : ∃ (p : Polynomial R) (n : ℕ), x * (Polynomial.aeval P.x) P.g ^ n = (Polynomial.aeval P.x) p

def StandardEtalePresentation.mapEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (P : StandardEtalePresentation R S) (e : S ≃ₐ[R] T) : StandardEtalePresentation R T

Mapping StandardEtalePresentation under AlgEquivs.

Equations

• P.mapEquiv e = { P := P.P, x := e P.x, hasMap := ⋯, lift_bijective := ⋯ }

class Algebra.IsStandardEtale (R : Type u_4) (S : Type u_5) [CommRing R] [CommRing S] [Algebra R S] : Prop

The class of standard etale algebras, defined to be the existence of a StandardEtalePresentation.

• nonempty_standardEtalePresentation : Nonempty (StandardEtalePresentation R S)

instance Algebra.instIsStandardEtaleRing {R : Type u_1} [CommRing R] (P : StandardEtalePair R) : IsStandardEtale R P.Ring

@[instance 100]

instance Algebra.instEtaleOfIsStandardEtale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsStandardEtale R S] : Etale R S

theorem Algebra.IsStandardEtale.of_equiv {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] (e : S ≃ₐ[R] T) [IsStandardEtale R S] : IsStandardEtale R T

instance Algebra.instIsStandardEtale {R : Type u_1} [CommRing R] : IsStandardEtale R R

theorem Algebra.IsStandardEtale.of_isLocalizationAway {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsStandardEtale R S] {Sₛ : Type u_4} [CommRing Sₛ] [Algebra S Sₛ] [Algebra R Sₛ] [IsScalarTower R S Sₛ] (s : S) [IsLocalization.Away s Sₛ] : IsStandardEtale R Sₛ

theorem Algebra.IsStandardEtale.of_surjective (R : Type u_4) (S : Type u_5) (T : Type u_6) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [IsStandardEtale R S] [Etale R T] (f : S →ₐ[R] T) (hf : Function.Surjective ⇑f) : IsStandardEtale R T

If T is an etale algebra, and a standard etale algebra surjects onto T, then T is also standard etale.