Lemmas for Mathlib #

These are small lemmas that can be immediatly PR'ed to Mathlib.

source

@[simp]

theorem comp_vecCons {α : Type u_1} {β : Type u_2} {n : ℕ} (f : Fin n → α) (x : α) (g : α → β) :

g ∘ Matrix.vecCons x f = Matrix.vecCons (g x) (g ∘ f)

source

@[simp]

theorem comp_vecEmpty {α : Type u_1} {β : Type u_2} {g : α → β} :

g ∘ ![] = ![]

source

theorem Fin.apply_append_apply {M : Type u_1} {i j : ℕ} (f : Fin i → M) (g : Fin j → M) {N : Type u_2} (v : M → N) (p : Fin (i + j)) :

v (append f g p) = append (v ∘ f) (v ∘ g) p

source

theorem Fin.comp_append {M : Type u_1} {i j : ℕ} (f : Fin i → M) (g : Fin j → M) {N : Type u_2} (v : M → N) :

v ∘ append f g = append (v ∘ f) (v ∘ g)

source

@[simp]

theorem Fin.append_update_left {M : Type u_1} {i j : ℕ} (f : Fin i → M) (g : Fin j → M) (c : Fin i) (x : M) [DecidableEq (Fin i)] [DecidableEq (Fin (i + j))] :

append (Function.update f c x) g = Function.update (append f g) (castAdd j c) x

source

@[simp]

theorem Fin.append_update_right {M : Type u_1} {i j : ℕ} (f : Fin i → M) (g : Fin j → M) (c : Fin j) (x : M) [DecidableEq (Fin j)] [DecidableEq (Fin (i + j))] :

append f (Function.update g c x) = Function.update (append f g) (natAdd i c) x

source

theorem Fin.lastCases_update_left {n : ℕ} {M : Fin (n + 1) → Type u_2} (p q : M (last n)) (v : (i : Fin n) → M i.castSucc) (j : Fin (n + 1)) :

lastCases p v j = Function.update (fun (i : Fin (n + 1)) => lastCases q v i) (last n) p j

source

@[simp]

theorem Fin.update_last {n : ℕ} [DecidableEq (Fin (n + 1))] {M : Fin (n + 1) → Type u_2} (v : (i : Fin (n + 1)) → M i) (i : Fin n) (x : M i.castSucc) :

Function.update v i.castSucc x (last n) = v (last n)

source

@[simp]

theorem Fin.update_castSucc {n : ℕ} [DecidableEq (Fin (n + 1))] {M : Fin (n + 1) → Type u_2} (v : (i : Fin (n + 1)) → M i) (i : Fin n) (x : M i.castSucc) (j : Fin n) :

Function.update v i.castSucc x j.castSucc = Function.update (fun (c : Fin n) => v c.castSucc) i x j

source

@[simp]

theorem Fin.lastCases_update_right {n : ℕ} [DecidableEq (Fin n)] {M : Fin (n + 1) → Type u_2} (p : M (last n)) (v : (i : Fin n) → M i.castSucc) (i : Fin n) (x : M i.castSucc) (j : Fin (n + 1)) :

lastCases p (Function.update v i x) j = Function.update (fun (i : Fin (n + 1)) => lastCases p v i) i.castSucc x j

source

@[simp]

theorem Fin.lastCases_last_castSucc {n : ℕ} {M : Fin (n + 1) → Type u_2} (v : (i : Fin (n + 1)) → M i) :

(fun (i : Fin (n + 1)) => lastCases (v (last n)) (fun (i : Fin n) => v i.castSucc) i) = v

source

def Fin.permAdd {i j : ℕ} (e₁ : Equiv.Perm (Fin i)) (e₂ : Equiv.Perm (Fin j)) :

Equiv.Perm (Fin (i + j))

Equations

Fin.permAdd e₁ e₂ = finSumFinEquiv.permCongr (e₁.sumCongr e₂)

Instances For

source

@[simp]

theorem Fin.permAdd_left {i j : ℕ} (e₁ : Equiv.Perm (Fin i)) (e₂ : Equiv.Perm (Fin j)) (x : Fin i) :

(permAdd e₁ e₂) (castAdd j x) = castAdd j (e₁ x)

source

@[simp]

theorem Fin.permAdd_right {i j : ℕ} (e₁ : Equiv.Perm (Fin i)) (e₂ : Equiv.Perm (Fin j)) (x : Fin j) :

(permAdd e₁ e₂) (natAdd i x) = natAdd i (e₂ x)

source

theorem Finsupp.image_lift (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {X : Type u_3} (f : X → M) :

LinearMap.range ((lift M R X) f) = Submodule.span R (Set.range f)

source

theorem Finsupp.lift_surjective_iff (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {X : Type u_3} (f : X → M) :

Function.Surjective ⇑((lift M R X) f) ↔ Submodule.span R (Set.range f) = ⊤

source

theorem Finsupp.lift_surjective_iff' (R : Type u_1) [Semiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (s : Set M) :

Function.Surjective ⇑((lift M R ↑s) Subtype.val) ↔ Submodule.span R s = ⊤

s spans a module M iff the corresponding map from s →₀ R is surjective.

source

theorem MultilinearMap.hom_ext {R : Type u_1} {ι : Type u_2} {N : Type u_3} [CommSemiring R] [Finite ι] {M : ι → Type u_4} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] {f g : MultilinearMap R M N} (s : (i : ι) → Set (M i)) (span : ∀ (i : ι), Submodule.span R (s i) = ⊤) (h : ∀ (v : (i : ι) → ↑(s i)), (f fun (i : ι) => ↑(v i)) = g fun (i : ι) => ↑(v i)) :

f = g

source

theorem MultilinearMap.hom_ext' {R : Type u_1} {ι : Type u_2} {N : Type u_3} [CommSemiring R] [Finite ι] {M : ι → Type u_4} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] {f g : MultilinearMap R M N} (X : ι → Type u_5) (s : (i : ι) → X i → M i) (span : ∀ (i : ι), Submodule.span R (Set.range (s i)) = ⊤) (h : ∀ (v : (i : ι) → X i), (f fun (i : ι) => s i (v i)) = g fun (i : ι) => s i (v i)) :

f = g

source

theorem MultilinearMap.hom_ext₂ {R : Type u_1} {ι : Type u_2} {N : Type u_3} [CommSemiring R] [Finite ι] {M : ι → Type u_4} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] {f g : MultilinearMap R M N} (X : ι → Type u_5) (Y : ι → Type u_6) (s : (i : ι) → X i → Y i → M i) (span : ∀ (i : ι), Submodule.span R {t : M i | ∃ (m : X i) (n : Y i), s i m n = t} = ⊤) (h : ∀ (v : (i : ι) → X i) (w : (i : ι) → Y i), (f fun (i : ι) => s i (v i) (w i)) = g fun (i : ι) => s i (v i) (w i)) :

f = g

source

@[simp]

theorem TensorProduct.span_mk_one_eq_top {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :

Submodule.span A (Set.range ⇑((mk R A M) 1)) = ⊤

source

noncomputable def Submodule.quotientComapLinearEquiv {R : Type u_1} [Ring R] {M₁ : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (hf : Function.Surjective ⇑f) (N : Submodule R M₂) :

(M₁ ⧸ comap f N) ≃ₗ[R] M₂ ⧸ N

Equations

Submodule.quotientComapLinearEquiv f hf N = LinearEquiv.ofBijective ((Submodule.comap f N).mapQ N f ⋯) ⋯

Instances For

source

@[simp]

theorem Submodule.quotientComapLinearEquiv_apply {R : Type u_1} [Ring R] {M₁ : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (hf : Function.Surjective ⇑f) (N : Submodule R M₂) (a✝ : M₁ ⧸ comap f N) :

(quotientComapLinearEquiv f hf N) a✝ = ((comap f N).mapQ N f ⋯) a✝

source

@[simp]

theorem Submodule.quotientComapLinearEquiv_symm_apply {R : Type u_1} [Ring R] {M₁ : Type u_2} {M₂ : Type u_3} [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (hf : Function.Surjective ⇑f) (N : Submodule R M₂) (a✝ : M₂ ⧸ N) :

(quotientComapLinearEquiv f hf N).symm a✝ = (LinearEquiv.ofInjective ((comap f N).mapQ N f ⋯) ⋯).symm ((LinearEquiv.ofTop (LinearMap.range ((comap f N).mapQ N f ⋯)) ⋯).symm a✝)

source

@[simp]

theorem LinearEquiv.baseChange_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (a : A) (m : M) :

(baseChange R A M N e) (a ⊗ₜ[R] m) = a ⊗ₜ[R] e m

source

noncomputable def Submodule.quotientBaseChange {R : Type u} {M : Type v} (A : Type w) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (S : Submodule R M) :

(TensorProduct R A M ⧸ baseChange A S) ≃ₗ[A] TensorProduct R A (M ⧸ S)

Equations

Submodule.quotientBaseChange A S = ⋯.linearEquivOfSurjective ⋯

Instances For

source

@[simp]

theorem Submodule.quotientBaseChange_apply {R : Type u} {M : Type v} (A : Type w) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (S : Submodule R M) (a : A) (m : M) :

(quotientBaseChange A S) (Quotient.mk (a ⊗ₜ[R] m)) = a ⊗ₜ[R] Quotient.mk m

source

@[simp]

theorem Submodule.quotientBaseChange_symm_apply {R : Type u} {M : Type v} (A : Type w) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (S : Submodule R M) (a : A) (m : M) :

(quotientBaseChange A S).symm (a ⊗ₜ[R] Quotient.mk m) = Quotient.mk (a ⊗ₜ[R] m)

source

@[simp]

theorem Submodule.quotientBaseChange_comp_baseChange_mkQ {R : Type u} {M : Type v} (A : Type w) [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (S : Submodule R M) :

↑(quotientBaseChange A S) ∘ₗ (baseChange A S).mkQ = LinearMap.baseChange A S.mkQ

source

theorem AlgebraTensorModule.cancelBaseChange_comp_mk_one {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring B] [AddCommMonoid M] [Module R M] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] :

↑R ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M) ∘ₗ ↑R ((TensorProduct.mk A B (TensorProduct R A M)) 1) = LinearMap.rTensor M (IsScalarTower.toAlgHom R A B).toLinearMap

The triangle of R-modules A ⊗[R] M ⟶ B ⊗[A] (A ⊗[R] M) ⟶ B ⊗[R] M commutes.

source

theorem AlgebraTensorModule.cancelBaseChange_comp_mk_one' {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring B] [AddCommMonoid M] [Module R M] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] :

↑R (↑A ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M) ∘ₗ (TensorProduct.mk A B (TensorProduct R A M)) 1) = LinearMap.rTensor M (IsScalarTower.toAlgHom R A B).toLinearMap

The triangle of R-modules A ⊗[R] M ⟶ B ⊗[A] (A ⊗[R] M) ⟶ B ⊗[R] M commutes.

source

theorem AlgebraTensorModule.coe_cancelBaseChange_comp_mk_one {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [CommSemiring R] [CommSemiring A] [Semiring B] [AddCommMonoid M] [Module R M] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] :

⇑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B B M) ∘ ⇑((TensorProduct.mk A B (TensorProduct R A M)) 1) = ⇑(LinearMap.rTensor M (IsScalarTower.toAlgHom R A B).toLinearMap)

The triangle of R-modules A ⊗[R] M ⟶ B ⊗[A] (A ⊗[R] M) ⟶ B ⊗[R] M commutes.

source

theorem LinearMap.restrictScalars_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) :

↑R (baseChange A f) = lTensor A f

source

@[simp]

theorem LinearMap.quotKerEquivOfSurjective_apply {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (f : M →ₗ[R] M₂) (hf : Function.Surjective ⇑f) (x : M) :

(f.quotKerEquivOfSurjective hf) (Submodule.Quotient.mk x) = f x

source

theorem LinearEquiv.piRing_symm_apply_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} {S : Type u_4} [Semiring R] [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : ι → M) (i : ι) (r : R) :

((piRing R M ι S).symm f) (Pi.single i r) = r • f i

source

theorem LinearEquiv.piRing_symm_apply_single_one {R : Type u_1} {M : Type u_2} {ι : Type u_3} {S : Type u_4} [Semiring R] [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] (f : ι → M) (i : ι) :

((piRing R M ι S).symm f) (Pi.single i 1) = f i

source

theorem SMulCommClass.isScalarTower (R₁ : Type u) (R : Type v) [Monoid R₁] [CommMonoid R] [MulAction R₁ R] [SMulCommClass R₁ R R] :

IsScalarTower R₁ R R

Documentation

EllipticCurve.Lemmas

Lemmas for Mathlib #