R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
⊢ inertiaDeg (algebraMap R S) p P = finrank (R ⧸ p) (S ⧸ P)
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
⊢ inertiaDeg (algebraMap R S) p P = finrank (R ⧸ p) (S ⧸ P)
nontriviality S ⧸ P using inertiaDeg_of_subsingleton, finrank_zero_of_subsingleton
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
⊢ inertiaDeg (algebraMap R S) p P = finrank (R ⧸ p) (S ⧸ P)
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
⊢ inertiaDeg (algebraMap R S) p P = finrank (R ⧸ p) (S ⧸ P)
have := comap_eq_of_scalar_tower_quotient (algebraMap (R ⧸ p) (S ⧸ P)).injective
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
⊢ finrank (R ⧸ p) (S ⧸ P) = finrank (R ⧸ p) (S ⧸ P)
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
⊢ inertiaDeg (algebraMap R S) p P = finrank (R ⧸ p) (S ⧸ P)
rw [inertiaDeg, dif_pos this]
case h.e_5.h.h.e_5.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
⊢ RingHom.toAlgebra
      (Quotient.lift p (RingHom.comp (Quotient.mk P) (algebraMap R S))
        (_ : ∀ (x : R), x ∈ p → ↑(Quotient.mk P) (↑(algebraMap R S) x) = 0)) =
    inst✝¹
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
⊢ finrank (R ⧸ p) (S ⧸ P) = finrank (R ⧸ p) (S ⧸ P)
congr
case h.e_5.h.h.e_5.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
x' : R ⧸ p
x : R
⊢ ↑(algebraMap (R ⧸ p) (S ⧸ P)) (Quotient.mk'' x) = ↑(algebraMap (R ⧸ p) (S ⧸ P)) (Quotient.mk'' x)
case h.e_5.h.h.e_5.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
⊢ RingHom.toAlgebra
      (Quotient.lift p (RingHom.comp (Quotient.mk P) (algebraMap R S))
        (_ : ∀ (x : R), x ∈ p → ↑(Quotient.mk P) (↑(algebraMap R S) x) = 0)) =
    inst✝¹
refine' Algebra.algebra_ext _ _ fun x' => Quotient.inductionOn' x' fun x => _
case h.e_5.h.h.e_5.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
x' : R ⧸ p
x : R
⊢ ↑(Quotient.lift p (RingHom.comp (Quotient.mk P) (algebraMap R S))
          (_ : ∀ (x : R), x ∈ p → ↑(Quotient.mk P) (↑(algebraMap R S) x) = 0))
      (↑(Quotient.mk p) x) =
    ↑(algebraMap ((fun x => R ⧸ p) x) (S ⧸ P)) (↑(Quotient.mk p) x)
case h.e_5.h.h.e_5.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
x' : R ⧸ p
x : R
⊢ ↑(algebraMap (R ⧸ p) (S ⧸ P)) (Quotient.mk'' x) = ↑(algebraMap (R ⧸ p) (S ⧸ P)) (Quotient.mk'' x)
change Ideal.Quotient.lift p _ _ (Ideal.Quotient.mk p x) = algebraMap _ _ (Ideal.Quotient.mk p x)
no goals
case h.e_5.h.h.e_5.h
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
f : R →+* S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
hp : IsMaximal p
✝ : Nontrivial (S ⧸ P)
this : comap (algebraMap R S) P = p
x' : R ⧸ p
x : R
⊢ ↑(Quotient.lift p (RingHom.comp (Quotient.mk P) (algebraMap R S))
          (_ : ∀ (x : R), x ∈ p → ↑(Quotient.mk P) (↑(algebraMap R S) x) = 0))
      (↑(Quotient.mk p) x) =
    ↑(algebraMap ((fun x => R ⧸ p) x) (S ⧸ P)) (↑(Quotient.mk p) x)
rw [Ideal.Quotient.lift_mk, ← Ideal.Quotient.algebraMap_eq P, ← IsScalarTower.algebraMap_eq,
  ← Ideal.Quotient.algebraMap_eq,  ← IsScalarTower.algebraMap_apply]