@@ -32,14 +32,16 @@ Instances constructed from this result:
3232
3333@[expose] public section
3434
35+ variable {R A : Type *}
36+
3537/-- Given `R →+* A`, then `char A ∣ char R`. -/
36- theorem CharP.dvd_of_ringHom {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A]
38+ theorem CharP.dvd_of_ringHom [NonAssocSemiring R] [NonAssocSemiring A]
3739 (f : R →+* A) (p q : ℕ) [CharP R p] [CharP A q] : q ∣ p := by
3840 refine (CharP.cast_eq_zero_iff A q p).mp ?_
3941 rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]
4042
4143/-- Given `R →+* A`, where `R` is a domain with `char R > 0`, then `char A = char R`. -/
42- theorem CharP.of_ringHom_of_ne_zero {R A : Type *} [NonAssocSemiring R] [NoZeroDivisors R]
44+ theorem CharP.of_ringHom_of_ne_zero [NonAssocSemiring R] [NoZeroDivisors R]
4345 [NonAssocSemiring A] [Nontrivial A]
4446 (f : R →+* A) (p : ℕ) (hp : p ≠ 0 ) [CharP R p] : CharP A p := by
4547 have := f.domain_nontrivial
@@ -51,47 +53,47 @@ theorem CharP.of_ringHom_of_ne_zero {R A : Type*} [NonAssocSemiring R] [NoZeroDi
5153 exact e ▸ hq
5254
5355/-- If a ring homomorphism `R →+* A` is injective then `A` has the same characteristic as `R`. -/
54- theorem charP_of_injective_ringHom {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A]
56+ theorem charP_of_injective_ringHom [NonAssocSemiring R] [NonAssocSemiring A]
5557 {f : R →+* A} (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p where
5658 cast_eq_zero_iff x := by
5759 rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]
5860
5961/-- If the algebra map `R →+* A` is injective then `A` has the same characteristic as `R`. -/
60- theorem charP_of_injective_algebraMap {R A : Type *} [CommSemiring R] [Semiring A] [Algebra R A]
62+ theorem charP_of_injective_algebraMap [CommSemiring R] [Semiring A] [Algebra R A]
6163 (h : Function.Injective (algebraMap R A)) (p : ℕ) [CharP R p] : CharP A p :=
6264 charP_of_injective_ringHom h p
6365
64- theorem charP_of_injective_algebraMap' (R : Type *) {A : Type *} [CommRing R] [Semiring A]
66+ theorem charP_of_injective_algebraMap' (R : Type *) [CommRing R] [Semiring A]
6567 [Algebra R A] [FaithfulSMul R A] (p : ℕ) [CharP R p] : CharP A p :=
6668 charP_of_injective_ringHom (FaithfulSMul.algebraMap_injective R A) p
6769
6870/-- If a ring homomorphism `R →+* A` is injective and `R` has characteristic zero
6971then so does `A`. -/
70- theorem charZero_of_injective_ringHom {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A]
72+ theorem charZero_of_injective_ringHom [NonAssocSemiring R] [NonAssocSemiring A]
7173 {f : R →+* A} (h : Function.Injective f) [CharZero R] : CharZero A where
7274 cast_injective _ _ _ := CharZero.cast_injective <| h <| by simpa only [map_natCast f]
7375
7476/-- If the algebra map `R →+* A` is injective and `R` has characteristic zero then so does `A`. -/
75- theorem charZero_of_injective_algebraMap {R A : Type *} [CommSemiring R] [Semiring A] [Algebra R A]
77+ theorem charZero_of_injective_algebraMap [CommSemiring R] [Semiring A] [Algebra R A]
7678 (h : Function.Injective (algebraMap R A)) [CharZero R] : CharZero A :=
7779 charZero_of_injective_ringHom h
7880
7981/-- If `R →+* A` is injective, and `A` is of characteristic `p`, then `R` is also of
8082characteristic `p`. Similar to `RingHom.charZero`. -/
81- theorem RingHom.charP {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
83+ theorem RingHom.charP [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
8284 (H : Function.Injective f) (p : ℕ) [CharP A p] : CharP R p := by
8385 obtain ⟨q, h⟩ := CharP.exists R
8486 exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h
8587
8688/-- If `R →+* A` is injective, then `R` is of characteristic `p` if and only if `A` is also of
8789characteristic `p`. Similar to `RingHom.charZero_iff`. -/
88- protected theorem RingHom.charP_iff {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A]
90+ protected theorem RingHom.charP_iff [NonAssocSemiring R] [NonAssocSemiring A]
8991 (f : R →+* A) (H : Function.Injective f) (p : ℕ) : CharP R p ↔ CharP A p :=
9092 ⟨fun _ ↦ charP_of_injective_ringHom H p, fun _ ↦ f.charP H p⟩
9193
9294/-- If a ring homomorphism `R →+* A` is injective then `A` has the same exponential characteristic
9395as `R`. -/
94- lemma expChar_of_injective_ringHom {R A : Type *}
96+ lemma expChar_of_injective_ringHom
9597 [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A} (h : Function.Injective f)
9698 (q : ℕ) [hR : ExpChar R q] : ExpChar A q := by
9799 rcases hR with _ | hprime
@@ -100,33 +102,42 @@ lemma expChar_of_injective_ringHom {R A : Type*}
100102
101103/-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
102104exponential characteristic `p`. Similar to `RingHom.charZero`. -/
103- lemma RingHom.expChar {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
105+ lemma RingHom.expChar [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
104106 (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p := by
105107 cases ‹ExpChar A p› with
106108 | zero => haveI := f.charZero; exact .zero
107109 | prime hp => haveI := f.charP H p; exact .prime hp
108110
109111/-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
110112also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`. -/
111- lemma RingHom.expChar_iff {R A : Type *} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
113+ lemma RingHom.expChar_iff [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
112114 (H : Function.Injective f) (p : ℕ) : ExpChar R p ↔ ExpChar A p :=
113115 ⟨fun _ ↦ expChar_of_injective_ringHom H p, fun _ ↦ f.expChar H p⟩
114116
115117/-- If the algebra map `R →+* A` is injective then `A` has the same exponential characteristic
116118as `R`. -/
117- lemma expChar_of_injective_algebraMap {R A : Type *} [CommSemiring R] [Semiring A] [Algebra R A]
119+ lemma expChar_of_injective_algebraMap [CommSemiring R] [Semiring A] [Algebra R A]
118120 (h : Function.Injective (algebraMap R A)) (q : ℕ) [ExpChar R q] : ExpChar A q :=
119121 expChar_of_injective_ringHom h q
120122
121- theorem ExpChar.of_injective_algebraMap' (R : Type *) {A : Type *} [CommRing R] [CommRing A]
123+ variable (R) in
124+ theorem ExpChar.of_injective_algebraMap' [CommRing R] [CommRing A]
122125 [Algebra R A] [FaithfulSMul R A] (q : ℕ) [ExpChar R q] : ExpChar A q :=
123126 expChar_of_injective_ringHom (FaithfulSMul.algebraMap_injective R A) q
124127
128+ namespace Subfield
129+
130+ variable [DivisionRing R] (L : Subfield R) (p : ℕ)
131+
132+ instance charP [CharP R p] : CharP L p := L.subtype.charP L.subtype_injective p
133+ instance expChar [ExpChar R p] : ExpChar L p := L.subtype.expChar L.subtype_injective p
134+
135+ end Subfield
136+
125137/-!
126138As an application, a `ℚ`-algebra has characteristic zero.
127139-/
128140
129-
130141-- `CharP.charP_to_charZero A _ (charP_of_injective_algebraMap h 0)` does not work
131142-- here as it would require `Ring A`.
132143section QAlgebra
0 commit comments