Jyxu/graded module (#18308)

scripts/nolints.txt

@@ -345,9 +345,6 @@ apply_nolint stream.unfolds doc_blame
 -- data/stream/init.lean
 apply_nolint stream.is_bisimulation doc_blame
 
--- geometry/euclidean/circumcenter.lean
-apply_nolint affine_independent.exists_unique_dist_eq fintype_finite
-
 -- group_theory/group_action/sub_mul_action.lean
 apply_nolint sub_mul_action.has_zero fails_quickly
 

scripts/port_status.py

@@ -71,6 +71,11 @@ def mk_label(path: Path) -> str:
 for node in graph.nodes:
     if data[node].mathlib3_hash:
         verified[node] = data[node].mathlib3_hash
+        find_blobs_command = ['git', 'cat-file', '-t', data[node].mathlib3_hash]
+        hash_type = subprocess.check_output(find_blobs_command)
+        # the hash_type should be commits mostly, we are not interested in blobs
+        if b'blob\n' == hash_type:
+            break
         git_command = ['git', 'diff', '--quiet',
             f'--ignore-matching-lines={comment_git_re}',
             data[node].mathlib3_hash + "..HEAD", "--", "src" + os.sep + node.replace('.', os.sep) + ".lean"]

src/algebra/direct_sum/ring.lean

@@ -122,16 +122,6 @@ class gcomm_ring [add_comm_monoid ι] [Π i, add_comm_group (A i)] extends
 
 end defs
 
-/-- A graded version of `semiring.to_module`. -/
-instance gsemiring.to_gmodule (A : ι → Type*)
-  [add_monoid ι] [Π (i : ι), add_comm_monoid (A i)] [gsemiring A] :
-  graded_monoid.gmodule A A :=
-{ smul_add := λ _ _, gsemiring.mul_add,
-  smul_zero := λ i j, gsemiring.mul_zero,
-  add_smul := λ i j, gsemiring.add_mul,
-  zero_smul := λ i j, gsemiring.zero_mul,
-  ..graded_monoid.gmonoid.to_gmul_action A }
-
 lemma of_eq_of_graded_monoid_eq {A : ι → Type*} [Π (i : ι), add_comm_monoid (A i)]
   {i j : ι} {a : A i} {b : A j} (h : graded_monoid.mk i a = graded_monoid.mk j b) :
   direct_sum.of A i a = direct_sum.of A j b :=

src/algebra/gcd_monoid/finset.lean

@@ -9,6 +9,9 @@ import algebra.gcd_monoid.multiset
 /-!
 # GCD and LCM operations on finsets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main definitions
 
 - `finset.gcd` - the greatest common denominator of a `finset` of elements of a `gcd_monoid`

src/algebra/graded_mul_action.lean

@@ -104,12 +104,6 @@ class set_like.has_graded_smul {S R N M : Type*} [set_like S R] [set_like N M]
   [has_smul R M] [has_add ι] (A : ι → S) (B : ι → N) : Prop :=
 (smul_mem : ∀ ⦃i j : ι⦄ {ai bj}, ai ∈ A i → bj ∈ B j → ai • bj ∈ B (i + j))
 
-lemma set_like.smul_mem_graded {S R N M : Type*} [set_like S R] [set_like N M]
-  [has_smul R M] [has_add ι] {A : ι → S} {B : ι → N} [set_like.has_graded_smul A B]
-  ⦃i j⦄ {gi gj} (hi : gi ∈ A i) (hj : gj ∈ B j) :
-  gi • gj ∈ B (i + j) :=
-set_like.has_graded_smul.smul_mem hi hj
-
 instance set_like.ghas_smul {S R N M : Type*} [set_like S R] [set_like N M]
   [has_smul R M] [has_add ι] (A : ι → S) (B : ι → N) [set_like.has_graded_smul A B] :
   graded_monoid.ghas_smul (λ i, A i) (λ i, B i) :=
@@ -136,6 +130,6 @@ variables {S R N M : Type*} [set_like S R] [set_like N M]
 lemma set_like.is_homogeneous.graded_smul [has_add ι] [has_smul R M] {A : ι → S} {B : ι → N}
   [set_like.has_graded_smul A B] {a : R} {b : M} :
   set_like.is_homogeneous A a → set_like.is_homogeneous B b → set_like.is_homogeneous B (a • b)
-| ⟨i, hi⟩ ⟨j, hj⟩ := ⟨i + j, set_like.smul_mem_graded hi hj⟩
+| ⟨i, hi⟩ ⟨j, hj⟩ := ⟨i + j, set_like.has_graded_smul.smul_mem hi hj⟩
 
 end homogeneous_elements

src/algebra/group/basic.lean

@@ -651,3 +651,47 @@ lemma bit1_sub [has_one M] (a b : M) : bit1 (a - b) = bit1 a - bit0 b :=
 (congr_arg (+ (1 : M)) $ bit0_sub a b : _).trans $ sub_add_eq_add_sub _ _ _
 
 end subtraction_comm_monoid
+
+section multiplicative
+
+variables [monoid β] (p r : α → α → Prop) [is_total α r] (f : α → α → β)
+
+@[to_additive additive_of_symmetric_of_is_total]
+lemma multiplicative_of_symmetric_of_is_total
+  (hsymm : symmetric p) (hf_swap : ∀ {a b}, p a b → f a b * f b a = 1)
+  (hmul : ∀ {a b c}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c)
+  {a b c : α} (pab : p a b) (pbc : p b c) (pac : p a c) : f a c = f a b * f b c :=
+begin
+  suffices : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c,
+  { obtain rbc | rcb := total_of r b c,
+    { exact this rbc pab pbc pac },
+    { rw [this rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one] } },
+  intros b c rbc pab pbc pac,
+  obtain rab | rba := total_of r a b,
+  { exact hmul rab rbc pab pbc pac },
+  rw [← one_mul (f a c), ← hf_swap pab, mul_assoc],
+  obtain rac | rca := total_of r a c,
+  { rw [hmul rba rac (hsymm pab) pac pbc] },
+  { rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one] },
+end
+
+/-- If a binary function from a type equipped with a total relation `r` to a monoid is
+  anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
+  (i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
+  We allow restricting to a subset specified by a predicate `p`. -/
+@[to_additive additive_of_is_total "If a binary function from a type equipped with a total relation
+  `r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in order to show
+  it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and `r b c`
+  are satisfied. We allow restricting to a subset specified by a predicate `p`."]
+lemma multiplicative_of_is_total (p : α → Prop)
+  (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1)
+  (hmul : ∀ {a b c}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c)
+  {a b c : α} (pa : p a) (pb : p b) (pc : p c) : f a c = f a b * f b c :=
+begin
+  apply multiplicative_of_symmetric_of_is_total (λ a b, p a ∧ p b) r f (λ _ _, and.swap),
+  { simp_rw and_imp, exact @hswap },
+  { exact λ a b c rab rbc pab pbc pac, hmul rab rbc pab.1 pab.2 pac.2 },
+  exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩],
+end
+
+end multiplicative

src/algebra/group/inj_surj.lean

@@ -179,6 +179,17 @@ protected def comm_monoid [comm_monoid M₂] (f : M₁ → M₂) (hf : injective
   comm_monoid M₁ :=
 { .. hf.comm_semigroup f mul, .. hf.monoid f one mul npow }
 
+/-- A type endowed with `0`, `1` and `+` is an additive commutative monoid with one, if it admits an
+injective map that preserves `0`, `1` and `+` to an additive commutative monoid with one.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def add_comm_monoid_with_one {M₁} [has_zero M₁] [has_one M₁] [has_add M₁] [has_smul ℕ M₁]
+  [has_nat_cast M₁] [add_comm_monoid_with_one M₂] (f : M₁ → M₂) (hf : injective f) (zero : f 0 = 0)
+  (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x)
+  (nat_cast : ∀ n : ℕ, f n = n) :
+  add_comm_monoid_with_one M₁ :=
+{ ..hf.add_monoid_with_one f zero one add nsmul nat_cast, ..hf.add_comm_monoid f zero add nsmul }
+
 /-- A type endowed with `1` and `*` is a cancel commutative monoid,
 if it admits an injective map that preserves `1` and `*` to a cancel commutative monoid.
 See note [reducible non-instances]. -/
@@ -303,6 +314,21 @@ protected def comm_group [comm_group M₂] (f : M₁ → M₂) (hf : injective f
   comm_group M₁ :=
 { .. hf.comm_monoid f one mul npow, .. hf.group f one mul inv div npow zpow }
 
+/-- A type endowed with `0`, `1` and `+` is an additive commutative group with one, if it admits an
+injective map that preserves `0`, `1` and `+` to an additive commutative group with one.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def add_comm_group_with_one {M₁} [has_zero M₁] [has_one M₁] [has_add M₁] [has_smul ℕ M₁]
+  [has_neg M₁] [has_sub M₁] [has_smul ℤ M₁] [has_nat_cast M₁] [has_int_cast M₁]
+  [add_comm_group_with_one M₂] (f : M₁ → M₂) (hf : injective f)
+  (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
+  (neg : ∀ x, f (- x) = - f x) (sub : ∀ x y, f (x - y) = f x - f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) :
+  add_comm_group_with_one M₁ :=
+{ ..hf.add_group_with_one f zero one add neg sub nsmul zsmul nat_cast int_cast,
+  ..hf.add_comm_monoid f zero add nsmul }
+
 end injective
 
 /-!
@@ -395,6 +421,19 @@ protected def comm_monoid [comm_monoid M₁] (f : M₁ → M₂) (hf : surjectiv
   comm_monoid M₂ :=
 { .. hf.comm_semigroup f mul, .. hf.monoid f one mul npow }
 
+/-- A type endowed with `0`, `1` and `+` is an additive monoid with one,
+if it admits a surjective map that preserves `0`, `1` and `*` from an additive monoid with one.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def add_comm_monoid_with_one
+  {M₂} [has_zero M₂] [has_one M₂] [has_add M₂] [has_smul ℕ M₂] [has_nat_cast M₂]
+  [add_comm_monoid_with_one M₁] (f : M₁ → M₂) (hf : surjective f)
+  (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x)
+  (nat_cast : ∀ n : ℕ, f n = n) :
+  add_comm_monoid_with_one M₂ :=
+{ ..hf.add_monoid_with_one f zero one add nsmul nat_cast, ..hf.add_comm_monoid _ zero _ nsmul }
+
 /-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type
 which has an involutive inversion. -/
 @[reducible, to_additive "A type has an involutive negation if it admits a surjective map that
@@ -446,6 +485,7 @@ protected def group [group M₁] (f : M₁ → M₂) (hf : surjective f)
 /-- A type endowed with `0`, `1`, `+` is an additive group with one,
 if it admits a surjective map that preserves `0`, `1`, and `+` to an additive group with one.
 See note [reducible non-instances]. -/
+@[reducible]
 protected def add_group_with_one
   {M₂} [has_zero M₂] [has_one M₂] [has_add M₂] [has_neg M₂] [has_sub M₂]
   [has_smul ℕ M₂] [has_smul ℤ M₂] [has_nat_cast M₂] [has_int_cast M₂]
@@ -475,6 +515,22 @@ protected def comm_group [comm_group M₁] (f : M₁ → M₂) (hf : surjective
   comm_group M₂ :=
 { .. hf.comm_monoid f one mul npow, .. hf.group f one mul inv div npow zpow }
 
+/-- A type endowed with `0`, `1`, `+` is an additive commutative group with one, if it admits a
+surjective map that preserves `0`, `1`, and `+` to an additive commutative group with one.
+See note [reducible non-instances]. -/
+@[reducible]
+protected def add_comm_group_with_one
+  {M₂} [has_zero M₂] [has_one M₂] [has_add M₂] [has_neg M₂] [has_sub M₂]
+  [has_smul ℕ M₂] [has_smul ℤ M₂] [has_nat_cast M₂] [has_int_cast M₂]
+  [add_comm_group_with_one M₁] (f : M₁ → M₂) (hf : surjective f)
+  (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
+  (neg : ∀ x, f (- x) = - f x) (sub : ∀ x y, f (x - y) = f x - f y)
+  (nsmul : ∀ x (n : ℕ), f (n • x) = n • f x) (zsmul : ∀ x (n : ℤ), f (n • x) = n • f x)
+  (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) :
+  add_comm_group_with_one M₂ :=
+{ ..hf.add_group_with_one f zero one add neg sub nsmul zsmul nat_cast int_cast,
+  ..hf.add_comm_monoid _ zero add nsmul }
+
 end surjective
 
 end function

src/algebra/hom/centroid.lean

@@ -9,6 +9,9 @@ import algebra.hom.group_instances
 /-!
 # Centroid homomorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `A` be a (non unital, non associative) algebra. The centroid of `A` is the set of linear maps
 `T` on `A` such that `T` commutes with left and right multiplication, that is to say, for all `a`
 and `b` in `A`,