FLT/DedekindDomain/FiniteAdeleRing/TensorPi.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

9 declarations, 0 contain sorry, 0 declared as axioms

Tensor product commutes with direct product when tensoring with a finite free module

If M is a finite free module and Nᵢ is an indexed collection of modules of a commutative ring R then there is an R-module isomorphism between M ⊗ ∏ᵢ Nᵢ and ∏ᵢ (M ⊗ Nᵢ).

Main definition

TODO

Switch the names around because the primed version is more general hence better.

Imports (3)
Imported by 3 files
  1. theorem Module.FinitePresentation.exists_fin_exact line 34 source

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

    Statement uses: Ring, AddCommGroup, Module, Module.FinitePresentation, Exists, Nat, LinearMap, RingHom.id, Fin, And, Function.Exact, Function.Surjective

    Proof uses: Submodule, LinearEquiv, HasQuotient.Quotient, Submodule.FG, Module.FinitePresentation.exists_fin, Finset, Eq, Submodule.span, Finset.card, Function.comp, Subtype, Membership.mem, Equiv, Equiv.symm, Finset.equivFin, Fintype.linearCombination, LinearMap.comp, LinearEquiv.symm, Submodule.mkQ, LinearMap.range and 22 more

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  2. def directSumPiEquivPiSum ⨁ⱼ(∏ᵢ Nᵢⱼ) ≅ ∏ᵢ(⨁ⱼNᵢⱼ) if j ranges over a finite index set and i over an arbitrary index set line 65 source

    Source documentation

    ⨁ⱼ(∏ᵢ Nᵢⱼ) ≅ ∏ᵢ(⨁ⱼNᵢⱼ) if j ranges over a finite index set and i over an arbitrary index set. This variant is for R-modules and gives an R-module isomorphism.

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

    Statement uses: Fintype, DecidableEq, Semiring, AddCommMonoid, Module, LinearEquiv, RingHom.id, DirectSum

    Proof uses: LinearEquiv.mk, LinearMap.mk, AddHom.mk, Finset.sum, Finset.univ, AddMonoidHom, DirectSum.of, DFinsupp

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

    def directSumPiEquivPiSum : (⨁ (i' : ι'), (∀ i, N i i')) ≃ₗ[R] (∀ i, (⨁ i', N i i')) where
…
  3. def freeModuleTensorPiEquiv The isomorphism M ⊗ ∏ᵢ Nᵢ ≅ (B →₀ R) ⊗ ∏ᵢ Nᵢ, where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator line 111 source

    Source documentation

    The isomorphism M ⊗ ∏ᵢ Nᵢ ≅ (B →₀ R) ⊗ ∏ᵢ Nᵢ, where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator. This is an auxiliary definition.

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

    Statement uses: CommRing, AddCommGroup, Module, Module.Free, LinearEquiv, RingHom.id, TensorProduct, Finsupp, Module.Free.ChooseBasisIndex

    Proof uses: TensorProduct.congr, Module.Basis.repr, Module.Free.chooseBasis, LinearEquiv.refl

    28 instances, coercions and auxiliary constants left out.

    noncomputable def freeModuleTensorPiEquiv :
    M ⊗[R] (∀ i, N i) ≃ₗ[R] (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] (∀ i, N i) :=
…
  4. def finsuppLeftTensorPiEquivPiTensor If B is finite then tensoring by the free module with basis B commutes with arbitrary products line 117 source

    Source documentation

    If B is finite then tensoring by the free module with basis B commutes with arbitrary products.

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

    Statement uses: CommRing, AddCommGroup, Module, Fintype, DecidableEq, LinearEquiv, RingHom.id, TensorProduct, Finsupp

    Proof uses: LinearEquiv.trans, DirectSum, TensorProduct.finsuppScalarLeft, finsuppLEquivDirectSum, directSumPiEquivPiSum, LinearEquiv.piCongrRight, LinearEquiv.symm

    37 instances, coercions and auxiliary constants left out.

    noncomputable def finsuppLeftTensorPiEquivPiTensor (B : Type*) [Fintype B] [DecidableEq B] :
    (B →₀ R) ⊗[R] (Π i, N i) ≃ₗ[R] Π i, (B →₀ R) ⊗[R] (N i) :=
…
  5. def tensorPiEquivFinitefreeModule The isomorphism Πᵢ ((B →₀ R) ⊗ Nᵢ) ≅ Πᵢ (M ⊗ Nᵢ) where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator line 133 source

    Source documentation

    The isomorphism Πᵢ ((B →₀ R) ⊗ Nᵢ) ≅ Πᵢ (M ⊗ Nᵢ) where M is assumed free and B is the basis of M given by Lean's global axiom-of-choice operator. This is an auxiliary definition.

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

    Statement uses: CommRing, AddCommGroup, Module, Module.Free, LinearEquiv, RingHom.id, TensorProduct, Finsupp, Module.Free.ChooseBasisIndex

    Proof uses: LinearEquiv.piCongrRight, LinearEquiv.rTensor, LinearEquiv.symm, Module.Basis.repr, Module.Free.chooseBasis

    28 instances, coercions and auxiliary constants left out.

    noncomputable def tensorPiEquivFinitefreeModule :
    (Π i, (Module.Free.ChooseBasisIndex R M →₀ R) ⊗[R] N i) ≃ₗ[R] Π i, (M ⊗[R] N i) :=
…
  6. def tensorPiEquivPiTensor Tensoring with a finite free module commutes with arbitrary products line 139 source

    Source documentation

    Tensoring with a finite free module commutes with arbitrary products.

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

    Statement uses: CommRing, AddCommGroup, Module, Module.Free, Module.Finite, LinearEquiv, RingHom.id, TensorProduct

    Proof uses: LinearEquiv.trans, Finsupp, Module.Free.ChooseBasisIndex, freeModuleTensorPiEquiv, finsuppLeftTensorPiEquivPiTensor, tensorPiEquivFinitefreeModule

    27 instances, coercions and auxiliary constants left out.

    noncomputable def tensorPiEquivPiTensor :
    M ⊗[R] (Π i, N i) ≃ₗ[R] Π i, (M ⊗[R] N i) :=
…
  7. lemma tensorPi_equiv_piTensor_apply line 148 source

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

    Statement uses: CommRing, AddCommGroup, Module, Module.Free, Module.Finite, Eq, TensorProduct, LinearEquiv, RingHom.id, tensorPiEquivPiTensor, TensorProduct.tmul

    Proof uses: id, LinearEquiv.trans, Finsupp, Module.Free.ChooseBasisIndex, freeModuleTensorPiEquiv, finsuppLeftTensorPiEquivPiTensor, tensorPiEquivFinitefreeModule, Module.Basis.repr, Module.Free.chooseBasis, LinearEquiv.symm, of_eq_true, Eq.trans, True, congrFun', congrArg, LinearEquiv.symm_apply_apply, eq_self, Eq.mpr, Eq.symm, LinearEquiv.apply_symm_apply and 65 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  8. def tensorPiEquivPiTensor' Tensoring with a finitely-presented module commutes with arbitrary products line 199 source

    Source documentation

    Tensoring with a finitely-presented module commutes with arbitrary products. To prove this, we consider the following commutative diagram. The goal is to show that i₃ is an isomorphism, which we do using the five lemma:

    Rᵐ ⊗[R] (Π i, N i) --f₁--> Rⁿ ⊗[R] (Π i, N i) --f₂--> M ⊗[R] (Π i, N i) --f₃--> 0 --f₄--> 0
        |                         |                         |                   |         |
        i₁                        i₂                        i₃                  i₄        i₅
        |                         |                         |                   |         |
        v                         v                         v                   v         v
Π i, (Rᵐ ⊗[R] N i) --g₁--> Π i, (Rⁿ ⊗[R] N i) --g₂--> Π i, (M ⊗[R] N i) --g₃--> 0 --g₄--> 0

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

    Statement uses: CommRing, AddCommGroup, Module, Module.FinitePresentation, LinearEquiv, RingHom.id, TensorProduct

    Proof uses: IsTensorProduct.equiv, TensorProduct.piRightHomBil

    19 instances, coercions and auxiliary constants left out.

    Tactic trace: 57 steps

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

    noncomputable def tensorPiEquivPiTensor' :
    M ⊗[R] (Π i, N i) ≃ₗ[R] Π i, (M ⊗[R] N i) := IsTensorProduct.equiv
…
  9. lemma tensorPi_equiv_piTensor'_apply line 272 source

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

    Statement uses: CommRing, AddCommGroup, Module, Module.FinitePresentation, Eq, TensorProduct, LinearEquiv, RingHom.id, tensorPiEquivPiTensor', TensorProduct.tmul

    Proof uses: rfl

    24 instances, coercions and auxiliary constants left out.