Frobenius elements.

This file proves a general result in commutative algebra which can be used to define Frobenius elements of Galois groups of local or fields (for example number fields).

KB was alerted to this very general result (which needs no Noetherian or finiteness assumptions on the rings, just on the Galois group) by Joel Riou here https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Uses.20of.20Frobenius.20elements.20in.20mathematics/near/448934112

Mathematical details

The general commutative algebra result

This is Theorem 2 in Chapter V, Section 2, number 2 of Bourbaki Alg Comm. It says the following. Let A → B be commutative rings and let G be a finite group acting on B by ring automorphisms, such that the G-invariants of B are exactly the image of A.

The two claims of the theorem are: (i) If P is a prime ideal of A then G acts transitively on the primes of B above P. (ii) If Q is a prime ideal of B lying over P then the canonica map from the stabilizer of Q in G to the automorphism group of the residue field extension Frac(B/Q) / Frac(A/P) is surjective.

We say "automorphism group" rather than "Galois group" because the extension might not be separable (it is algebraic and normal however, but it can be infinite; however its maximal separable subextension is finite).

This result means that if the inertia group I_Q is trivial and the residue fields are finite, there's a Frobenius element Frob_Q in the stabiliser of Q, and a Frobenius conjugacy class Frob_P in G.

theorem Ideal.IsPrime.finprod_mem_iff_exists_mem {R : Type u_7} {S : Type u_8} [Finite R] [CommSemiring S] (I : Ideal S) [hI : I.IsPrime] (f : R → S) : ∏ᶠ (x : R), f x ∈ I ↔ ∃ (p : R), f p ∈ I

noncomputable def MulSemiringAction.CharacteristicPolynomial.F {B : Type u_5} [CommRing B] (G : Type u_6) [Group G] [MulSemiringAction G B] (b : B) : Polynomial B

The characteristic polynomial of an element b of a G-semiring B is the polynomial ∏_{g ∈ G} (X - g • b) (here G is finite; junk returned in the infinite case) .

Equations

• MulSemiringAction.CharacteristicPolynomial.F G b = ∏ᶠ (τ : G), (Polynomial.X - Polynomial.C (τ • b))

theorem MulSemiringAction.CharacteristicPolynomial.F_spec {B : Type u_5} [CommRing B] {G : Type u_6} [Group G] [MulSemiringAction G B] (b : B) : MulSemiringAction.CharacteristicPolynomial.F G b = ∏ᶠ (τ : G), (Polynomial.X - Polynomial.C (τ • b))

theorem MulSemiringAction.CharacteristicPolynomial.F_monic {B : Type u_5} [CommRing B] {G : Type u_6} [Group G] [MulSemiringAction G B] [Finite G] [Nontrivial B] (b : B) : (MulSemiringAction.CharacteristicPolynomial.F G b).Monic

theorem MulSemiringAction.CharacteristicPolynomial.F_natdegree {B : Type u_5} [CommRing B] {G : Type u_6} [Group G] [MulSemiringAction G B] [Finite G] [Nontrivial B] (b : B) : (MulSemiringAction.CharacteristicPolynomial.F G b).natDegree = Nat.card G

theorem MulSemiringAction.CharacteristicPolynomial.F_degree {B : Type u_5} [CommRing B] (G : Type u_6) [Group G] [MulSemiringAction G B] [Finite G] [Nontrivial B] (b : B) : (MulSemiringAction.CharacteristicPolynomial.F G b).degree = ↑(Nat.card G)

theorem MulSemiringAction.CharacteristicPolynomial.F_smul_eq_self {B : Type u_5} [CommRing B] {G : Type u_6} [Group G] [MulSemiringAction G B] [Finite G] (σ : G) (b : B) : σ • MulSemiringAction.CharacteristicPolynomial.F G b = MulSemiringAction.CharacteristicPolynomial.F G b

theorem MulSemiringAction.CharacteristicPolynomial.F_eval_eq_zero {B : Type u_5} [CommRing B] {G : Type u_6} [Group G] [MulSemiringAction G B] [Finite G] (b : B) : Polynomial.eval b (MulSemiringAction.CharacteristicPolynomial.F G b) = 0

noncomputable def MulSemiringAction.CharacteristicPolynomial.instAlgebraPolynomial_fLT {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] : Algebra (Polynomial A) (Polynomial B)

Equations

• MulSemiringAction.CharacteristicPolynomial.instAlgebraPolynomial_fLT = (Polynomial.mapRingHom Algebra.toRingHom).toAlgebra

@[simp]

theorem coe_monomial {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] (n : ℕ) (a : A) : ↑((Polynomial.monomial n) a) = (Polynomial.monomial n) ↑a

noncomputable def MulSemiringAction.CharacteristicPolynomial.splitting_of_full {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) (b : B) : A

This "splitting" function from B to A will only ever be evaluated on G-invariant elements of B, and the two key facts about it are that it lifts such an element to A, and for reasons of convenience it lifts 1 to 1.

Equations

• MulSemiringAction.CharacteristicPolynomial.splitting_of_full hFull b = if b = 1 then 1 else if h : ∀ (σ : G), σ • b = b then ⋯.choose else 37

theorem MulSemiringAction.CharacteristicPolynomial.splitting_of_full_spec {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) {b : B} (hb : ∀ (σ : G), σ • b = b) : ↑(MulSemiringAction.CharacteristicPolynomial.splitting_of_full hFull b) = b

theorem MulSemiringAction.CharacteristicPolynomial.splitting_of_full_one {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) : MulSemiringAction.CharacteristicPolynomial.splitting_of_full hFull 1 = 1

noncomputable def MulSemiringAction.CharacteristicPolynomial.M {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) (b : B) : Polynomial A

Equations

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

theorem MulSemiringAction.CharacteristicPolynomial.M_deg_le {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) (b : B) : (MulSemiringAction.CharacteristicPolynomial.M hFull b).degree ≤ (MulSemiringAction.CharacteristicPolynomial.F G b).degree

theorem MulSemiringAction.CharacteristicPolynomial.M_coeff_card {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial B] [Finite G] (b : B) : (MulSemiringAction.CharacteristicPolynomial.M hFull b).coeff (Nat.card G) = 1

theorem MulSemiringAction.CharacteristicPolynomial.M_deg_eq_F_deg {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial B] [Finite G] [Nontrivial A] (b : B) : (MulSemiringAction.CharacteristicPolynomial.M hFull b).degree = (MulSemiringAction.CharacteristicPolynomial.F G b).degree

theorem MulSemiringAction.CharacteristicPolynomial.M_deg {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial B] [Finite G] [Nontrivial A] (b : B) : (MulSemiringAction.CharacteristicPolynomial.M hFull b).degree = ↑(Nat.card G)

theorem MulSemiringAction.CharacteristicPolynomial.M_monic {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial B] [Finite G] (b : B) : (MulSemiringAction.CharacteristicPolynomial.M hFull b).Monic

theorem MulSemiringAction.CharacteristicPolynomial.M_spec {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Finite G] (b : B) : ↑(MulSemiringAction.CharacteristicPolynomial.M hFull b) = MulSemiringAction.CharacteristicPolynomial.F G b

theorem MulSemiringAction.CharacteristicPolynomial.M_spec_map {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Finite G] (b : B) : Polynomial.map (algebraMap A B) (MulSemiringAction.CharacteristicPolynomial.M hFull b) = MulSemiringAction.CharacteristicPolynomial.F G b

theorem MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Finite G] (b : B) : Polynomial.eval₂ (algebraMap A B) b (MulSemiringAction.CharacteristicPolynomial.M hFull b) = 0

theorem MulSemiringAction.CharacteristicPolynomial.isIntegral {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial B] [Finite G] : Algebra.IsIntegral A B

theorem isIntegral_of_Full {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] [Nontrivial B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) : Algebra.IsIntegral A B

theorem Nontrivial_of_exists_prime {R : Type u_7} [CommRing R] (h : ∃ (P : Ideal R), P.IsPrime) : Nontrivial R

theorem part_a {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] (P : Ideal B) (Q : Ideal B) [P.IsPrime] [Q.IsPrime] [SMulCommClass G A B] (hPQ : Ideal.comap (algebraMap A B) P = Ideal.comap (algebraMap A B) Q) (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) : ∃ (g : G), Q = g • P

theorem Ideal.Quotient.eq_zero_iff_mem' {A : Type u_4} [CommRing A] (P : Ideal A) (x : A) : (algebraMap A (A ⧸ P)) x = 0 ↔ x ∈ P

noncomputable def Ideal.Quotient.out {R : Type u_7} [CommRing R] {I : Ideal R} (x : R ⧸ I) : R

Equations

• Ideal.Quotient.out x = Quotient.out' x

theorem Ideal.Quotient.out_eq {R : Type u_7} [CommRing R] {I : Ideal R} (x : R ⧸ I) : (Ideal.Quotient.mk I) (Ideal.Quotient.out x) = x

theorem Ideal.Quotient.induction_on {R : Type u_7} [CommRing R] {I : Ideal R} {p : R ⧸ I → Prop} (x : R ⧸ I) (h : ∀ (a : R), p ((Ideal.Quotient.mk I) a)) : p x

noncomputable def MulSemiringAction.CharacteristicPolynomial.Mbar {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] {Q : Ideal B} (P : Ideal A) (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) (bbar : B ⧸ Q) : Polynomial (A ⧸ P)

Equations

• MulSemiringAction.CharacteristicPolynomial.Mbar P hFull' bbar = Polynomial.map (Ideal.Quotient.mk P) (MulSemiringAction.CharacteristicPolynomial.M hFull' (Ideal.Quotient.out bbar))

theorem MulSemiringAction.CharacteristicPolynomial.Mbar_monic {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B) (P : Ideal A) (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial B] (bbar : B ⧸ Q) : (MulSemiringAction.CharacteristicPolynomial.Mbar P hFull' bbar).Monic

theorem MulSemiringAction.CharacteristicPolynomial.Mbar_deg {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B) (P : Ideal A) [P.IsPrime] (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial A] [Nontrivial B] (bbar : B ⧸ Q) : (MulSemiringAction.CharacteristicPolynomial.Mbar P hFull' bbar).degree = ↑(Nat.card G)

theorem MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B) (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) [Nontrivial A] [Nontrivial B] (bbar : B ⧸ Q) : Polynomial.eval₂ (algebraMap (A ⧸ P) (B ⧸ Q)) bbar (MulSemiringAction.CharacteristicPolynomial.Mbar P hFull' bbar) = 0

theorem MulSemiringAction.reduction_isIntegral {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B) (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] [Nontrivial A] [Nontrivial B] (hFull' : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) : Algebra.IsIntegral (A ⧸ P) (B ⧸ Q)

theorem Polynomial.nonzero_const_if_isIntegral (R : Type) (S : Type) [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) : ∃ (q : Polynomial R), q.coeff 0 ≠ 0 ∧ Polynomial.eval₂ (algebraMap R S) s q = 0

theorem Algebra.exists_dvd_nonzero_if_isIntegral (R : Type) (S : Type) [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] [IsDomain S] (s : S) (hs : s ≠ 0) : ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S) r

noncomputable def instAlgebraPolynomial_fLT {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] : Algebra (Polynomial A) (Polynomial B)

Equations

• instAlgebraPolynomial_fLT = (Polynomial.mapRingHom Algebra.toRingHom).toAlgebra

theorem IsAlgebraic.mul {R : Type u_9} {K : Type u_10} [CommRing R] [CommRing K] [Algebra R K] {x : K} {y : K} (hx : IsAlgebraic R x) (hy : IsAlgebraic R y) : IsAlgebraic R (x * y)

theorem IsAlgebraic.invLoc {R : Type u_9} {S : Type u_10} {K : Type u_11} [CommRing R] {M : Submonoid R} [CommRing S] [Algebra R S] [IsLocalization M S] {x : ↥M} [CommRing K] [Algebra K S] (h : IsAlgebraic K ↑↑x) : IsAlgebraic K (IsLocalization.mk' S 1 x)

noncomputable def Bourbaki52222.residueFieldExtensionPolynomial (G : Type u_6) (L : Type u_7) [Field L] (K : Type u_8) [Field K] [DecidableEq L] (x : L) : Polynomial K

Equations

• Bourbaki52222.residueFieldExtensionPolynomial G L K x = if x = 0 then (Polynomial.monomial (Nat.card G)) 1 else 37

theorem Bourbaki52222.f_exists {G : Type u_6} [Group G] [Finite G] (L : Type u_7) [Field L] (K : Type u_8) [Field K] [Algebra K L] [DecidableEq L] (l : L) : ∃ (f : Polynomial K), f.Monic ∧ f.degree = ↑(Nat.card G) ∧ Polynomial.eval₂ (algebraMap K L) l f = 0 ∧ Polynomial.Splits (algebraMap K L) f

theorem Bourbaki52222.algebraMap_cast {R : Type u_9} {S : Type u_10} [CommRing R] [CommRing S] [Algebra R S] (r : R) : ↑r = (algebraMap R S) r

theorem Bourbaki52222.algebraMap_algebraMap {R : Type u_9} {S : Type u_10} {T : Type u_11} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (r : R) : (algebraMap S T) ((algebraMap R S) r) = (algebraMap R T) r

theorem Bourbaki52222.Algebra.isAlgebraic_of_subring_isAlgebraic {R : Type u_9} {k : Type u_10} {K : Type u_11} [CommRing R] [CommRing k] [CommRing K] [Algebra R K] [IsFractionRing R K] [Algebra k K] (h : ∀ (x : R), IsAlgebraic k ↑x) : Algebra.IsAlgebraic k K

theorem Bourbaki52222.algebraic {A : Type u_9} [CommRing A] {B : Type u_10} [Nontrivial B] [CommRing B] [Algebra A B] [Algebra.IsIntegral A B] {G : Type u_11} [Group G] [Finite G] [MulSemiringAction G B] (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (L : Type u_12) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] (K : Type u_13) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [Algebra A K] [IsScalarTower A (A ⧸ P) K] [Algebra B L] [IsScalarTower B (B ⧸ Q) L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] (hFull : ∀ (b : B), (∀ (g : G), g • b = b) → ∃ (a : A), b = ↑a) : Algebra.IsAlgebraic K L

theorem Bourbaki52222.normal {G : Type u_3} [Group G] [Finite G] (L : Type u_7) [Field L] (K : Type u_8) [Field K] [Algebra K L] [DecidableEq L] : Normal K L

theorem Bourbaki52222.separableClosure_finiteDimensional (L : Type u_7) [Field L] (K : Type u_8) [Field K] [Algebra K L] : FiniteDimensional K ↥(separableClosure K L)

theorem Bourbaki52222.separableClosure_finrank_le {G : Type u_6} [Group G] [Finite G] (L : Type u_7) [Field L] (K : Type u_8) [Field K] [Algebra K L] : Module.finrank K ↥(separableClosure K L) ≤ Nat.card G

theorem Bourbaki52222.primitive_element (L : Type u_7) [Field L] (K : Type u_8) [Field K] [Algebra K L] : ∃ (y : L), K⟮y⟯ = separableClosure K L

noncomputable def Bourbaki52222.y (L : Type u_7) [Field L] (K : Type u_8) [Field K] [Algebra K L] : L

Equations

• Bourbaki52222.y L K = ⋯.choose

def Bourbaki52222.quotientRingAction {B : Type u_5} [CommRing B] {G : Type u_6} [Group G] [MulSemiringAction G B] (Q : Ideal B) (Q' : Ideal B) (g : G) (hg : g • Q = Q') : B ⧸ Q ≃+* B ⧸ Q'

Equations

• Bourbaki52222.quotientRingAction Q Q' g hg = Q.quotientEquiv Q' (MulSemiringAction.toRingEquiv G B g) ⋯

def Bourbaki52222.quotientAlgebraAction {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (Q : Ideal B) (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (g : G) (hg : g • Q = Q) : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q

Equations

• Bourbaki52222.quotientAlgebraAction Q P g hg = { toEquiv := (Bourbaki52222.quotientRingAction Q Q g hg).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def Bourbaki52222.Pointwise.quotientAlgebraActionMonoidHom {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (Q : Ideal B) (P : Ideal A) [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] : ↥(MulAction.stabilizer G Q) →* (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q

Equations

• Bourbaki52222.Pointwise.quotientAlgebraActionMonoidHom Q P = { toFun := fun (gh : ↥(MulAction.stabilizer G Q)) => Bourbaki52222.quotientAlgebraAction Q P ↑gh ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def Bourbaki52222.IsFractionRing.algEquiv_lift {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] (L : Type u_7) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] (K : Type u_8) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [Algebra K L] [IsScalarTower (A ⧸ P) K L] (e : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) : L ≃ₐ[K] L

Equations

• Bourbaki52222.IsFractionRing.algEquiv_lift Q P L K e = { toEquiv := (IsFractionRing.fieldEquivOfRingEquiv e.toRingEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def Bourbaki52222.stabilizer.toGaloisGroup {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (L : Type u_7) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] (K : Type u_8) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [Algebra K L] [IsScalarTower (A ⧸ P) K L] : ↥(MulAction.stabilizer G Q) →* L ≃ₐ[K] L

Equations

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

theorem Bourbaki52222.MulAction.stabilizer_surjective_of_action {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] {G : Type u_6} [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] (Q : Ideal B) [Q.IsPrime] (P : Ideal A) [P.IsPrime] [Algebra (A ⧸ P) (B ⧸ Q)] [IsScalarTower A (A ⧸ P) (B ⧸ Q)] (L : Type u_7) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] (K : Type u_8) [Field K] [Algebra (A ⧸ P) K] [IsFractionRing (A ⧸ P) K] [Algebra K L] [IsScalarTower (A ⧸ P) K L] : Function.Surjective ⇑(Bourbaki52222.stabilizer.toGaloisGroup Q P L K)

From Bourbaki Comm Alg, Chapter V.

@[reducible, inline]

abbrev S {A : Type u_4} [CommRing A] (P : Ideal A) [P.IsPrime] : Submonoid A

Equations

• S P = P.primeCompl

@[reducible, inline]

abbrev SA {A : Type u_4} [CommRing A] (P : Ideal A) [P.IsPrime] : Type u_4

Equations

• SA P = OreLocalization (S P) A

@[reducible, inline]

abbrev SB {A : Type u_4} [CommRing A] {B : Type u_5} [CommRing B] [Algebra A B] (P : Ideal A) [P.IsPrime] : Type (max u_4 u_5)

Equations

• SB P = OreLocalization (S P) B