FLT/HaarMeasure/FiniteAdeleRing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

We show that GLₙ(𝔸ᶠ) and PGLₙ(𝔸ᶠ) are unimodular.

Imports (11)
Imported by 2 files
  1. lemma RestrictedProduct.modularCharacter_eq line 45 source

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

    Statement uses: Group, TopologicalSpace, Subgroup, Fact, IsOpen, CompactSpace, Subtype, Membership.mem, SecondCountableTopology, IsTopologicalGroup, LocallyCompactSpace, Countable, RestrictedProduct, Filter.cofinite, Eq, NNReal, MonoidHom, MeasureTheory.Measure.modularCharacter, finprod

    Proof uses: MeasurableSpace, borel, BorelSpace, BorelSpace.mk, rfl, Eq.mpr, MeasureTheory.mulEquivHaarChar, MulDistribMulAction.toContinuousMulEquiv, ConjAct, MulEquiv, ConjAct.toConjAct, id, congr, congrArg, MeasureTheory.modularCharacter_eq_mulEquivHaarChar, funext, ContinuousMulEquiv.restrictedProductCongrRight, Filter.mp_mem, Set.ofPred, Set and 32 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  2. instance RestrictedProduct.isUnimodularGroup line 59 source

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

    Statement uses: Group, TopologicalSpace, Subgroup, Fact, IsOpen, CompactSpace, Subtype, Membership.mem, SecondCountableTopology, Countable, IsUnimodularGroup, RestrictedProduct, Filter.cofinite

    Proof uses: IsUnimodularGroup.mk, MonoidHom.ext, NNReal, MeasureTheory.Measure.modularCharacter, OfNat.ofNat, MonoidHom, NNReal.eq, of_eq_true, Eq, Real, Eq.trans, True, congrFun', congrArg, finprod, RestrictedProduct.modularCharacter_eq, funext, IsUnimodularGroup.modularCharacter_eq_one, finprod_one, eq_self

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  3. instance RestrictedProduct.(instance at line 67) line 67 source
  4. instance RestrictedProduct.(instance at line 83) line 83 source
  5. instance RestrictedProduct.(instance at line 88) line 88 source
  6. lemma RestrictedProduct.unitsMap_algebraMap_le_center line 100 source

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

    Statement uses: CommSemiring, Semiring, Algebra, LE.le, Subgroup, Units, MonoidHom.range, Units.map, Algebra.algebraMap, Subgroup.center

    Proof uses: Membership.mem, Eq, MonoidHom, of_eq_true, RingHom, Eq.trans, HMul.hMul, True, forall_congr, congrArg, Algebra.commutes, eq_self, implies_true

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  7. instance RestrictedProduct.(instance at line 105) line 105 source
  8. instance RestrictedProduct.(instance at line 109) line 109 source
  9. instance RestrictedProduct.(instance at line 114) line 114 source
  10. lemma RestrictedProduct.Module.FaithfullyFlat.smul_top_eq_top_iff line 118 source

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

    Statement uses: CommRing, AddCommGroup, Module, Module.FaithfullyFlat, Ideal, Iff, Eq, Submodule, HSMul.hSMul, Top.top

    Proof uses: Iff.intro, Subsingleton, TensorProduct, HasQuotient.Quotient, Equiv.subsingleton, AddEquiv.toEquiv, LinearEquiv.toAddEquiv, RingHom.id, LinearEquiv.trans, TensorProduct.quotTensorEquivQuotSMul, Submodule.quotEquivOfEq, Iff.mp, Ideal.Quotient.subsingleton_iff, Module.FaithfullyFlat.rTensor_reflects_triviality, Eq.rec, Submodule.top_smul, Eq.symm

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  11. lemma RestrictedProduct.Ideal.map_eq_top_iff line 128 source

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

    Statement uses: CommRing, Algebra, Module.FaithfullyFlat, Ideal, Iff, Eq, Ideal.map, RingHom, Algebra.algebraMap, Top.top

    Proof uses: Iff.intro, Iff.mp, Submodule, HSMul.hSMul, RestrictedProduct.Module.FaithfullyFlat.smul_top_eq_top_iff, Eq.mpr, Submodule.restrictScalars, id, congrArg, Ideal.smul_top_eq_map, Submodule.restrictScalars_top, Eq.refl, Eq.rec, Ideal.map_top, Eq.symm

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  12. lemma RestrictedProduct.Finsupp.linearCombination_comm line 134 source

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

    Statement uses: CommSemiring, Finsupp, Eq, LinearMap, RingHom.id, Finsupp.linearCombination

    Proof uses: Eq.mpr, Finset.sum, Finsupp.support, HMul.hMul, id, congr, congrArg, Finset.sum_congr, HSMul.hSMul, Eq.refl, Finset, Membership.mem, Finset.sum_congr_of_eq_on_inter, of_eq_true, Not, OfNat.ofNat, Eq.trans, True, forall_congr, Ne and 7 more

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  13. lemma RestrictedProduct.Module.Free.exists_comp_linearMap_eq_id line 140 source

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

    Statement uses: CommRing, Algebra, Module.Free, Nontrivial, Exists, LinearMap, RingHom.id, Eq, LinearMap.comp, Algebra.linearMap, LinearMap.id

    Proof uses: Sigma, Module.Basis, Nonempty, Module.Free.exists_basis, Finsupp, LinearEquiv, Module.Basis.repr, OfNat.ofNat, Ideal, Ideal.span, Set.range, Top.top, Eq.mpr, Ideal.map, RingHom, Algebra.algebraMap, id, congrArg, Eq.symm, propext and 34 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  14. lemma RestrictedProduct.IsModuleTopology.isClosed_one_of_exists_linearMap line 157 source

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

    Statement uses: CommRing, Ring, Algebra, Exists, LinearMap, RingHom.id, Eq, LinearMap.comp, Algebra.linearMap, LinearMap.id, TopologicalSpace, IsModuleTopology, T1Space, IsClosed, Submodule, OfNat.ofNat

    Proof uses: Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim, Subsingleton, of_eq_true, Nontrivial, ContinuousAdd, IsModuleTopology.toContinuousAdd, Eq.mpr, LinearMap.ker, ContinuousLinearMap.mk, HSub.hSub, IsModuleTopology.continuous_of_linearMap, eq_of_heq, Set, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, SetLike, Submodule.ext and 11 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  15. lemma RestrictedProduct.Submonoid.isClosed_units line 173 source

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

    Statement uses: TopologicalSpace, Monoid, Submonoid, IsClosed, Units, Subgroup, Submonoid.units

    Proof uses: IsClosed.inter, Set.preimage, Inv.inv, Submonoid.inv, Submonoid.comap, MonoidHom, Units.coeHom, IsClosed.preimage, Units.continuous_val, Units.continuous_coe_inv

    19 instances, coercions and auxiliary constants left out.

  16. lemma RestrictedProduct.Units.range_map line 177 source

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

    Statement uses: Monoid, MonoidHom, Function.Injective, Eq, Subgroup, Units, MonoidHom.range, Units.map, Submonoid.units, MonoidHom.mrange

    Proof uses: Subgroup.ext, Iff.intro, Membership.mem, of_eq_true, Eq.trans, And, Submonoid, Inv.inv, True, congr, congrArg, Exists, and_self, Set, Submonoid.comap, Units.coeHom, Submonoid.inv, Exists.intro, Units.mk, HMul.hMul and 11 more

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  17. lemma RestrictedProduct.isClosed_unitsMap_matrix line 185 source

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

    Statement uses: CommRing, TopologicalSpace, IsTopologicalRing, T1Space, Fintype, DecidableEq, IsClosed, Matrix.GeneralLinearGroup, Matrix, Subgroup, Units, MonoidHom.range, Units.map, Algebra.algebraMap

    Proof uses: IsEmpty, Nonempty, Or, Eq, isEmpty_or_nonempty, Or.inl, of_eq_true, Set.range, MonoidHom, RingHom, Or.inr, Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim, Subsingleton, Membership.mem, Nontrivial, Subring, RingHom.range, Eq.mpr, Submodule, OfNat.ofNat and 39 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  18. instance RestrictedProduct.(instance at line 201) line 201 source