AlgebrasOverFields_minimalPrimes_bijection_of_geometrically_IrreducibleAlgebra.lean`

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib

class GeometricallyIrreducibleAlgebra line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra
4 instances, coercions and auxiliary constants left out.
Also declared: APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_transitive.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_geometrically_irreducible_tfae.lean:41 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:41 (same declaration text).
def alg_dir_lim line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Preorder, IsDirected, LE.le, Nonempty, CommRing, Algebra, AlgHom, Ring.DirectLimit
Proof uses: Classical.arbitrary, RingHom, Ring.DirectLimit.of, RingHom.toAlgebra, RingHom.comp, algebraMap
17 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_of_directed_colimit.lean:46 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_GeometricallyIrreducibleAlgebra_transitive.lean:46 (same statement text; different proof or body), APNOutputs/StacksProject/AlgebrasOverFields_geometrically_irreducible_tfae.lean:46 (same declaration text), APNOutputs/StacksProject/AlgebrasOverFields_unique_minimal_prime_of_tensor_product_of_separably_closed.lean:46 (same declaration text). Qualify references as alg_dir_lim@path.
def tensor_basis line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Module.Basis, Module.Free.ChooseBasisIndex, TensorProduct
Proof uses: Algebra.TensorProduct.basis, Module.Free.chooseBasis
42 instances, coercions and auxiliary constants left out.
lemma sum_in_Q line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, TensorProduct, Finsupp, Module.Free.ChooseBasisIndex, Membership.mem, Finset, Finsupp.support, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, LinearEquiv, RingHom.id, LinearEquiv.symm, Module.Basis.repr, tensor_basis
Proof uses: Finsupp.induction, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, map_zero, RingHom, Not, Ne, HAdd.hAdd, Finsupp.single, Iff.mpr, Finsupp.mem_support_iff, Eq.mpr, id, Eq, Finsupp.add_apply, ite, Finsupp.single_apply and 27 more
138 instances, coercions and auxiliary constants left out.
Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma basis_repr_not_in_P line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, TensorProduct, Not, Membership.mem, Exists, Module.Free.ChooseBasisIndex, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, Finsupp, LinearEquiv, RingHom.id, Module.Basis.repr, tensor_basis
Proof uses: Classical.byContradiction, LinearEquiv.symm, sum_in_Q, Finset, Finsupp.support, Eq.mp, Eq.trans, binderNameHint, forall_congr, congrArg, LinearEquiv.symm_apply_apply
94 instances, coercions and auxiliary constants left out.
Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma exists_pow_mul_eq_zero_of_mem_minimalPrimes line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Membership.mem, Set, minimalPrimes, Exists, Nat, And, Not, Eq, HMul.hMul, HPow.hPow, OfNat.ofNat
Proof uses: Submonoid, Submonoid.mk, Subsemigroup.mk, setOf, Exists.intro, HAdd.hAdd, And.intro, Ideal.IsPrime, And.left, LE.le, Bot.bot, Or, Ideal.IsPrime.mem_or_mem, False, Or.inl, Or.inr, Eq.refl, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.instCommSemiringNat, Nat.rawCast and 69 more
118 instances, coercions and auxiliary constants left out.
Tactic trace: 79 steps
Open to load the checked before-and-after goal states.
lemma isPrime_nilradical_of_irreducible line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IrreducibleSpace, PrimeSpectrum, Ideal.IsPrime, nilradical
Proof uses: Iff.mpr, And, Ne, Ideal, Top.top, Membership.mem, HMul.hMul, Or, Ideal.isPrime_iff, by_contradiction, Not, dite, False, Exists, Eq, Classical.propDecidable, Exists.elim, Submodule, And.elim, Exists.choose and 53 more
80 instances, coercions and auxiliary constants left out.
Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma minimal_prime_eq line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ideal, Membership.mem, Set, minimalPrimes, Ideal.IsPrime, LE.le, Eq
Proof uses: le_antisymm, And.right, And, Bot.bot, And.intro, bot_le
28 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma unique_minimal_prime line 220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IrreducibleSpace, PrimeSpectrum, ExistsUnique, Ideal, Membership.mem, Set, minimalPrimes
Proof uses: Ideal.IsPrime, nilradical, isPrime_nilradical_of_irreducible, id, Ideal.minimalPrimes, Bot.bot, Subsingleton, Nontrivial, Or, Eq, subsingleton_or_nontrivial, Exists, And, Or.inl, False, Ideal.IsPrime.ne_top', Subsingleton.elim, Top.top, Eq.refl, Or.inr and 23 more
32 instances, coercions and auxiliary constants left out.
Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma unique_minimal_prime_of_geometricallyIrreducible line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, ExistsUnique, Ideal, TensorProduct, Membership.mem, Set, minimalPrimes
Proof uses: IrreducibleSpace, PrimeSpectrum, GeometricallyIrreducibleAlgebra.out, unique_minimal_prime
43 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def FiberRing line 240 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal
Proof uses: ULift, FractionRing, HasQuotient.Quotient
10 instances, coercions and auxiliary constants left out.
instance FiberRing_field line 243 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, FiberRing
Proof uses: inferInstanceAs, ULift, FractionRing, HasQuotient.Quotient
13 instances, coercions and auxiliary constants left out.
instance FiberRing_algebra line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, FiberRing
Proof uses: inferInstanceAs, ULift, FractionRing, HasQuotient.Quotient, nonZeroDivisors
27 instances, coercions and auxiliary constants left out.
lemma mapsTo_minimalPrimes_comap line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Set.MapsTo, Ideal, TensorProduct, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, minimalPrimes
Proof uses: Membership.mem, Set, Ideal.IsPrime, And.left, LE.le, Bot.bot, And, Ideal.comap_isPrime, And.intro, bot_le, Submodule, Classical.byContradiction, Not, Nat, Exists, Eq, HMul.hMul, HPow.hPow, OfNat.ofNat, False and 29 more
122 instances, coercions and auxiliary constants left out.
Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
instance FiberRing_algebraR line 285 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, FiberRing
Proof uses: inferInstanceAs, ULift, FractionRing, HasQuotient.Quotient, nonZeroDivisors
28 instances, coercions and auxiliary constants left out.
instance FiberRing_isScalarTower line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, IsScalarTower, FiberRing
Proof uses: inferInstanceAs, ULift, FractionRing, HasQuotient.Quotient, nonZeroDivisors
60 instances, coercions and auxiliary constants left out.
def fiberMap line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, AlgHom, TensorProduct, FiberRing
Proof uses: IsScalarTower.toAlgHom, AlgHom.id, Algebra.TensorProduct.map, AlgEquiv, Algebra.TensorProduct.comm, AlgHom.comp
56 instances, coercions and auxiliary constants left out.
lemma fiber_ker line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, Eq, Ideal.comap, FiberRing, RingHom, algebraMap, Bot.bot
Proof uses: Eq.mpr, Iff, Membership.mem, OfNat.ofNat, id, Eq.trans, forall_congr, congrArg, Submodule, Iff.trans, HasQuotient.Quotient, Ideal.Quotient.mk, ULift, FractionRing, Iff.symm, Ideal.Quotient.eq_zero_iff_mem, nonZeroDivisors, IsFractionRing.to_map_eq_zero_iff, ULift.up, ULift.up_inj and 1 more
66 instances, coercions and auxiliary constants left out.
Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma fiberMap_comp_includeLeft line 305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, Eq, RingHom, TensorProduct, FiberRing, RingHom.comp, AlgHom.toRingHom, fiberMap, Algebra.TensorProduct.includeLeft, Algebra.TensorProduct.includeRight, algebraMap
Proof uses: of_eq_true, AlgHom, AlgHom.comp, AlgEquiv, Algebra.TensorProduct.comm, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, Eq.trans, True, TensorProduct.tmul, OfNat.ofNat, forall_congr, HSMul.hSMul, congr, congrArg, Algebra.algebraMap_eq_smul_one, eq_self, eq_true, True.intro and 1 more
80 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma fiberMap_comp_includeLeft_apply line 310 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, Eq, TensorProduct, FiberRing, AlgHom, fiberMap, Algebra.TensorProduct.includeLeft, Algebra.TensorProduct.includeRight, RingHom, algebraMap
Proof uses: RingHom.comp, AlgHom.toRingHom, Iff.mp, RingHom.ext_iff, fiberMap_comp_includeLeft
63 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def fiberMap_alt line 316 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, AlgHom, TensorProduct, FiberRing
Proof uses: Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id
36 instances, coercions and auxiliary constants left out.
lemma fiberMap_alt_comp_includeLeft line 320 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, Eq, RingHom, TensorProduct, FiberRing, RingHom.comp, AlgHom.toRingHom, fiberMap_alt, Algebra.TensorProduct.includeLeft, algebraMap
Proof uses: of_eq_true, AlgHom, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, Eq.trans, True, TensorProduct.tmul, OfNat.ofNat, forall_congr, HSMul.hSMul, congr, congrArg, Algebra.algebraMap_eq_smul_one, eq_self, eq_true, True.intro, implies_true
75 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def tensor_basis_K line 325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, Module.Basis, Module.Free.ChooseBasisIndex, FiberRing, TensorProduct
Proof uses: Algebra.TensorProduct.basis, Module.Free.chooseBasis
47 instances, coercions and auxiliary constants left out.
lemma fiberMap_alt_apply_symm line 331 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, Finsupp, Module.Free.ChooseBasisIndex, Eq, TensorProduct, FiberRing, AlgHom, fiberMap_alt, LinearEquiv, RingHom.id, LinearEquiv.symm, Module.Basis.repr, tensor_basis, tensor_basis_K, Finsupp.mapRange, RingHom and 2 more
Proof uses: Eq.mpr, Finset.sum, Finsupp.support, Algebra.TensorProduct.map, IsScalarTower.toAlgHom, AlgHom.id, HSMul.hSMul, TensorProduct.tmul, OfNat.ofNat, Module.Basis, Module.Free.chooseBasis, LinearMap, Finsupp.linearCombination, Algebra.TensorProduct.basis, id, congr, congrArg, Eq.trans, Module.Basis.repr_symm_apply, Finsupp.sum and 32 more
144 instances, coercions and auxiliary constants left out.
Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma fiberMap_ker_le line 337 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, Ideal, Ideal.IsPrime, TensorProduct, Eq, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, LE.le, RingHom.ker, FiberRing, RingHom, AlgHom.toRingHom, fiberMap
Proof uses: Membership.mem, Submodule, OfNat.ofNat, AlgHom.comp, Algebra.TensorProduct.comm, fiberMap_alt, rfl, Trans.trans, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Function.Injective, AlgEquiv, AlgEquiv.injective, map_zero, Finsupp, Module.Free.ChooseBasisIndex, LinearEquiv and 20 more
113 instances, coercions and auxiliary constants left out.
Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma fiber_unique_minimal_prime line 380 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Ideal, TensorProduct, Membership.mem, Set, minimalPrimes, Eq, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft
Proof uses: Ideal.IsPrime, And.left, LE.le, Bot.bot, And, Ideal.comap_isPrime, FiberRing, ExistsUnique, unique_minimal_prime_of_geometricallyIrreducible, fiberMap, nilradical, IrreducibleSpace, PrimeSpectrum, GeometricallyIrreducibleAlgebra.out, isPrime_nilradical_of_irreducible, And.intro, bot_le, Submodule, Nat, OfNat.ofNat and 16 more
91 instances, coercions and auxiliary constants left out.
Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma fiber_exists_minimal_prime line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Ideal, Membership.mem, Set, minimalPrimes, Exists, TensorProduct, And, Eq, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft
Proof uses: Ideal.IsPrime, And.left, LE.le, Bot.bot, FiberRing, ExistsUnique, unique_minimal_prime_of_geometricallyIrreducible, fiberMap, Ideal.comap_isPrime, Ideal.ext, Iff.intro, RingHom, AlgHom.toRingHom, Algebra.TensorProduct.includeRight, Ideal.eq_bot_of_prime, algebraMap, Eq.mp, congrArg, fiberMap_comp_includeLeft_apply, fiber_ker and 9 more
77 instances, coercions and auxiliary constants left out.
Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
lemma injOn_minimalPrimes_comap line 490 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Set.InjOn, Ideal, TensorProduct, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, minimalPrimes
Proof uses: Membership.mem, Set, Eq, fiber_unique_minimal_prime
51 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma surjOn_minimalPrimes_comap line 498 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Set.SurjOn, Ideal, TensorProduct, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, minimalPrimes
Proof uses: Membership.mem, Set, fiber_exists_minimal_prime
30 instances, coercions and auxiliary constants left out.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem minimalPrimes_bijection_of_geometricallyIrreducibleAlgebra line 507 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, GeometricallyIrreducibleAlgebra, Set.BijOn, Ideal, TensorProduct, Ideal.comap, AlgHom, Algebra.TensorProduct.includeLeft, minimalPrimes
Proof uses: And.intro, Set.MapsTo, And, Set.InjOn, Set.SurjOn, mapsTo_minimalPrimes_comap, injOn_minimalPrimes_comap, surjOn_minimalPrimes_comap
50 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.