FLT/Mathlib/LinearAlgebra/Pi.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. class Pi.FiberwiseSMul A class encoding the product scalar multiplication of ∀ b : β, R b on ∀ a : α, M a that is determined by the fibers of a supplied function f : α → β on indices line 23 source

   Source documentation

   A class encoding the product scalar multiplication of ∀ b : β, R b on ∀ a : α, M a that is determined by the fibers of a supplied function f : α → β on indices. Specifically, if f a = b, then (r • x) a = r b • x a for any r : ∀ b, R b and x : ∀ a, M a.

   standard axioms: Quot.sound what this means

   Statement uses: Semiring, AddCommMonoid, Subtype, Eq, Module

   3 instances, coercions and auxiliary constants left out.

   class Pi.FiberwiseSMul {α β : Type*} (f : α → β) (R : β → Type*) (M : α → Type*)
       [(b : β) → Semiring (R b)] [(a : α) → AddCommMonoid (M a)]
       [(b : β) → (σ : {a // f a = b}) → Module (R b) (M σ)]
       [Module ((b : β) → R b) ((a : α) → M a)] : Prop where
   …

2. def LinearEquiv.piScalarPiCongrFiberwise Let f : α → β be a function on index types line 35 source

   Source documentation

   Let f : α → β be a function on index types. A family of R b-linear equivalences, indexed by b : β, between the product over the fiber of b under f given as ∀ (σ : { a : α // f a = b }) → γ₁ σ.1) ≃ₗ[R b] γ₂ b lifts to an equivalence over the products ∀ a, γ₁ a ≃ₗ[∀ b, R b] ∀ b, γ₂ b with product scalars ∀ b, R b, provided that ∀ b, R b acts on ∀ a, γ₁ a fiberwise. This is Equiv.piCongrFiberwise as a LinearEquiv with product scalars.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Semiring, AddCommMonoid, Subtype, Eq, Module, Pi.FiberwiseSMul, LinearEquiv, RingHom.id

   Proof uses: Equiv, Equiv.piCongrFiberwise, LinearEquiv.toEquiv, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, Equiv.invFun

   24 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

   Open to load the checked before-and-after goal states.

   def LinearEquiv.piScalarPiCongrFiberwise {α : Type*} {β : Type*} {R : β → Type*} {γ₁ : α → Type*}
       {γ₂ : β → Type*} {f : α → β} [(b : β) → Semiring (R b)] [(a : α) → AddCommMonoid (γ₁ a)]
       [(b : β) → AddCommMonoid (γ₂ b)] [(b : β) → (a : { a : α // f a = b }) → Module (R b) (γ₁ a)]
       [(b : β) → Module (R b) (γ₂ b)] [Module (∀ b, R b) (∀ a, γ₁ a)] [Pi.FiberwiseSMul f R γ₁]
       (e : (b : β) → ((σ : { a : α // f a = b }) → γ₁ σ.1) ≃ₗ[R b] γ₂ b) :
       ((a : α) → γ₁ a) ≃ₗ[∀ b, R b] ((b : β) → γ₂ b) where
   …

   Mentions: Pi.FiberwiseSMul

3. def LinearEquiv.piScalarPiComm Documented declaration: piScalarPiComm line 48 source

   Source documentation

   Given φ : α → β → Type* and R : α → Type* such that φ a b is an R a module for all a b, this is the linear equivalence between ∀ a b, φ a b and ∀ b a, φ a b with product scalars. This is Equiv.piComm as a product-scalar LinearEquiv.

   standard axioms: Quot.sound, propext what this means

   Statement uses: Semiring, AddCommMonoid, Module, LinearEquiv, RingHom.id

   Proof uses: Equiv, Equiv.piComm, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Equiv.toFun, Equiv.invFun

   21 instances, coercions and auxiliary constants left out.

   def LinearEquiv.piScalarPiComm {α β : Type*} (R : α → Type*) (φ : α → β → Type*)
       [∀ a, Semiring (R a)] [∀ a b, AddCommMonoid (φ a b)] [∀ a b, Module (R a) (φ a b)] :
       ((a : α) → (b : β) → φ a b) ≃ₗ[∀ a, R a] ((b : β) → (a : α) → φ a b) where
   …

4. class Prod.IsProdSMul A class encoding the product scalar multiplication of R × S on M × N of the format x • y = (x.1 • y.1, x.2 • y.2) line 58 source

   Source documentation

   A class encoding the product scalar multiplication of R × S on M × N of the format x • y = (x.1 • y.1, x.2 • y.2). Use this as an assumption instead of constructing the R × S action on M × N.

   no axioms what this means

   Statement uses: SMul, Prod

   class Prod.IsProdSMul (R S M N : Type*) [SMul R M] [SMul S N] [SMul (R × S) (M × N)] : Prop where
   …

5. theorem Prod.IsProdSMul.smul_fst line 61 source

   no axioms what this means

   Statement uses: SMul, Prod, Prod.IsProdSMul, Eq, Prod.fst, HSMul.hSMul

   Proof uses: Eq.mpr, Prod.mk, Prod.snd, id, congrArg, Prod.IsProdSMul.map_smul, Eq.refl

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

6. theorem Prod.IsProdSMul.smul_snd line 65 source

   no axioms what this means

   Statement uses: SMul, Prod, Prod.IsProdSMul, Eq, Prod.snd, HSMul.hSMul

   Proof uses: Eq.mpr, Prod.mk, Prod.fst, id, congrArg, Prod.IsProdSMul.map_smul, Eq.refl

   2 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

7. class RestrictedProduct.FiberwiseSMul Documented declaration: FiberwiseSMul line 74 source

   Source documentation

   A class encoding the product scalar multiplication of Πʳ b, [R b, A b]_[𝓕] on Πʳ a, [M a, B a]_[𝓖] that is determined by the fibers of a supplied function f : α → β on indices. Specifically, if f a = b, then (r • x) a = r b • x a for any r : ∀ b, R b and x : ∀ a, M a. This is Pi.FiberwiseSMul for restricted products.

   no axioms what this means

   Statement uses: Set, Filter, Subtype, Eq, SMul, RestrictedProduct

   1 instances, coercions and auxiliary constants left out.

   class RestrictedProduct.FiberwiseSMul {α β : Type*} (f : α → β) (R : (b : β) → Type*)
       (A : (b : β) → Set (R b)) (𝓕 : Filter β) (M : (a : α) → Type*) (B : (a : α) → Set (M a))
       (𝓖 : Filter α) [(b : β) → (σ : { a // f a = b }) → SMul (R b) (M ↑σ)]
       [SMul (Πʳ b, [R b, A b]_[𝓕]) (Πʳ a, [M a, B a]_[𝓖])] : Prop where
   …