-- Mathlib/RingTheory/Frobenius.lean
/-- Let `G` be a finite group acting on `S`, and `R` be the fixed subring.
If `Q` is a prime of `S` with finite residue field,
then there exists a Frobenius element `σ : G` at `Q`. -/
lemma exists_of_isInvariant [Q.IsPrime] [Finite (S ⧸ Q)] : ∃ σ : G, IsArithFrobAt R σ Q

Proof state:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝¹ : Algebra.IsIntegral R S
this✝ : Q.IsMaximal
this : P.IsMaximal
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
obtain ⟨p, hc⟩ := CharP.exists (R ⧸ P)

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝¹ : Algebra.IsIntegral R S
this✝ : Q.IsMaximal
this : P.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
⊢ ∃ σ, IsArithFrobAt R σ Q

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝¹ : Algebra.IsIntegral R S
this✝ : Q.IsMaximal
this : P.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝² : Algebra.IsIntegral R S
this✝¹ : Q.IsMaximal
this✝ : P.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this : Finite (R ⧸ P)
⊢ ∃ σ, IsArithFrobAt R σ Q

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝⁴ : Algebra.IsIntegral R S
this✝³ : Q.IsMaximal
this✝² : P.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
l : (S ⧸ Q) ≃ₐ[R ⧸ P] S ⧸ Q :=
  let __spread.0 := iterateFrobeniusEquiv (S ⧸ Q) p ↑k;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ : (Ideal.Quotient.stabilizerHom Q P G) σ = l
x : S
⊢ (Ideal.Quotient.mk Q) ((MulSemiringAction.toAlgHom R S ↑σ) x) = (Ideal.Quotient.mk Q) (x ^ p ^ ↑k)

Tactic:
exact DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝ : Algebra.IsIntegral R S
this : Q.IsMaximal
⊢ ∃ σ, IsArithFrobAt R σ Q

Tactic:
have : P.IsMaximal := Ideal.isMaximal_comap_of_isIntegral_of_isMaximal Q

Result:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝¹ : Algebra.IsIntegral R S
this✝ : Q.IsMaximal
this : P.IsMaximal
⊢ ∃ σ, IsArithFrobAt R σ Q

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝⁴ : Algebra.IsIntegral R S
this✝³ : Q.IsMaximal
this✝² : P.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
l : (S ⧸ Q) ≃ₐ[R ⧸ P] S ⧸ Q :=
  let __spread.0 := iterateFrobeniusEquiv (S ⧸ Q) p ↑k;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ : (Ideal.Quotient.stabilizerHom Q P G) σ = l
x : S
⊢ (MulSemiringAction.toAlgHom R S ↑σ) x - x ^ Nat.card (R ⧸ Ideal.under R Q) ∈ Q

Tactic:
rw [← Ideal.Quotient.eq, Nat.card_eq_fintype_card, hk]

Result:
case intro.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
G : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulSemiringAction G S
inst✝⁴ : SMulCommClass G R S
Q : Ideal S
inst✝³ : Finite G
inst✝² : Algebra.IsInvariant R S G
inst✝¹ : Q.IsPrime
inst✝ : Finite (S ⧸ Q)
P : Ideal R := Ideal.under R Q
this✝⁴ : Algebra.IsIntegral R S
this✝³ : Q.IsMaximal
this✝² : P.IsMaximal
p : ℕ
hc : CharP (R ⧸ P) p
this✝¹ : Finite (R ⧸ P)
val✝ : Fintype (R ⧸ P)
k : ℕ+
hp : Nat.Prime p
hk : Fintype.card (R ⧸ P) = p ^ ↑k
this✝ : CharP (S ⧸ Q) p
this : ExpChar (S ⧸ Q) p
l : (S ⧸ Q) ≃ₐ[R ⧸ P] S ⧸ Q :=
  let __spread.0 := iterateFrobeniusEquiv (S ⧸ Q) p ↑k;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
σ : ↥(MulAction.stabilizer G Q)
hσ : (Ideal.Quotient.stabilizerHom Q P G) σ = l
x : S
⊢ (Ideal.Quotient.mk Q) ((MulSemiringAction.toAlgHom R S ↑σ) x) = (Ideal.Quotient.mk Q) (x ^ p ^ ↑k)