FLT/Mathlib/Topology/Algebra/Module/Equiv.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def ContinuousLinearEquiv.piScalarPiCongrFiberwise Let f : α → β be a function on index types line 30 source

   Source documentation

   Let f : α → β be a function on index types. A family of R b-linear homeomorphisms, 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 ContinuousLinearEquiv with product scalars.

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

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

   Proof uses: LinearEquiv, LinearEquiv.piScalarPiCongrFiberwise, ContinuousLinearEquiv.mk

   22 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

   def ContinuousLinearEquiv.piScalarPiCongrFiberwise {α : Type*} {β : Type*} {R : β → Type*}
       {γ₁ : α → Type*} {γ₂ : β → Type*} {f : α → β} [(a : α) → TopologicalSpace (γ₁ a)]
       [(b : β) → TopologicalSpace (γ₂ b)] [(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) ≃L[R b] γ₂ b) :
       ((a : α) → γ₁ a) ≃L[∀ b, R b] ((b : β) → γ₂ b) where
   …

   Mentions: Pi.FiberwiseSMul

2. def ContinuousLinearEquiv.piScalarPiComm Documented declaration: piScalarPiComm line 50 source

   Source documentation

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

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

   Statement uses: Semiring, AddCommMonoid, Module, TopologicalSpace, ContinuousLinearEquiv, RingHom.id

   Proof uses: LinearEquiv, LinearEquiv.piScalarPiComm, ContinuousLinearEquiv.mk

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 4 steps

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

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

3. lemma ContinuousLinearEquiv.toContinuousAddEquiv_trans line 62 source

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

   Statement uses: Semiring, AddCommMonoid, Module, TopologicalSpace, ContinuousLinearEquiv, RingHom.id, Eq, ContinuousAddEquiv, ContinuousLinearEquiv.toContinuousAddEquiv, ContinuousLinearEquiv.trans, ContinuousAddEquiv.trans

   Proof uses: rfl

   12 instances, coercions and auxiliary constants left out.

4. lemma ContinuousLinearEquiv.toMatrix_isUnit_det line 68 source

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

   Statement uses: CommRing, Fintype, DecidableEq, AddCommGroup, Module, TopologicalSpace, Module.Basis, ContinuousLinearEquiv, RingHom.id, IsUnit, Matrix.det, LinearEquiv, LinearMap, Matrix, LinearMap.toMatrix

   Proof uses: LinearEquiv.isUnit_det

   30 instances, coercions and auxiliary constants left out.

5. lemma ContinuousLinearEquiv.toMatrix_isUnit line 74 source

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

   Statement uses: CommRing, Fintype, DecidableEq, AddCommGroup, Module, TopologicalSpace, Module.Basis, ContinuousLinearEquiv, RingHom.id, IsUnit, Matrix, LinearEquiv, LinearMap, LinearMap.toMatrix

   Proof uses: Iff.mpr, Matrix.det, Matrix.isUnit_iff_isUnit_det, ContinuousLinearEquiv.toMatrix_isUnit_det

   50 instances, coercions and auxiliary constants left out.

6. lemma ContinuousLinearEquiv.toMatrix_det_ne_zero line 82 source

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

   Statement uses: CommRing, Nontrivial, Fintype, DecidableEq, AddCommGroup, Module, TopologicalSpace, Module.Basis, ContinuousLinearEquiv, RingHom.id, Ne, Matrix.det, LinearEquiv, LinearMap, Matrix, LinearMap.toMatrix, OfNat.ofNat

   Proof uses: IsUnit.ne_zero, ContinuousLinearEquiv.toMatrix_isUnit_det

   50 instances, coercions and auxiliary constants left out.

7. def Matrix.toContinuousLinearEquiv Given M : Matrix ι ι F, b : Module.Basis ι F V and h : M.det ≠ 0, this is the continuous linear equivalence arising from Matrix.toLinearEquiv b M (Ne.isUnit h) line 101 source

   Source documentation

   Given M : Matrix ι ι F, b : Module.Basis ι F V and h : M.det ≠ 0, this is the continuous linear equivalence arising from Matrix.toLinearEquiv b M (Ne.isUnit h)

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

   Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Matrix, Module.Basis, IsUnit, Matrix.det, ContinuousLinearEquiv, RingHom.id

   Proof uses: LinearEquiv, Matrix.toLinearEquiv, Continuous, LinearEquiv.symm, ContinuousLinearEquiv.mk

   43 instances, coercions and auxiliary constants left out.

   noncomputable def toContinuousLinearEquiv
       (M : Matrix ι ι F) (b : Module.Basis ι F V) (h : IsUnit M.det) : V ≃L[F] V :=
   …

8. lemma Matrix.toContinousLinearEquiv_apply line 111 source

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

   Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Matrix, Module.Basis, IsUnit, Matrix.det, Eq, ContinuousLinearEquiv, RingHom.id, Matrix.toContinuousLinearEquiv, LinearMap, LinearEquiv, Matrix.toLin

   Proof uses: rfl

   58 instances, coercions and auxiliary constants left out.

9. lemma Matrix.toContinuousLinearEquiv_toLin_coe line 116 source

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

   Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Matrix, Module.Basis, IsUnit, Matrix.det, Eq, ContinuousLinearEquiv, RingHom.id, Matrix.toContinuousLinearEquiv, LinearMap, LinearEquiv, Matrix.toLin

   Proof uses: rfl

   58 instances, coercions and auxiliary constants left out.

10. lemma Matrix.toContinuousLinearEquiv_toLinearEquiv line 121 source

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

    Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Module.Basis, Matrix, IsUnit, Matrix.det, Eq, LinearEquiv, RingHom.id, Matrix.toContinuousLinearEquiv, Matrix.toLinearEquiv

    Proof uses: rfl

    40 instances, coercions and auxiliary constants left out.

11. lemma Matrix.toContinousLinearEquiv_toMatrix line 125 source

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

    Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Module.Basis, Matrix, IsUnit, Matrix.det, Eq, LinearEquiv, RingHom.id, LinearMap, LinearMap.toMatrix, Matrix.toContinuousLinearEquiv

    Proof uses: Iff.mp, LinearEquiv.symm, LinearEquiv.eq_symm_apply, rfl

    72 instances, coercions and auxiliary constants left out.

12. lemma Matrix.toContinousLinearEquiv_mul line 130 source

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

    Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Module.Basis, Matrix, IsUnit, Matrix.det, HMul.hMul, Eq, ContinuousLinearEquiv, RingHom.id, Matrix.toContinuousLinearEquiv, ContinuousLinearEquiv.trans

    Proof uses: ContinuousLinearEquiv.ext, funext, of_eq_true, LinearMap, LinearEquiv, Matrix.toLin, Eq.trans, True, congrFun', congrArg, LinearMap.comp, AddCommMonoid, Finite, Matrix.toLin_mul, eq_self

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

13. lemma ContinuousLinearEquiv.toMatrix_toContinousLinearEquiv line 141 source

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

    Statement uses: CommRing, TopologicalSpace, Fintype, DecidableEq, AddCommGroup, Module, IsModuleTopology, ContinuousAdd, Module.Basis, ContinuousLinearEquiv, RingHom.id, Eq, Matrix.toContinuousLinearEquiv, LinearEquiv, LinearMap, Matrix, LinearMap.toMatrix, ContinuousLinearEquiv.toMatrix_isUnit_det

    Proof uses: ContinuousLinearEquiv.ext, funext, of_eq_true, Eq.trans, True, congrFun', congrArg, Matrix.toLin, Matrix.toLin_toMatrix, eq_self

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

14. theorem ContinuousLinearEquiv.toContinuousAddEquiv_apply line 148 source

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

    Statement uses: Semiring, TopologicalSpace, AddCommMonoid, Module, ContinuousLinearEquiv, RingHom.id, Eq, ContinuousAddEquiv, ContinuousLinearEquiv.toContinuousAddEquiv

    Proof uses: rfl

    17 instances, coercions and auxiliary constants left out.