[Merged by Bors] - chore(algebra/ring/ulift): Split off and golf field instances

src/algebra/field/ulift.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import algebra.field.basic
+import algebra.ring.ulift
+
+/-!
+# Field instances for `ulift`
+
+This file defines instances for field, semifield and related structures on `ulift` types.
+
+(Recall `ulift α` is just a "copy" of a type `α` in a higher universe.)
+-/
+
+universes u v
+variables {α : Type u} {x y : ulift.{v} α}
+
+namespace ulift
+
+instance [has_rat_cast α] : has_rat_cast (ulift α) := ⟨λ a, up a⟩
+
+@[simp, norm_cast] lemma up_rat_cast [has_rat_cast α] (q : ℚ) : up (q : α) = q := rfl
+@[simp, norm_cast] lemma down_rat_cast [has_rat_cast α] (q : ℚ) : down (q : ulift α) = q := rfl
+
+instance division_semiring [division_semiring α] : division_semiring (ulift α) :=
+by refine down_injective.division_semiring down _ _ _ _ _ _ _ _ _ _; intros; refl
+
+instance semifield [semifield α] : semifield (ulift α) :=
+{ ..ulift.division_semiring, ..ulift.comm_group_with_zero }
+
+instance division_ring [division_ring α] : division_ring (ulift α) :=
+{ ..ulift.division_semiring, ..ulift.add_group }
+
+instance field [field α] : field (ulift α) :=
+{ ..ulift.semifield, ..ulift.division_ring }
+
+end ulift

src/algebra/group/ulift.lean

@@ -77,20 +77,27 @@ equiv.ulift.injective.mul_zero_one_class _ rfl rfl $ λ x y, rfl
 instance monoid [monoid α] : monoid (ulift α) :=
 equiv.ulift.injective.monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
-instance add_monoid_with_one [add_monoid_with_one α] : add_monoid_with_one (ulift α) :=
-{ nat_cast := λ n, ⟨n⟩,
-  nat_cast_zero := congr_arg ulift.up nat.cast_zero,
-  nat_cast_succ := λ n, congr_arg ulift.up (nat.cast_succ _),
-  .. ulift.has_one, .. ulift.add_monoid }
-
-@[simp] lemma nat_cast_down [add_monoid_with_one α] (n : ℕ) :
-  (n : ulift α).down = n :=
-rfl
-
 @[to_additive]
 instance comm_monoid [comm_monoid α] : comm_monoid (ulift α) :=
 equiv.ulift.injective.comm_monoid _ rfl (λ _ _, rfl) (λ _ _, rfl)
 
+instance [has_nat_cast α] : has_nat_cast (ulift α) := ⟨λ n, up n⟩
+instance [has_int_cast α] : has_int_cast (ulift α) := ⟨λ n, up n⟩
+
+@[simp, norm_cast] lemma up_nat_cast [has_nat_cast α] (n : ℕ) : up (n : α) = n := rfl
+@[simp, norm_cast] lemma up_int_cast [has_int_cast α] (n : ℤ) : up (n : α) = n := rfl
+@[simp, norm_cast] lemma down_nat_cast [has_nat_cast α] (n : ℕ) : down (n : ulift α) = n := rfl
+@[simp, norm_cast] lemma down_int_cast [has_int_cast α] (n : ℤ) : down (n : ulift α) = n := rfl
+
+instance add_monoid_with_one [add_monoid_with_one α] : add_monoid_with_one (ulift α) :=
+{ nat_cast_zero := congr_arg ulift.up nat.cast_zero,
+  nat_cast_succ := λ n, congr_arg ulift.up (nat.cast_succ _),
+  .. ulift.has_one, .. ulift.add_monoid, ..ulift.has_nat_cast }
+
+instance add_comm_monoid_with_one [add_comm_monoid_with_one α] :
+  add_comm_monoid_with_one (ulift α) :=
+{ ..ulift.add_monoid_with_one, .. ulift.add_comm_monoid }
+
 instance monoid_with_zero [monoid_with_zero α] : monoid_with_zero (ulift α) :=
 equiv.ulift.injective.monoid_with_zero _ rfl rfl (λ _ _, rfl) (λ _ _, rfl)
 
@@ -107,20 +114,19 @@ instance group [group α] : group (ulift α) :=
 equiv.ulift.injective.group _ rfl (λ _ _, rfl) (λ _, rfl)
   (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
 
+@[to_additive]
+instance comm_group [comm_group α] : comm_group (ulift α) :=
+equiv.ulift.injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl)
+  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+
 instance add_group_with_one [add_group_with_one α] : add_group_with_one (ulift α) :=
 { int_cast := λ n, ⟨n⟩,
   int_cast_of_nat := λ n, congr_arg ulift.up (int.cast_of_nat _),
   int_cast_neg_succ_of_nat := λ n, congr_arg ulift.up (int.cast_neg_succ_of_nat _),
   .. ulift.add_monoid_with_one, .. ulift.add_group }
 
-@[simp] lemma int_cast_down [add_group_with_one α] (n : ℤ) :
-  (n : ulift α).down = n :=
-rfl
-
-@[to_additive]
-instance comm_group [comm_group α] : comm_group (ulift α) :=
-equiv.ulift.injective.comm_group _ rfl (λ _ _, rfl) (λ _, rfl)
-  (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)
+instance add_comm_group_with_one [add_comm_group_with_one α] : add_comm_group_with_one (ulift α) :=
+{ ..ulift.add_group_with_one, .. ulift.add_comm_group }
 
 instance group_with_zero [group_with_zero α] : group_with_zero (ulift α) :=
 equiv.ulift.injective.group_with_zero _ rfl rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

src/algebra/ring/ulift.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.group.ulift
-import algebra.field.defs
 import algebra.ring.equiv
 
 /-!
@@ -107,25 +106,4 @@ instance comm_ring [comm_ring α] : comm_ring (ulift α) :=
 by refine_struct { .. ulift.ring };
 tactic.pi_instance_derive_field
 
-instance [has_rat_cast α] : has_rat_cast (ulift α) :=
-⟨λ a, ulift.up (coe a)⟩
-
-@[simp] lemma rat_cast_down [has_rat_cast α] (n : ℚ) : ulift.down (n : ulift α) = n :=
-rfl
-
-instance field [field α] : field (ulift α) :=
-begin
-  have of_rat_mk : ∀ a b h1 h2, ((⟨a, b, h1, h2⟩ : ℚ) : ulift α) = ↑a * (↑b)⁻¹,
-  { intros a b h1 h2,
-    ext,
-    rw [rat_cast_down, mul_down, inv_down, nat_cast_down, int_cast_down],
-    exact field.rat_cast_mk a b h1 h2 },
-  refine_struct { zero := (0 : ulift α), inv := has_inv.inv, div := has_div.div,
-  zpow := λ n a, ulift.up (a.down ^ n), rat_cast := coe, rat_cast_mk := of_rat_mk, qsmul := (•),
-  .. @ulift.nontrivial α _, .. ulift.comm_ring }; tactic.pi_instance_derive_field,
-  -- `mul_inv_cancel` requires special attention: it leaves the goal `∀ {a}, a ≠ 0 → a * a⁻¹ = 1`.
-  cases a,
-  tauto
-end
-
 end ulift

src/field_theory/cardinality.lean

@@ -3,14 +3,14 @@ Copyright (c) 2022 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
-import algebra.ring.ulift
+import algebra.field.ulift
 import data.mv_polynomial.cardinal
+import data.nat.factorization.prime_pow
 import data.rat.denumerable
 import field_theory.finite.galois_field
 import logic.equiv.transfer_instance
 import ring_theory.localization.cardinality
 import set_theory.cardinal.divisibility
-import data.nat.factorization.prime_pow
 
 /-!
 # Cardinality of Fields