FLT/DedekindDomain/FiniteAdeleRing/TensorRestrictedProduct.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

16 declarations, 0 contain sorry, 0 declared as axioms

Tensor product distributing over a restricted product

For a flat R-module M and a restricted product of R-modules N i relative to submodules L i, we construct the natural R-linear (and M-linear) map M ⊗_R ∏'ᵢ [N i, L i] → ∏'ᵢ [M ⊗_R N i, M ⊗_R L i].

Imports (5)
Imported by 2 files
  1. def RestrictedProduct.rangeLTensor M ⊗_R (L i) as an R-submodule of M ⊗_R (N i) line 35 source

    Source documentation

    M ⊗_R (L i) as an R-submodule of M ⊗_R (N i).

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

    Statement uses: CommRing, AddCommGroup, Module, Submodule, TensorProduct

    Proof uses: LinearMap.range, Subtype, Membership.mem, RingHom.id, LinearMap.lTensor, Submodule.subtype

    16 instances, coercions and auxiliary constants left out.

    def rangeLTensor (i : ι) : Submodule R (M ⊗[R] N i) :=
…
  2. def RestrictedProduct.rangeLTensorLeft M ⊗_R (L i) as an M-submodule of M ⊗_R (N i) line 39 source

    Source documentation

    M ⊗_R (L i) as an M-submodule of M ⊗_R (N i).

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

    Statement uses: CommSemiring, Algebra, Semiring, Submodule, TensorProduct

    Proof uses: LinearMap.range, Subtype, Membership.mem, RingHom.id, LinearMap, TensorProduct.AlgebraTensorModule.lTensor, Submodule.subtype

    28 instances, coercions and auxiliary constants left out.

    noncomputable def rangeLTensorLeft (R M : Type*) [CommSemiring R] [CommSemiring M] [Algebra R M]
    {ι : Type*} (N : ι → Type*) [∀ i, Semiring (N i)] [∀ i, Algebra R (N i)]
    (L : ∀ i, Submodule R (N i)) (i : ι) : Submodule M (M ⊗[R] N i) :=
…
  3. def RestrictedProduct.lTensor The R-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i) line 47 source

    Source documentation

    The R-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i).

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

    Statement uses: CommRing, AddCommGroup, Module, Filter, Submodule, LinearMap, RingHom.id, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensor

    Proof uses: Filter.Eventually, Set.MapsTo, TensorProduct.mk, TensorProduct.lift, LinearMap.mk, AddHom.mk, RestrictedProduct.mapAlongLinearMap, id, Filter.tendsto_id

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

    def lTensor :
    M ⊗[R] Πʳ i, [N i, L i]_[ℱ] →ₗ[R] Πʳ i, [M ⊗[R] N i, rangeLTensor R M N L i]_[ℱ] :=
…

    Mentions: RestrictedProduct.rangeLTensor

  4. def RestrictedProduct.lTensorLeft The M-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i) line 62 source

    Source documentation

    The M-linear map φ : M ⊗_R ∏'_i [N i, L i]_[𝓕] → ∏'_i [M ⊗_R (N i), M ⊗_R (L i)]_[𝓕] given by φ (m ⊗ n) i = m ⊗ (n i).

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

    Statement uses: CommRing, Algebra, Ring, Filter, Submodule, LinearMap, RingHom.id, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensorLeft

    Proof uses: Filter.Eventually, Set.MapsTo, TensorProduct.mk, LinearMap.mk, AddHom.mk, TensorProduct.tmul, OfNat.ofNat, SMulMemClass, IsScalarTower, LinearMap.liftBaseChange, RestrictedProduct.mapAlongLinearMap, id, Filter.tendsto_id

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

    noncomputable def lTensorLeft (R M : Type*) [CommRing R] [CommRing M] [Algebra R M] {ι : Type*}
    (N : ι → Type*) [∀ i, Ring (N i)] [∀ i, Algebra R (N i)] (ℱ : Filter ι)
    (L : ∀ i, Submodule R (N i)) :
    M ⊗[R] Πʳ i, [N i, L i]_[ℱ] →ₗ[M] Πʳ i, [M ⊗[R] N i, rangeLTensorLeft R M N L i]_[ℱ] :=
…

    Mentions: RestrictedProduct.rangeLTensorLeft

  5. lemma RestrictedProduct.lTensor_tmul line 79 source

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

    Statement uses: CommRing, AddCommGroup, Module, Filter, Submodule, RestrictedProduct, Eq, TensorProduct, RestrictedProduct.rangeLTensor, LinearMap, RingHom.id, RestrictedProduct.lTensor, TensorProduct.tmul

    Proof uses: rfl

    30 instances, coercions and auxiliary constants left out.

  6. lemma RestrictedProduct.lTensorLeft_tmul line 85 source

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

    Statement uses: CommRing, Algebra, Ring, Submodule, Filter, RestrictedProduct, Eq, TensorProduct, RestrictedProduct.rangeLTensorLeft, LinearMap, RingHom.id, RestrictedProduct.lTensorLeft, TensorProduct.tmul

    Proof uses: Eq.mpr, LinearMap.liftBaseChange, RestrictedProduct.mapAlongLinearMap, id, Filter.tendsto_id, LinearMap.mk, AddHom.mk, OfNat.ofNat, congrArg, RestrictedProduct.lTensorLeft.eq_1, HSMul.hSMul, LinearMap.liftBaseChange_tmul, RestrictedProduct.smul_apply, RestrictedProduct.mapAlongLinearMap_apply, of_eq_true, Eq.trans, True, congrFun', CommSemiring, Module and 4 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  7. lemma RestrictedProduct.coe_lTensorLeft_eq_lTensor line 93 source

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

    Statement uses: CommRing, Algebra, Ring, Submodule, Filter, Eq, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensorLeft, LinearMap, RingHom.id, RestrictedProduct.lTensorLeft, RestrictedProduct.rangeLTensor, RestrictedProduct.lTensor

    Proof uses: funext, RestrictedProduct.ext, TensorProduct.inductionOn, Eq.mpr, TensorProduct.tmul, id, congrFun', congrArg, RestrictedProduct.lTensorLeft_tmul, Eq.refl, HAdd.hAdd, congr, Eq.trans, congrFun, map_add

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  8. def RestrictedProduct.tmulEquivRangeLTensor R-Linear isomorphism between M ⊗_R (L i) and rangeLTensor R M N L i line 105 source

    Source documentation

    R-Linear isomorphism between M ⊗_R (L i) and rangeLTensor R M N L i.

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

    Statement uses: CommRing, AddCommGroup, Module, Submodule, Module.Flat, LinearEquiv, RingHom.id, TensorProduct, Subtype, Membership.mem, RestrictedProduct.rangeLTensor

    Proof uses: LinearEquiv.ofInjective, LinearMap.lTensor, Submodule.subtype

    23 instances, coercions and auxiliary constants left out.

    noncomputable def tmulEquivRangeLTensor (i : ι) : M ⊗[R] (L i) ≃ₗ[R] rangeLTensor R M N L i :=
…

    Mentions: RestrictedProduct.rangeLTensor

  9. def RestrictedProduct.lTensorPrincipalEquiv R-Linear isomorphism that's propositionally equal to lTensor line 113 source

    Source documentation

    R-Linear isomorphism that's propositionally equal to lTensor.

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

    Statement uses: CommRing, AddCommGroup, Module, Submodule, Set, Module.FinitePresentation, Module.Flat, LinearEquiv, RingHom.id, TensorProduct, RestrictedProduct, Filter.principal, RestrictedProduct.rangeLTensor

    Proof uses: ite, Membership.mem, Classical.propDecidable, Top.top, Subtype, LinearEquiv.mk, LinearMap.mk, AddHom.mk, Subtype.mk, Filter.Eventually, LinearEquiv.lTensor, tensorPiEquivPiTensor', LinearEquiv.trans, LinearEquiv.ofEq, RestrictedProduct.tmulEquivRangeLTensor, Not, LinearEquiv.ofTop, dite, LinearEquiv.symm

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

    noncomputable def lTensorPrincipalEquiv :
    M ⊗[R] Πʳ i, [N i, L i]_[𝓟 S] ≃ₗ[R] Πʳ i, [M ⊗[R] N i, rangeLTensor R M N L i]_[𝓟 S] :=
…

    Mentions: RestrictedProduct.rangeLTensor

  10. lemma RestrictedProduct.lTensorPrincipalEquiv_tmul line 165 source

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

    Statement uses: CommRing, AddCommGroup, Module, Submodule, Set, Module.FinitePresentation, Module.Flat, RestrictedProduct, Filter.principal, Eq, TensorProduct, RestrictedProduct.rangeLTensor, LinearEquiv, RingHom.id, RestrictedProduct.lTensorPrincipalEquiv, TensorProduct.tmul

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, congrFun, LinearMap.range, Subtype, Membership.mem, LinearMap.lTensor, Submodule.subtype, Subtype.mk, Filter.Eventually, dite, Classical.propDecidable, LinearMap, ite, Top.top, LinearEquiv.lTensor, LinearEquiv.ofEq and 10 more

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  11. lemma RestrictedProduct.lTensor_bijective line 172 source

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

    Statement uses: CommRing, AddCommGroup, Module, Filter, Submodule, Module.FinitePresentation, Module.Flat, Function.Bijective, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensor, LinearMap, RingHom.id, RestrictedProduct.lTensor

    Proof uses: LinearEquiv, Module.DirectLimit, OrderDual, Set, Filter.sets, Membership.mem, Filter.principal, LE.le, RestrictedProduct.inclusionLinearMap, Filter.monotone_principal, LinearMap.lTensor, TensorProduct.directLimitRight, IsDirectLimit.Module.linearEquiv, Iff.mpr, Filter.le_principal_iff, Subtype.property, Module.DirectLimit.of, LinearEquiv.trans, LinearEquiv.lTensor, Module.DirectLimit.congr and 76 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

  12. lemma RestrictedProduct.lTensorLeft_bijective line 227 source

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

    Statement uses: CommRing, Algebra, Ring, Submodule, Filter, Module.Flat, Module.FinitePresentation, Function.Bijective, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensorLeft, LinearMap, RingHom.id, RestrictedProduct.lTensorLeft

    Proof uses: Eq.mpr, RestrictedProduct.rangeLTensor, RestrictedProduct.lTensor, id, Eq, congrArg, RestrictedProduct.coe_lTensorLeft_eq_lTensor, RestrictedProduct.lTensor_bijective

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  13. def RestrictedProduct.lTensorEquiv The R-linear isomorphism given by lTensor when M is a finite flat R-module line 235 source

    Source documentation

    The R-linear isomorphism given by lTensor when M is a finite flat R-module.

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

    Statement uses: CommRing, AddCommGroup, Module, Filter, Submodule, Module.FinitePresentation, Module.Flat, LinearEquiv, RingHom.id, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensor

    Proof uses: LinearEquiv.ofBijective, RestrictedProduct.lTensor, RestrictedProduct.lTensor_bijective

    28 instances, coercions and auxiliary constants left out.

    noncomputable def lTensorEquiv :
    M ⊗[R] Πʳ i, [N i, L i]_[ℱ] ≃ₗ[R] Πʳ i, [M ⊗[R] N i, rangeLTensor R M N L i]_[ℱ] :=
…

    Mentions: RestrictedProduct.rangeLTensor

  14. def RestrictedProduct.lTensorEquivLeft The M-linear isomorphism given by lTensor when M is a finite flat R-module line 240 source

    Source documentation

    The M-linear isomorphism given by lTensor when M is a finite flat R-module.

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

    Statement uses: CommRing, Algebra, Ring, Submodule, Filter, Module.Flat, Module.FinitePresentation, LinearEquiv, RingHom.id, TensorProduct, RestrictedProduct, RestrictedProduct.rangeLTensorLeft

    Proof uses: LinearEquiv.ofBijective, RestrictedProduct.lTensorLeft, RestrictedProduct.lTensorLeft_bijective

    36 instances, coercions and auxiliary constants left out.

    noncomputable def lTensorEquivLeft (R M : Type*) [CommRing R] [CommRing M] [Algebra R M] {ι : Type*}
    (N : ι → Type*) [∀ i, Ring (N i)] [∀ i, Algebra R (N i)] (L : ∀ i, Submodule R (N i))
    (ℱ : Filter ι) [Module.Flat R M] [Module.FinitePresentation R M] :
    M ⊗[R] Πʳ i, [N i, L i]_[ℱ] ≃ₗ[M] Πʳ i, [M ⊗[R] N i, rangeLTensorLeft R M N L i]_[ℱ] :=
…

    Mentions: RestrictedProduct.rangeLTensorLeft

  15. lemma RestrictedProduct.lTensorEquiv_tmul line 247 source

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

    Statement uses: CommRing, AddCommGroup, Module, Filter, Submodule, Module.FinitePresentation, Module.Flat, RestrictedProduct, Eq, TensorProduct, RestrictedProduct.rangeLTensor, LinearEquiv, RingHom.id, RestrictedProduct.lTensorEquiv, TensorProduct.tmul

    Proof uses: rfl

    34 instances, coercions and auxiliary constants left out.

  16. lemma RestrictedProduct.lTensorEquivLeft_tmul line 252 source

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

    Statement uses: CommRing, Algebra, Ring, Submodule, Filter, Module.Flat, Module.FinitePresentation, RestrictedProduct, Eq, TensorProduct, RestrictedProduct.rangeLTensorLeft, LinearEquiv, RingHom.id, RestrictedProduct.lTensorEquivLeft, TensorProduct.tmul

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, RestrictedProduct.lTensorLeft_tmul, eq_self

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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