Merge branch 'master' into bicategory-adjunction

.docker/debian/lean/Dockerfile

@@ -49,7 +49,7 @@ ENTRYPOINT ["/bin/bash", "-l"]
 ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"
 
 # install elan
-RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none && \
     . ~/.profile && \
     elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
 # install leanproject

.docker/gitpod/mathlib/Dockerfile

@@ -14,7 +14,7 @@ WORKDIR /home/gitpod
 SHELL ["/bin/bash", "-c"]
 
 # install elan
-RUN curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
 # install whichever toolchain mathlib is currently using
 RUN . ~/.profile && elan toolchain install $(curl https://raw.githubusercontent.com/leanprover-community/mathlib/master/leanpkg.toml | grep lean_version | awk -F'"' '{print $2}')
 # install `leanproject` using `pip`

.github/workflows/bors.yml

@@ -142,7 +142,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
@@ -179,7 +179,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

.github/workflows/build.yml

@@ -150,7 +150,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
@@ -187,7 +187,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

.github/workflows/build.yml.in

@@ -128,7 +128,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
@@ -165,7 +165,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

.github/workflows/build_fork.yml

@@ -148,7 +148,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
@@ -185,7 +185,7 @@ jobs:
       - name: install elan
         run: |
           set -o pipefail
-          curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 

.github/workflows/dependent-issues.yml

@@ -1,19 +1,8 @@
 name: Dependent Issues
 
 on:
-  issues:
-    types:
-      - opened
-      - edited
-      - reopened
-  pull_request_target:
-    types:
-      - opened
-      - edited
-      - reopened
-      - synchronize
   schedule:
-    - cron: '15 * * * *' # schedule hourly check for external dependencies
+    - cron: '*/15 * * * *' # run every 15 minutes
 
 jobs:
   cancel:
@@ -32,7 +21,7 @@ jobs:
       - uses: z0al/dependent-issues@v1
         env:
           # (Required) The token to use to make API calls to GitHub.
-          GITHUB_TOKEN: ${{ secrets.TRIAGE_TOKEN }}
+          GITHUB_TOKEN: ${{ secrets.DEPENDENT_ISSUES_TOKEN }}
         with:
           # (Optional) The label to use to mark dependent issues
           label: blocked-by-other-PR

.github/workflows/merge_conflicts.yml

@@ -17,4 +17,4 @@ jobs:
         uses: eps1lon/actions-label-merge-conflict@releases/2.x
         with:
           dirtyLabel: "merge-conflict"
-          repoToken: "${{ secrets.TRIAGE_TOKEN }}"
+          repoToken: "${{ secrets.MERGE_CONFLICTS_TOKEN }}"

.gitpod.yml

@@ -6,4 +6,5 @@ vscode:
     - jroesch.lean
 
 tasks:
-  - command: . /home/gitpod/.profile && leanproject get-cache --fallback=download-all
+  - init: leanpkg configure && leanproject get-cache --fallback=download-all
+    command: . /home/gitpod/.profile

CODE_OF_CONDUCT.md

@@ -108,7 +108,7 @@ Violating these terms may lead to a permanent ban.
 ### 4. Permanent Ban
 
 **Community Impact**: Demonstrating a pattern of violation of community
-standards, including sustained inappropriate behavior,  harassment of an
+standards, including sustained inappropriate behavior, harassment of an
 individual, or aggression toward or disparagement of classes of individuals.
 
 **Consequence**: A permanent ban from any sort of public interaction within

archive/100-theorems-list/83_friendship_graphs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark, Kyle Miller
 -/
 import combinatorics.simple_graph.adj_matrix
-import linear_algebra.matrix.charpoly.coeff
+import linear_algebra.matrix.charpoly.finite_field
 import data.int.modeq
 import data.zmod.basic
 import tactic.interval_cases

docs/100.yaml

@@ -211,6 +211,8 @@
   title  : Theorem of Ceva
 62:
   title  : Fair Games Theorem
+  decl   : measure_theory.submartingale_iff_expected_stopped_value_mono
+  author : Kexing Ying
 63:
   title  : Cantor’s Theorem
   decl   : cardinal.cantor

scripts/nolints.txt

@@ -27,26 +27,10 @@ apply_nolint mul_hom.ext_iff to_additive_doc
 apply_nolint one_hom.comp_assoc to_additive_doc
 
 -- algebra/order/group.lean
-apply_nolint inv_le_of_inv_le' to_additive_doc
-apply_nolint inv_lt_of_inv_lt' to_additive_doc
-apply_nolint inv_mul_lt_of_lt_mul to_additive_doc
-apply_nolint inv_of_one_lt_inv to_additive_doc
-apply_nolint le_inv_mul_of_mul_le to_additive_doc
-apply_nolint le_inv_of_le_inv to_additive_doc
-apply_nolint le_one_of_one_le_inv to_additive_doc
 apply_nolint left.inv_le_one_iff to_additive_doc
 apply_nolint left.inv_lt_one_iff to_additive_doc
 apply_nolint left.one_le_inv_iff to_additive_doc
 apply_nolint left.one_lt_inv_iff to_additive_doc
-apply_nolint lt_inv_mul_of_mul_lt to_additive_doc
-apply_nolint lt_inv_of_lt_inv to_additive_doc
-apply_nolint lt_mul_of_inv_mul_lt to_additive_doc
-apply_nolint lt_of_inv_lt_inv to_additive_doc
-apply_nolint mul_le_of_le_inv_mul to_additive_doc
-apply_nolint mul_lt_of_lt_inv_mul to_additive_doc
-apply_nolint one_le_of_inv_le_one to_additive_doc
-apply_nolint one_lt_inv_of_inv to_additive_doc
-apply_nolint one_lt_of_inv_lt_one to_additive_doc
 apply_nolint right.inv_le_one_iff to_additive_doc
 apply_nolint right.one_le_inv_iff to_additive_doc
 
@@ -1084,8 +1068,6 @@ apply_nolint nonarchimedean_group.prod_self_subset to_additive_doc
 apply_nolint nonarchimedean_group.prod_subset to_additive_doc
 
 -- topology/algebra/order/compact.lean
-apply_nolint continuous.bdd_above_range_of_has_compact_mul_support to_additive_doc
-apply_nolint continuous.bdd_below_range_of_has_compact_mul_support to_additive_doc
 apply_nolint continuous.exists_forall_ge_of_has_compact_mul_support to_additive_doc
 apply_nolint continuous.exists_forall_le_of_has_compact_mul_support to_additive_doc
 

src/algebra/algebra/restrict_scalars.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import algebra.algebra.basic
+import algebra.algebra.tower
 
 /-!
 
@@ -16,10 +16,14 @@ typeclass instead.
 ## Main definitions
 
 * `restrict_scalars R S M`: the `S`-module `M` viewed as an `R` module when `S` is an `R`-algebra.
-* `restrict_scalars.linear_equiv : restrict_scalars R S M ≃ₗ[S] M`: the equivalence as an
-  `S`-module between the restricted and origianl space.
-* `restrict_scalars.alg_equiv : restrict_scalars R S A ≃ₐ[S] A`: the equivalence as an `S`-algebra
-   between the restricted and original space.
+  Note that by default we do *not* have a `module S (restrict_scalars R S M)` instance
+  for the original action.
+  This is available as a def `restrict_scalars.module_orig` if really needed.
+* `restrict_scalars.add_equiv : restrict_scalars R S M ≃+ M`: the additive equivalence
+  between the restricted and original space (in fact, they are definitionally equal,
+  but sometimes it is helpful to avoid using this fact, to keep instances from leaking).
+* `restrict_scalars.ring_equiv : restrict_scalars R S A ≃+* A`: the ring equivalence
+   between the restricted and original space when the module is an algebra.
 
 ## See also
 
@@ -76,16 +80,19 @@ instance [I : add_comm_monoid M] : add_comm_monoid (restrict_scalars R S M) := I
 
 instance [I : add_comm_group M] : add_comm_group (restrict_scalars R S M) := I
 
-instance restrict_scalars.module_orig [semiring S] [add_comm_monoid M] [I : module S M] :
+section module
+
+section
+variables [semiring S] [add_comm_monoid M]
+
+/-- We temporarily install an action of the original ring on `restrict_sclars R S M`. -/
+def restrict_scalars.module_orig [I : module S M] :
   module S (restrict_scalars R S M) := I
 
-/-- `restrict_scalars.linear_equiv` is an equivalence of modules over the semiring `S`. -/
-def restrict_scalars.linear_equiv [semiring S] [add_comm_monoid M] [module S M] :
-  restrict_scalars R S M ≃ₗ[S] M :=
-linear_equiv.refl S M
+variables [comm_semiring R] [algebra R S] [module S M]
 
-section module
-variables [semiring S] [add_comm_monoid M] [comm_semiring R] [algebra R S] [module S M]
+section
+local attribute [instance] restrict_scalars.module_orig
 
 /--
 When `M` is a module over a ring `S`, and `S` is an algebra over `R`, then `M` inherits a
@@ -96,17 +103,44 @@ The preferred way of setting this up is `[module R M] [module S M] [is_scalar_to
 instance : module R (restrict_scalars R S M) :=
 module.comp_hom M (algebra_map R S)
 
+/--
+This instance is only relevant when `restrict_scalars.module_orig` is available as an instance.
+-/
+instance : is_scalar_tower R S (restrict_scalars R S M) :=
+⟨λ r S M, by { rw [algebra.smul_def, mul_smul], refl }⟩
+
+end
+
+/--
+The `R`-algebra homomorphism from the original coefficient algebra `S` to endomorphisms
+of `restrict_scalars R S M`.
+-/
+def restrict_scalars.lsmul : S →ₐ[R] module.End R (restrict_scalars R S M) :=
+begin
+  -- We use `restrict_scalars.module_orig` in the implementation,
+  -- but not in the type.
+  letI : module S (restrict_scalars R S M) := restrict_scalars.module_orig R S M,
+  exact algebra.lsmul R (restrict_scalars R S M),
+end
+
+end
+
+variables [add_comm_monoid M]
+
+/-- `restrict_scalars.add_equiv` is the additive equivalence with the original module. -/
+@[simps] def restrict_scalars.add_equiv : restrict_scalars R S M ≃+ M :=
+add_equiv.refl M
+
+variables [comm_semiring R] [semiring S] [algebra R S] [module S M]
+
 lemma restrict_scalars_smul_def (c : R) (x : restrict_scalars R S M) :
   c • x = ((algebra_map R S c) • x : M) := rfl
 
-@[simp] lemma restrict_scalars.linear_equiv_map_smul (t : R) (x : restrict_scalars R S M) :
-  restrict_scalars.linear_equiv R S M (t • x)
-  = (algebra_map R S t) • restrict_scalars.linear_equiv R S M x :=
+@[simp] lemma restrict_scalars.add_equiv_map_smul (t : R) (x : restrict_scalars R S M) :
+  restrict_scalars.add_equiv R S M (t • x)
+  = (algebra_map R S t) • restrict_scalars.add_equiv R S M x :=
 rfl
 
-instance : is_scalar_tower R S (restrict_scalars R S M) :=
-⟨λ r S M, by { rw [algebra.smul_def, mul_smul], refl }⟩
-
 end module
 
 section algebra
@@ -116,16 +150,17 @@ instance [I : ring A] : ring (restrict_scalars R S A) := I
 instance [I : comm_semiring A] : comm_semiring (restrict_scalars R S A) := I
 instance [I : comm_ring A] : comm_ring (restrict_scalars R S A) := I
 
-variables [comm_semiring S] [semiring A]
-
-instance restrict_scalars.algebra_orig [I : algebra S A] : algebra S (restrict_scalars R S A) := I
+variables [semiring A]
 
-variables [algebra S A]
+/-- Tautological ring isomorphism `restrict_scalars R S A ≃+* A`. -/
+def restrict_scalars.ring_equiv : restrict_scalars R S A ≃+* A := ring_equiv.refl _
 
-/-- Tautological `S`-algebra isomorphism `restrict_scalars R S A ≃ₐ[S] A`. -/
-def restrict_scalars.alg_equiv : restrict_scalars R S A ≃ₐ[S] A := alg_equiv.refl
+variables [comm_semiring S] [algebra S A] [comm_semiring R] [algebra R S]
 
-variables [comm_semiring R] [algebra R S]
+@[simp] lemma restrict_scalars.ring_equiv_map_smul (r : R) (x : restrict_scalars R S A) :
+  restrict_scalars.ring_equiv R S A (r • x)
+  = (algebra_map R S r) • restrict_scalars.ring_equiv R S A x :=
+rfl
 
 /-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/
 instance : algebra R (restrict_scalars R S A) :=
@@ -134,4 +169,9 @@ instance : algebra R (restrict_scalars R S A) :=
   smul_def' := λ _ _, algebra.smul_def _ _,
   .. (algebra_map S A).comp (algebra_map R S) }
 
+@[simp] lemma restrict_scalars.ring_equiv_algebra_map (r : R) :
+  restrict_scalars.ring_equiv R S A (algebra_map R (restrict_scalars R S A) r) =
+    algebra_map S A (algebra_map R S r) :=
+rfl
+
 end algebra