Theorems · Definition · algebraic geometry
Algebra.IsUnramifiedAt
(R : Type u_1) →
{A : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (q : Ideal A) → [q.IsPrime] → PropWe say that an R-algebra A is unramified at a prime q of A
if A_q is formally unramified over R.
If A is of finite type over R and q is lying over p, then this is equivalent to
κ(q)/κ(p) being separable and pA_q = qA_q.
See Algebra.isUnramifiedAt_iff_map_eq in RingTheory.Unramified.LocalRing
- Defined in
- Mathlib.RingTheory.Unramified.Locus
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Idealstatement and proof · cited by 4,748
- Ideal.IsPrimestatement and proof · cited by 827
- Localization.AtPrimeproof · cited by 299
- Algebra.FormallyUnramifiedproof · cited by 75
Cited by37
Results whose statement or proof uses this declaration.
- Algebra.IsUnramifiedInproof · cited by 9
- Algebra.unramifiedLocusproof · cited by 6
- Ideal.ramificationIdx_eq_one_iffstatement and proof · cited by 4
- Algebra.formallyUnramified_iff_forallstatement · cited by 3
- Ideal.ramificationIdx_eq_onestatement and proof · cited by 3
- Algebra.exists_formallyUnramified_of_isUnramifiedAtstatement and proof · cited by 2
- Algebra.isUnramifiedAt_botstatement · cited by 2
- Algebra.isUnramifiedAt_iff_map_eqstatement and proof · cited by 2
- NumberField.not_dvd_discr_iff_forall_liesOverstatement · cited by 2
- NumberField.exists_not_isUnramifiedAt_intstatement · cited by 2
- NumberField.finrank_eq_one_of_unramifiedproof · cited by 1
- IsUnramifiedAt.of_liesOver_of_ne_botstatement and proof · cited by 1